Maria performs simulation, exhaustive reachability analysis and on-the-fly LTL model checking of high-level Petri nets with
fairness constraints. The algebra contains powerful built-in data types and operations. Models can be exported to low-level
Petri nets and labelled transition systems. Translator programs allow Maria to analyse transition systems as well as distributed
computer programs written in procedural or object-oriented languages, or high-level specifications such as SDL. Maria has
been implemented in portable C and C++, and it is freely available under the conditions of the GNU General Public License.
This research was financed by the Helsinki Graduate School on Computer Science and Engineering, the National Technology Agency
of Finland (TEKES), the Nokia Corporation, Elisa Communications, the Finnish Rail Administration, EKE Electronics and Genera,
and by a personal grant from Tekniikan Edistämissäätiö.