Efficient Symbolic State-Space Construction for Asynchronous Systems
Abstract
Many state of the art techniques for the verification of today's complex embedded systems rely on the analysis of their reachable state spaces. In this paper, we develop a new algorithm for the symbolic generation of the state space of asynchronous system models, such as Petri nets. The algorithm is based on previous work that employs Multi-valued Decision Diagrams (MDDs) for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality which is a fundamental semantic property of asynchronous systems. Additionally, the algorithm supports intelligent cache management and achieves faster convergence via advanced iteration control. It is implemented in the tool SMART, and run time results for several examples taken from the Petri net literature show that the algorithm performs about one order of magnitude faster than the best existing state space generators.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1999
- Accession Number
- ADA371566
Entities
People
- Gerald Luttgen
- Gianfranco Ciardo
- Radu Siminiceanu