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.

• Type: Conference
• Year: 2000
• Where: APN
• Authors: Gianfranco Ciardo, Gerald Lüttgen, Radu Siminiceanu
• Keywords: APN 2000, Artificial Intelligence, Petri Net, Reachable States, State Spaces