printlogo
ETH Zuerich - Homepage
Computer Engineering and Networks Laboratory (TIK)
 
ETH Zurich - ITET - TIK - Publications
print
  

Publication Details for Inproceedings "A New Algorithm for Partitioned Symbolic Reachability Analysis"

 

 Back

 New Search

 

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 ]

 

 Back

 New Search

top
© 2019 Laboratory TIK, ETH Zurich | Imprint | Last updated on Wed, 16 May, 2018 17:35 | t=0.0041s | Valid HTML 4.01