Jörn Ossowski



Symbolic Representation and Manipulation of Discrete Functions
Jörn Ossowski (Diploma Thesis)
FEVBDDs are well suited for algebraic computation. This is because the multiplication and addition with a constant value can be calculated without a traversal. In this thesis Normalized Algebraic Decision Diagrams (NADDs) were introduced, which share the same advantages as FEVBDDs. Additionally, the maximum and mimimum value of a function can be calculated in constant time.
The JJS-BDD library is not available anymore. JINC is the redevelopment.


Symbolic Reasoning with Weighted and Normalized Decision Diagrams
Jörn Ossowski, Christel Baier (published in Calculemus 2005)
Several variants of Bryant's ordered binary decision diagrams have been suggested in the literature to reason about discrete functions. In this paper, we introduce a generic notion of weighted decision diagrams that captures many of them and present criteria for canonicity. As a special instance of such weighted diagrams, we introduce a new BDD-variant for real-valued functions, called normalized algebraic decision diagrams. Regarding the number of nodes and arithmetic operations like addition and multiplication, these normalized diagrams are as efficient as factored edge-valued binary decision diagrams, while several other operators, like the calculation of extrema, minimum or maximum of two functions or the switch from real-valued functions to boolean functions through a given threshold, are more efficient for normalized diagrams than for their factored counterpart.
The JJS-BDD library is not available anymore. JINC is the redevelopment.


Partially-shared Zero-Suppressed Multi-Terminal BDDs: Concept, Algorithms and Applications
Kai Lampka, Markus Siegle, Jörn Ossowski, Christel Baier (published as TIK)
Multi-Terminal Binary Decision Diagrams (MTBDDs) are a well accepted technique for the state graph (SG) based quantitative analysis of large and complex systems specified by means of high-level model description techniques. However, this type of Decision Diagram (DD) is not always the best choice, since finite functions with small satisfaction sets, and where the fulfilling assignments possess many 0-assigned positions, may yield relatively large MTBDD based representations. Therefore, this article introduces zero-suppressed MTBDDs and proves that they are canonical representations of multi-valued functions on finite input sets. For manipulating DDs of this new type, possibly defined over different sets of function variables, the concept of partially-shared zero-suppressed MTBDDs and respective algorithms are developed. The efficiency of this new approach is demonstrated by comparing it to the well-known standard type of MTBDDs, where both types of DDs have been implemented by us within the C++-based DD-package JINC. The benchmarking takes place in the context of Markovian analysis and probabilistic model checking of systems. In total, the presented work extends existing approaches, since it not only allows one to directly employ (multi-terminal) zero-suppressed DDs in the field of quantitative verification, but also clearly demonstrates their efficiency.

A Uniform Framework for Weighted Decision Diagrams and its Implementation
Jörn Ossowski, Christel Baier (published in STTT)
This paper introduces a generic framework for OBDD variants with weighted edges. It covers many boolean and multi-valued OBDD-variants that have been studied in the literature and applied to the symbolic representation and manipulation of discrete functions. Our framework supports reasoning about reducedness and canonicity of new OBDD-variants and provides a platform for the implementation and comparison of OBDD-variants. Furthermore, we introduce a new multi-valued OBDD-variant, called normalized algebraic decision diagram, which supports min/max-operations and turns out to be very useful for, e.g., integer linear programming and model checking probabilistic systems. Finally, we explain the main features of an implementation of a newly developed BDD-package, called JINC, which relies on our generic notion of weighted decision diagrams, and realizes various synthesis algorithms, reordering techniques and transformation algorithms for boolean and multi-terminal OBDDs, with or without edge-attributes, and their zero-suppressed variants.


JINC – A Multi-Threaded Library for Higher-Order Weighted Decision Diagram Manipulation
Jörn Ossowski
Ordered Binary Decision Diagrams (OBDDs) have been proven to be an efficient data structure for symbolic algorithms. The efficiency of the symbolic methods de- pends on the underlying OBDD library. Available OBDD libraries are based on the standard concepts and so far only differ in implementation details. This thesis introduces new techniques to increase run-time and space-efficiency of an OBDD library.
This thesis introduces the framework of Higher-Order Weighted Decision Diagrams (HOWDDs) to combine the similarities of different OBDD variants. This framework pioneers the basis for the new variant Toggling Algebraic Decision Diagrams (TADDs) which has been shown to be a space-efficient HOWDD variant for symbolic matrix representation. The concept of HOWDDs has been use to implement the OBDD library JINC. This thesis also analyzes the usage of multi-threading techniques to speed-up OBDD manipulations. A new reordering framework applies the advantages of multi-threading techniques to reordering algorithms. This approach uses an abstraction layer so that the original reordering algorithms are not touched. The challenge that arise from a straight forward algorithm is that the computed-tables and the garbage collection are not as efficient as in a single- threaded environment. We resolve this problem by developing a new multi-operand APPLY algorithm that eliminates the creation of temporary nodes which could occur during computation and thus reduces the need for caching or garbage collection.
The HOWDD framework leads to an efficient library design which has been shown to be more efficient than the established OBDD library CUDD. The HOWDD instance TADD reduces the needed number of nodes by factor two compared to ordinary ADDs. The new multi-threading approaches are more efficient than single-threading approaches by several factors. In the case of the new reordering framework the speed- up almost equals the theoretical optimal speed-up. The novel multi-operand APPLY algorithm reduces the memory usage for the n-queens problem by factor 50 which enables the calculation of bigger problem instances compared to the traditional APPLY approach.
The new approaches improve the performance and reduce the memory footprint. This leads to the conclusion that applications should be reviewed whether they could benefit from the new multi-threading multi-operand approaches introduced and discussed in this thesis.


Towards Usable Client-Centric Privacy Advisory for Mobile Collaborative Applications Based on BDDs
Mohamed Bourimi, Jörn Ossowski, Dhiah el Diehn I. Abou-Tair, Stefan Berlik, Dirar Abu-Saymeh
Considering privacy advisory for collaborative settings on mobile devices, this paper presents an innovative approach to simultaneously support dynamically reconfigurable privacy advisory and the usability of providing it. Regarded are interaction design requirements such as user-friendless and non-intrusive advisory as well as restrictions of today's mobile devices like CPU and memory consumption etc. The prototypic implementation of a client-centric privacy advisor based on binary decision diagrams shows that the proposed mechanisms integrated in an iPhone application can be effectively extended and correlated with a usable privacy-enhancing model.