Personal tools
You are here: Home
 

AlPiNA : an Algebraic Petri Net Analyzer

logo_cow

AlPiNA stands for Algebraic Petri Nets Analyzer and is a model checker for Algebraic Petri Nets. It has been developped by the SMV Group and is 100% written in Java and available under the terms of the GNU general public license.

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.
 

How to cite

Please use the following reference to cite AlPiNA:
 
@article{HMLRB2011,
  author    = {Steve Hostettler and
               Alexis Marechal and
               Alban Linard and
               Matteo Risoldi and
               Didier Buchs},
  title     = {High-Level Petri Net Model Checking with AlPiNA},
  journal = {Fundamenta Informaticae},
  volume    = {113},
  number    = {3-4},
  year      = {2011},
  pages     = {229-264},
  ee        = {http://dx.doi.org/10.3233/FI-2011-608}
}
Document Actions