 |
|
|||
| 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 ] |
