Petri Nets

A Petri net is a mathematical modeling language particularly adapted to the description of distributed systems. It is a directed bipartite graph, in which the nodes represent transitions (i.e. events that may occur, represented by rectangles or bars) and places (i.e. conditions, represented by circles or ellipses). The directed arcs describe which places are pre and/or postconditions for which transitions.

Petri Nets were first defined by the German mathematician Carl Adam Petri.

There are numerous Petri net dialects and CosyVerif handles several of them:

  • P/T nets,
  • Symmetric nets, a subclass of colored nets,
  • Symmetric nets withs bags, an extension of Symmetric nets.

The pages of this section present the formalism itself, some illustrating examples, as well as the services for the verification of Petri nets available in CosyVerif.

Available services for Petri nets

So far, the following services are available in (full bundle or Petri Net Bundle):

  • Behavioral Analysis:
    • Model Checking with PROD (Univ. Helsinki),
    • Model Cheking with PNXDD (Univ. P. & M. Curie, LIP6),
    • Model Checking with Crocodile (Univ. P. & M. Curie, LIP6),
    • Cunf (ENS de Cachan, LSV),
  • Stochastic Analysis:
    • Statistical Model Checking with Cosmos (ENS de Cachan, LSV),
  • Structural Analysis:
    • Computation of Place/Transition Invariants with GreatSPN (Univ. Torino),
    • Computation of Structural Bounds (Univ. P. & M. Curie, LIP6),
  • Import/Exports:
    • Unfolder of Symmetric Nets into P/T Nets (Univ. P. & M. Curie, LIP6),
    • Export into the P/T GreatSPN format (Univ. P. & M. Curie, LIP6),

Please note that all services may not be documented (see the list in the table of content aside this page). However, the use of services by means of the user interface is quite intuitive so users aware of Petri nets should be able to cope with this lack 😉

Some references