| Popis: |
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. |
