Algebric Decision Diagrams and Their Applications

In this paper we present theory and experimental results on Algebraic Decision Diagrams. These diagrams extend BDDs by allowing values from an arbitrary finite domain to be associated with the terminal nodes of the diagram. We present a treatment founded in Boolean algebras and discuss algorithms and results in several areas of application: Matrix multiplication, shortest path algorithms, and direct methods for numerical linear algebra. Although we report an essentially negative result for Gaussian elimination per se, we propose a modified form of ADDs which appears to circumvent the difficulties in some cases. We discuss the relevance of our findings and point to directions for future work.     

Symbolic Verification and Analysis of Discrete Timed Systems

This paper presents a novel approach for real-time model checking. It combines the efficiency of traditional symbolic model checking with possibilities to describe and specify real-time systems. Using multi-terminal binary decision diagrams to represent time and time intervals, it becomes possible to transfer efficient algorithms and optimization heuristics known from standard CTL model checking to real-time applications. By introducing a new variant of models called I/O-interval structures we can describe systems in a modular way. Interval structures allow model composition of real-time structures such that state explosion effects are greatly reduced. Besides model checking we also present analysis algorithms which allow to compute key properties like system latencies and minimal response times from the structures describing the system. The practical applicability is proven by experimental results, computed by the verification system RAVEN, which implements all described algorithms, including counterexample generation and waveform visualization.