Sciweavers

Share
APN
2000
Springer

Efficient Symbolic State-Space Construction for Asynchronous Systems

10 years 3 months ago
Efficient Symbolic State-Space Construction for Asynchronous Systems
Many techniques for the verification of reactive systems rely on the analysis of their reachable state spaces. In this paper, a new algorithm for the symbolic generation of the state spaces of asynchronous system models, such as Petri nets, is developed. The algorithm is based on previous work that employs Multi-valued Decision Diagrams for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality, supports intelligent cache management, and achieves faster convergence via advanced iteration control. The algorithm is implemented in the Petri net tool SMART, and runtime results show that it often performs significantly faster than existing state-space generators.
Gianfranco Ciardo, Gerald Lüttgen, Radu Simin
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where APN
Authors Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu
Comments (0)
books