Abstract
AlPiNA is a graphical editor and model checker for a class of high-level Petri nets called Algebraic Petri Nets. Its main purpose is to perform reachability checks on complex models. It performs symbolic model checking based on ΣDD, an efficient evolution in the Decision Diagrams field, using novel techniques such as algebraic clustering and algebraic unfolding. AlPiNA offers a user-friendly interface, and is easily extensible.
This project was partially funded by the COMEDIA project of the Hasler foundation, ManCom initiative project number 2107.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. Transactions on Computers C-35, 677–691 (1986)
Buchs, D., Hostettler, S.: Managing complexity in model checking with decision diagrams for algebraic petri net. In: Moldt, D. (ed.) Pre-proceedings of the International Workshop on Petri Nets and Software Engineering, pp. 255–271 (2009), http://smv.unige.ch/publications/pdfs/pnse09.pdf
Buchs, D., Hostettler, S.: Sigma Decision Diagrams: Toward efficient rewriting of sets of terms. In: Corradini, A. (ed.) TERMGRAPH 2009: Preliminary proceedings of the 5th International Workshop on Computing with Terms and Graphs, number TR-09-05 in TERMGRAPH workshops, Università di Pisa, pp. 18–32 (2009), http://smv.unige.ch/publications/pdfs/termgraph09.pdf
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Ciardo, G., Lüttgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)
Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005)
CPN Group. CPN tools, http://wiki.daimi.au.dk/cpntools/cpntools.wiki
Eclipse. Eclipse modeling project, http://www.eclipse.org/modeling/
Hamez, A., Thierry-Mieg, Y., Kordon, F.: Hierarchical set decision diagrams and automatic saturation. In: Petri Nets, pp. 211–230 (2008)
Mäkelä, M.: Modular reachability analyzer, http://www.tcs.hut.fi/Software/maria/
Pajault, C., Evangelista, S.: High level net analyzer, http://helena.cnam.fr/
Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, London, UK, pp. 429–528. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buchs, D., Hostettler, S., Marechal, A., Risoldi, M. (2010). AlPiNA: An Algebraic Petri Net Analyzer. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)