Entry last updated: 2010/3/5
Entry last validated: 2010/3/5

Tool homepage:

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology) Components (see also help on terminology)


Tool Description

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.

AlPiNA is implemented as an Eclipse plugin. The user interface was created using the EMP metamodeling approach. Thus, models are easy to implement, without the need to know the underlying techniques related to model checking performance.

The actual model checking is performed in an independent engine, implemented in Java. 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. This allows to check models with very large state spaces.

Contact Information

Prof. Didier Buchs
Computer Science Department
University of Geneva
7 route de Drize, Bt. A, 
CH-1227 Carouge 

Phone:  0041 22 37 90 161
Fax:    0041 22 37 90 250

Other Remarks

This program is free software, it can be redistributed and/or modified under the terms of the GNU General Public License.
[PN Home][*]
The maintainers of this page