AlPiNA : an Algebraic Petri Net Analyzer
Our goal is to provide a user friendly suite of tools for checking models based of the Algebraic Petri Net formalism. In order to provide great user experience, we leverage on the powerful eclipse platform.
Algebraic Petri Nets (APN : Petri Nets + Abstract Algebraic Data Types) are powerful tools to model concurrent systems. Usually, concurrents systems take very large sets of states, that grow very fast in relation to the system size. This problem, called the State Space Explosion, is even worse in the APN case than in the P/T nets case, mainly because their high expressive power allows end users to model more complex systems. Symbolic Model Checking (SMC) and particularly Decision Diagrams (DD) based SMC is a proven technique to handle the State Space Explosion for simpler formalisms such as P/T Petri Nets.
AlPiNA uses Binary Decision Diagrams' (BDD) evolutions (Data Decision Diagrams, Set Decision Diagrams, Sigma-DD) to tackle aforementioned problem in the APN world. It also allows to specify both algebraic and topological clusters to groups states together and thus to reduce the memory footprint.