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 created by the SMV Group at the University of Geneva. It is 100% written in Java and it is 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. AlPiNA provides a user-friendly user interface that was built with the latest metamodeling techniques on the eclipse platform.

 

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.

 

How to cite

Please use the following reference to cite AlPiNA:
 
@article{HML+11,
  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},
  publisher = {IOS Press},
  address = {Amsterdam, The Netherlands, The Netherlands},
  volume = {113},
  number = {3-4},
  month = aug,
  year = {2011},
  issn = {0169-2968},
  numpages = {36},
  pages     = {229-264}
}
Document Actions