AlPiNA : an Algebraic Petri Net Analyzer
Usually, the number of states of concurrent systems grows exponentially in relation to the size of the system. This is called the State Space Explosion. Symbolic Model Checking (SMC) and particularly SMC based on Decision Diagrams (DDs) is a proven technique to handle the State Space Explosion for simple formalisms such as P/T Petri nets.
Algebraic Petri Nets (APN : Petri Nets + Abstract Algebraic Data Types) are powerful tools to model concurrent systems. The State Space Explosion problem is even worse in the case of the APNs than in the P/T nets, mainly because their high expressive power allows end users to model more complex systems. To tackle this problem, AlPiNA uses evolutions of the well known Binary Decision Diagrams (BDDs), such as Data Decision Diagrams, Set Decision Diagrams and Sigma-DDs. It includes some optimizations specific to the APN formalism, such as algebraic clustering and partial algebraic unfolding, to reduce the memory footprint. In short, AlPiNA provides a good balance between user-friendliness, modeling expressivity and computational performances.