[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

Introduction

Maria, or Modular Reachability Analyzer, is a reachability analyzer for Algebraic System Nets. It will generate reachability graphs for Algebraic System Nets, detect deadlocks and check properties expressed using temporal logic formulae.

Maria is remotely based on Prod, a reachability analyzer for Proposition/Transition Nets developed earlier at the Laboratory for Theoretical Computer Science. Its data type system and expression syntax are heavily inspired by the C programming language. In order to understand this manual, you should be familiar with the basic concepts of Petri Nets and also have some knowledge in C.

Maria was written by Marko Mäkelä in a research project at the Helsinki University of Technology in the Laboratory for Theoretical Computer Science. The project is financed by the National Technology Agency of Finland (TEKES), Nokia Research Center, Nokia Networks, the Helsinki Telephone Corporation and the Finnish Rail Administration.

Many of the ideas implemented in Maria were brought up in discussions among the laboratory staff. Ideas expressed by Dr. Kimmo Varpaaniemi, Dr. Nisse Husberg, Keijo Heljanko and Tommi Junttila have influenced the design. Dr. Varpaaniemi sketched the first version of the unification algorithm (see section The Unification Algorithm), and he helped in debugging by stressing the analyzer with quite obscure examples. Also Simo Blom, who was the first one to use the analyzer for something real, reported some bugs, which have now been fixed.

The model-checking functionality (see section Model Checking Algorithms) is based on the ideas of Keijo Heljanko and others, and the algorithms were initially implemented by Timo Latvala.

This edition corresponds to version 1.3.5 of Maria.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by root on December 1, 2016 using texi2html 1.82.