|
Authors: | Kai Lampka |
Group: | Computer Engineering |
Type: | Inproceedings |
Title: | A New Algorithm for Partitioned Symbolic Reachability Analysis |
Year: | 2008 |
Month: | December |
Pub-Key: | Lam08a |
Book Titel: | Proceedings of the Workshop on Reachability Problems |
Volume: | 223 |
Number: | 15 |
Pages: | 137--151 |
Keywords: | Binary Decision Diagrams and algorithms, quantitative verification of systems, symbolic reachability analysis |
Publisher: | Elsevier Science Publishers B. V. |
Abstract: | 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. |
Location: | Amsterdam, The Netherlands |
Resources: | [BibTeX] [ External LINK ] |