zbMATH — the first resource for mathematics

Computing a hierarchical static order for decision diagram-based representation from P/T nets. (English) Zbl 1350.68202
Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency V. Berlin: Springer (ISBN 978-3-642-29071-8/pbk). Lecture Notes in Computer Science 6900. Journal Subline, 121-140 (2012).
Summary: State space generation suffers from the typical combinatorial explosion problem when dealing with industrial specifications. In particular, memory consumption while storing the state space must be tackled to verify safety properties. Decision Diagrams are a way to tackle this problem. However, their performance strongly rely on the way variables encode a system. Another way to fight combinatorial explosion is to hierarchically encode the state space of a system.
This paper presents how we mix the two techniques via the hierarchization of a precomputed variable order. This way we obtain a hierarchical static order for the variables encoding a system. This heuristic was implemented and exhibits good performance.
For the entire collection see [Zbl 1238.68015].
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI