A new algorithm for partitioned symbolic reachability analysis. (English) Zbl 1337.68167

Halava, Vesa (ed.) et al., Proceedings of the 2nd workshop on reachability problems in computational models (RP 2008), Liverpool, UK, September 15–17, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 223, 137-151 (2008).
Summary: Binary Decision Diagrams (BDDs) and their multi-terminal extensions have shown to be very helpful for the quantitative verification of systems. Many different approaches have been proposed for deriving symbolic state graph (SG) representations from high-level model descriptions, where compositionality has shown to be crucial for the efficiency of the schemes. Since the symbolic composition schemes deliver the potential SG of a high-level model, one must execute a reachability analysis on the level of the symbolic structures. This step is the main resource of CPU-time and peak memory consumption when it comes to symbolic SG generation. In this work a new operator for zero-suppressed BDDs and their multi-terminal extensions for carrying out (partitioned) symbolic reachability analysis is presented. This algorithm not only replaces standard BDD-based schemes, it even makes symbolic composition as found in contemporary symbolic model checkers such as Prism and Caspa obsolete.
For the entire collection see [Zbl 1279.68014].


68Q60 Specification and verification (program logics, model checking, etc.)
68P05 Data structures
68R10 Graph theory (including graph drawing) in computer science
68W30 Symbolic computation and algebraic computation


Full Text: DOI


[1] Multi-terminal binary decision diagrams, Formal methods in system design, 10, 2-3, (April-May 1997), Special Issue on
[2] Akers, S.B., Binary decision diagrams, IEEE transactions on computers, C-27, 6, 509-516, (June 1978)
[3] Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE transactions on computers, C-35, 8, 677-691, (August 1986)
[4] J.R. Burch, E.M. Clarke, and D.E. Long. Symbolic Model Checking with Partitioned Transition Relations. In A. Halaas and P.B. Denyer, editors, International Conference on Very Large Scale Integration, pages 49-58, Edinburgh, Scotland, 1991. North-Holland
[5] Clarke, E.M.; Grumberg, O.; Pele, D.A., Model checking, (1999), The MIT Press Cambridge, MA (USA)
[6] de Alfaro, L.; Kwiatkowska, M.; Norman, G.; Parker, D.; Segala, R., Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation, (), 395-410 · Zbl 0960.68109
[7] Kuntz, M.; Siegle, M., Deriving symbolic representations from stochastic process algebras, (), 1-22
[8] Kuntz, M.; Siegle, M.; Werner, E., Symbolic performance and dependability evaluation with the tool CASPA, (), 293-307
[9] K. Lampka. A symbolic approach to the state graph based analysis of high-level Markov reward models. PhD thesis, University of Erlangen-Nuremberg, Erlangen (Germany), 2007
[10] K. Lampka and M. Siegle. Symbolic Composition within the Moebius Framework. In Proc. of the 2nd MMB Workshop, pages 63-74, September 2002. Forschungsbericht der Universität Hamburg Fachbereich Informatik
[11] K. Lampka and M. Siegle. Activity-Local State Graph Generation for High-Level Stochastic Models. In Meassuring, Modelling, and Evaluation of Systems 2006, pages 245-264, April 2006
[12] K. Lampka, M. Siegle, J. Ossowskis, and C. Baier. Partially-shared zero-suppressed Multi-Terminal BDDs: Concept, Algorithms and Applications, 2008. Article submitted for publication, a preliminary version can be downloaded as technical report from; ftp.tik.ee.ethz.ch/pub/publications/TIK-Report-289.pdf
[13] O. Lhoták, S. Curial, and J.N. Amaral. Using ZBDDs in Points-to Analysis. In Proc. of the 20th International Workshop on Languages and Compilers for Parallel Computing, October 2007
[14] Prism · Zbl 1383.05009
[15] Oriol Roig, Jordi Cortadella, and Enric Pastor. Verification of asynchronous circuits by BDD-based model checking of Petri nets. In 16th International Conference on the Application and Theory of Petri Nets, volume 815, pages 374-391, 1995
[16] W.H. Sanders. Construction and solution of performability models based on stochastic activity networks. PhD thesis, University of Michigan, 1988
[17] Shannon, C.S., A symbolic analysis of switching circuits, Transactions AIEE, 57, 713, (1938), Verlag Brinkmann + Bose, The article originally appeared with the title:
[18] Siegle, M., Advances in model representation, (), 1-22, Proc. of the Joint Int. Workshop, PAPM-PROBMIV 2001, Aachen (Germany) · Zbl 1010.68524
[19] Somenzi, F., Binary decision diagrams, Calculational system design, 173, 303-366, (1999) · Zbl 0948.68215
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.