UNIGE document Scientific Article
previous document  unige:12332  next document
add to browser collection

Toward efficient state space generation of algebraic Petri nets

Published in SMV technical report series. 2010, no. 206
Abstract Algebraic Petri Nets (APN: Petri Nets + Abstract Algebraic Data Types) are powerful tools to model concurrent systems. Because of their high expressive power, allowing end-user to model more complex systems, State Space Explo- sion is a big issue in APN. Symbolic Model Checking (SMC) and particularly Decision Diagrams (DD) based symbolic model checking is a proven technique to handle the State Space Explosion for simpler formalisms such as P/T Petri Nets. This paper discusses how to use Binary Decision Diagrams' (BDD) evo- lutions (Data Decision Diagrams, Set Decision Diagrams, Σ DD,... ) to tackle aforementioned problem in the APN world. The main contributions of this work are the encoding of any APN model using the DD framework and the notion of Algebraic Cluster that tackles the concurrency induced by the token multiplic- ity. The discussed algorithms have been implemented in a tool that is freely accessible on http://alpina.unige.ch.
Keywords System design and verificationHigher-level Nets ModelsAlgebraic Petri NetsState Space GenerationDecisions Diagrams
Full text
Article (Preprint) (2.5 MB) - public document Free access
(ISO format)
BUCHS, Didier, HOSTETTLER, Steve Patrick. Toward efficient state space generation of algebraic Petri nets. In: SMV technical report series, 2010, n° 206. https://archive-ouverte.unige.ch/unige:12332

338 hits



Deposited on : 2010-11-05

Export document
Format :
Citation style :