Entry last updated: 2004/5/17
Entry last validated: 2004/5/17

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

Maria is a reachability analyzer and a model checker whose modelling formalism is based on Algebraic System Nets, capable of handling tens of millions of reachable states and enabled transitions.

Maria includes a distributed algorithm for checking safety properties. The algorithm can be executed on multi-processor computers as well as on workstations in TCP/IP networks.

Optionally, nets can be unfolded or translated to transition systems.

Thanks to its modular design and open source license (GPL), Maria can easily be extended with new algorithms.

Contact Information

Marko M„kel„
Timo Latvala
Laboratory for Theoretical Computer Science
P.O.Box 5400
02015 Helsinki University of Technology

Phone:  +358 - 9 - 451 2895
Fax:    +358 - 9 - 451 3369

Other Remarks

Maria is efficient both in interactive use and in exhaustive reachability analysis, as it can both interpret models directly and compile them to fast C code.

The graphical user interface of Maria is based on GraphViz.

[PN Home][*]
The maintainers of this page