OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Hierarchical Set Decision Diagrams and Regular Models

Thierry-Mieg, Yann and Poitrenaud, Denis and Hamez, Alexandre and Kordon, Fabrice Hierarchical Set Decision Diagrams and Regular Models. (2009) In: Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. (Lecture Notes in Computer Science). Springer, Berlin, 1-15. ISBN 978-3-642-00767-5

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://link.springer.com/chapter/10.1007%2F978-3-642-00768-2_1


This paper presents algorithms and data structures that exploit a compositional and hierarchical specification to enable more efficient symbolic model-checking. We encode the state space and transition relation using hierarchical Set Decision Diagrams (SDD) [9]. In SDD, arcs of the structure are labeled with sets, themselves stored as SDD. To exploit the hierarchy of SDD, a structured model representation is needed. We thus introduce a formalism integrating a simple notion of type and instance. Complex composite behaviors are obtained using a synchronization mechanism borrowed from process calculi. Using this relatively general framework, we investigate how to capture similarities in regular and concurrent models. Experimental results are presented, showing that this approach can outperform in time and memory previous work in this area.

Item Type:Book Section
Additional Information:Thanks to Springer editor. The definitive version is available at http://link.springer.com/chapter/10.1007%2F978-3-642-00768-2_1
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Other partners > Université Pierre et Marie Curie, Paris 6 - UPMC (FRANCE)
Laboratory name:
Deposited On:27 Feb 2015 16:24

Repository Staff Only: item control page