The Azimuth Project
Petri net

Contents

Idea

A Petri net is a kind of diagram for describing processes that arise in systems with many components, known as distributed systems. They were invented in 1939 by Carl Adam Petri — when he was 13 years old — in order to describe chemical reactions. They are a widely used model of concurrency in theoretical computer science. They are also used to describe chemical reactions in molecular biology, interactions between organisms (e.g. predation, death, and birth), manufacturing processes, supply chains, and so on. They can be seen as part of a broader subject called network theory.

Chemical reaction networks look different from Petri nets, but it is easy to translate between the two, so they are actually equivalent formalisms. Both Petri nets and chemical reaction networks have been extensively discussed in a series of articles on the Azimuth Blog, which is best accessed starting here:

This article here is a brief summary.

A chemical process example

Here is an example of a Petri net taken from chemistry:

basic chemical Petri net

The circles in a Petri net denote so-called states, which in this example are chemical compounds. The boxes denote transitions, which in this example are chemical reaction. Every transition has a finite set of input states, with wires coming in from them, and a finite set of output states, with wires going out. All this information can equally well be captured by the usual notation for chemical reactions, as follows:

C + O2 \to CO2

CO2 + NaOH \to NaHCO3

NaHCO3 + HCl \to H2O + NaCl + CO2

One advantage of Petri nets is that we can also label each state by some number (0,1,2,3,…) of black dots, called tokens. In our example, each token represents a molecule of a given kind. Thus

chem net dots 1

describes a situation where one atom of carbon, one molecule of oxygen, one molecule of sodium hydroxide and one molecule of hydrochloric acid are present. No molecules of CO2, NaHCO3, H2O or HCl are present at this time.

We can then describe processes that occur with the passage of time by moving the tokens around. If the carbon reacts with oxygen we obtain:

chem net dots 2

If the carbon dioxide combines with the sodium hydroxide to form sodium bicarbonate, we obtain:

chem net dots 3

If the sodium bicarbonate and hydrochloric acid react, we then obtain:

chem net dots 4

Note that in each case the following rule holds: for any given transition, we can delete one token for each of its input states and simultaneously add one token for each of its output states.

Here is a simpler example, taken from this article:

Here the transitions are denoted by black rectangles. This example is somewhat degenerate, because there no transitions with more than one input or more than one output. However, it illustrates the possibility of having more than one token in a given state. It also illustrates the possibility of a transition with no inputs, or no outputs. In chemistry this is useful for modelling a process where molecules of a given sort are added to or removed from the environment.

Category-theoretic interpretation

If we ignore the tokens, a Petri net is a way of specifying a free strict symmetric monoidal category by giving a set of objects x 1,,x nx_1, \dots, x_n and a set of morphisms between tensor products of these objects, for example:

f 1:x 1x 1x 1 f_1 : x_1 \to x_1 \otimes x_1
f 2:x 1x 2x 2x 2 f_2 : x_1 \otimes x_2 \to x_2 \otimes x_2
f 2:x 21 f_2 : x_2 \to 1

Here 11 denotes the tensor product of no objects.

In applications, the objects might be molecules and the morphisms might be chemical reactions; in this case the tensor product symbol is written ‘++’ rather than ‘\otimes’.

For more on this, see:

Here Sassone describes a category of Petri nets and sketches the description of a functor from that category to the category of strict symmetric monoidal categories. Sassone also has some other papers on Petri nets and category theory.

Stochastic Petri net

In a stochastic Petri net, each morphism is labelled by a nonnegative number, which can be thought of as determining a ‘reaction rate’. See for example:

The following book gives a particularly readable introduction to stochastic Petri nets, with applications to the Lotka-Volterra equations describing predator-prey interactions, and also to gene expression:

  • Darren James Wilkinson, Stochastic Modelling for Systems Biology, Taylor & Francis, New York, 2006.

The basic idea here is very simple. Consider, for example, the following Petri net:

fox+rabbits Petri net

If we use x 1x_1 to denote “rabbit” and x 2x_2 to denote “fox”, the transitions are:

birth:x 1x 1x 1 birth : x_1 \to x_1 \otimes x_1

in which one rabbit becomes two,

predation:x 1x 2x 2x 2 predation : x_1 \otimes x_2 \to x_2 \otimes x_2

in which a fox eats a rabbit and reproduces, resulting in two foxes, and

death:x 21 death : x_2 \to 1

in which one fox dies. Of course this model is ridiculous — it would be slightly less silly if we replaced ‘fox’ and ‘rabbit’ by asexual micro-organisms, one predator and the other prey. But our goal here is not to give a realistic example, merely a simple and memorable one.

If we specify a nonnegative real constant for each transition in a Petri net, we get a stochastic Petri net. In chemistry these constants are called reaction rates, and there is a systematic procedure to obtain a set of differential equations from a stochastic Petri net. Just for fun, let us explain this procedure in terms of the rabbit and fox example above. Suppose:

  • α\alpha is the birth rate,

  • β\beta is the predation rate, and

  • γ\gamma is the death rate

Let [x 1][x_1] denote the concentration of rabbits (say, in rabbits per hectare) and let [x 2][x_2] the concentration of foxes as a function of time. Then following the standard procedure in chemistry, we would get these equations:

(1)d[x 1]dt=α[x 1]β[x 1][x 2] \frac{d [x_1]}{ d t} = \alpha [x_1] - \beta [x_1] [x_2]
(2)d[x 2]dt=+β[x 1][x 2]γ[x 2] \frac{d [x_2]}{ d t} = + \beta [x_1] [x_2] - \gamma [x_2]

The standard procedure works as follows:

  • The rate at which any transition occurs equals its reaction rate times the product of the concentrations of its inputs.

  • The time derivative of any concentration [x i][x_i] is given by a sum over all transitions.

  • Each transition contributes to the time derivative of [x i][x_i] in the obvious way: we take the rate at which that transition occurs, and multiply it by the number of times x ix_i occurs as an output of that transition, minus the number of copies times it occurs as an input.

Equations (1) and (2) are a special case of the Lotka-Volterra equations. In quantitative ecology, the Lotka-Volterra equations are often used as a simple model of predator-prey systems. However, the systematic procedure we have described for turning stochastic Petri nets into systems of differential equations is less appropriate for ecology than for chemistry. There are many reasons why. Here are some of the simplest:

  • Molecules move in a more or less random way, so the chance that molecules of two different kinds will collide is close to proportional to the product of their concentrations. This is not true with animals. Rabbits don’t randomly hop about and mate when they collide: they actively seek out sex partners. Similarly, foxes actively hunt rabbits.

  • There is a ‘saturation’ effect which prevents the reaction rate from being proportional to the product of the concentrations of its inputs when some of these concentrations are much larger than others. For example, a fox doesn’t really eat rabbits at a rate proportional to the concentration of rabbits: if you’ve got one fox and a million rabbits in a limited area, you probably won’t double the rate at which the fox eats rabbits by doubling the number of rabbits!

  • Similarly, the fact that animals come in discrete quantities (0,1,2,3,0,1,2,3,\dots) makes the continuum approximation inappropriate at very low concentrations. This is sometimes jokingly called the attowolf problem: if our model predicts the existence of 10 1810^{-18} of a wolf, we should not expect wolves to survive, even if the model predicts that their numbers rise later.

Chemical reaction network

Petri nets are different from, but entirely equivalent to, chemical reaction networks. Chemical reaction networks are widely used in chemistry, and they look like this:

chemical reaction network

A chemical reaction network shows a collection of different molecular species (types of molecules). For example, in the above diagram taken from Feinberg’s lectures below, A,BA, B and CC are three molecular species, and we have four reactions between them:

A+AB A + A \to B
CA+A C \to A + A
BC B \to C
CBC \to B

which can occur at various rates. After specifying the reaction rates, we obtain an ordinary differential equation describing the time evolution of the concentration of the various molecular species. We can infer some qualitative properties of the solutions of this equation just from the picture of the reaction network.

For details, start with:

and then try:

The last is apparently not free online, but here’s a quote that explains the philosophy:

A physical chemist usually consider electrons atoms, molecules and their interaction as primitive notions, and is interested in studying the mechanism of rearrangement of atoms into new molecules during chemical reactions. He may also explore what inferences may be drawn regarding reaction rates, possibly with the assistance of statistical mechanics.

The formal kineticist, on the other hand, takes a macroscopic viewpoint and his primitive concept is the elementary reaction. This is defined by a set of stoichiometric coefficients, together with a rule relating reaction rate to composition and temperature. The primary macroscopic observable is the rate of change of composition of the mixture, and an expression for this is constructed by adding the rates of elementary reactions, each weighted by the corresponding set of stoichiometric coefficients. The elementary reactions thus provide a framework for constructing differential equations to be satisfied by the composition.

The abstract is also useful:

Abstract: The familiar idea of mass action kinetics is extended to embrace situations more general than chemically reacting mixtures in closed vessels. Thus, for example, many reaction regions connected by convective or diffusive mass transport, such as the cellular aggregates of biological tissue, are drawn into a common mathematical scheme. The ideas of chemical thermodynamics, such as the algebraic nature of the equilibrium conditions and the decreasing property of the free energy, are also generalized in a natural way, and it is then possible to identify classes of generalized kinetic expressions which ensure consistency with the extended thermodynamic conditions. The principal result of this work shows that there exists a simply identifiable class of kinetic expressions, including the familiar detailed balanced kinetics as a proper subclass, which ensure consistency with the extended thermodynamic conditions. For kinetics of this class, which we call complex balanced kinetics, exotic behavior such as bistability and oscillation is precluded, so the domain of search for kinetic expressions with this type of behavior, which is of considerable biological interest, is greatly narrowed. It is also shown that the ideas of complex balancing and of detailed balancing are closely related to symmetry under time reversal.

This paper says that a fundamental reference on stochastic network analysis is:

  • B.L. Clarke and I. Prigogine, Stability of complex reaction networks, Adv. Chem. Phys., Wiley, New York, 43 (1980), 1–-216.

Bistability

When we go beyond the case of reaction networks with deficiency zero, we meet more interesting behaviors in the rate equation, which can be important in biochemistry. Examples include periodic solutions, which can serve as ‘biological clocks’, or multiple stable equilibria in the same stoichiometric subspace, which can serve as ‘switches’ in living organisms. The latter phenomenon is called ‘bistability’.

For bistability, see for example:

Here’s the abstract:

Abstract: Abstract bifurcation theory is one of the most widely used approaches for analysis of dynamical behaviour of chemical and biochemical reaction networks. Some of the interesting qualitative behaviour that are analyzed are oscillations and bistability (a situation where a system has at least two coexisting stable equilibria). Both phenomena have been identified as central features of many biological and biochemical systems. This paper, using the theory of stoichiometric network analysis (SNA) and notions from algebraic geometry, presents sufficient conditions for a reaction network to display bifurcations associated with these phenomena. The advantage of these conditions is that they impose fewer algebraic conditions on model parameters than conditions associated with standard bifurcation theorems. To derive the new conditions, a coordinate transformation will be made that will guarantee the existence of branches of positive equilibria in the system. This is particularly useful in mathematical biology, where only positive variable values are considered to be meaningful. The first part of the paper will be an extended introduction to SNA and algebraic geometry-related methods which are used in the coordinate transformation and set up of the theorems. In the second part of the paper we will focus on the derivation of bifurcation conditions using SNA and algebraic geometry. Conditions will be derived for three bifurcations: the saddle-node bifurcation, a simple branching point, both linked to bistability, and a simple Hopf bifurcation. The latter is linked to oscillatory behaviour. The conditions derived are sufficient and they extend earlier results from stoichiometric network analysis as can be found in (Aguda and Clarke in J Chem Phys 87:3461–3470, 1987; Clarke and Jiang in J Chem Phys 99:4464–4476, 1993; Gatermann et al. in J Symb Comput 40:1361–1382, 2005). In these papers some necessary conditions for two of these bifurcations were given. A set of examples will illustrate that algebraic conditions arising from given sufficient bifurcation conditions are not more difficult to interpret nor harder to calculate than those arising from necessary bifurcation conditions. Hence an increasing amount of information is gained at no extra computational cost. The theory can also be used in a second step for a systematic bifurcation analysis of larger reaction networks.

For oscillations, see:

Toric geometry

There is an interesting relation between chemical reaction networks (or, better, Petri nets) and toric varieties. See:

and also the paper by Mirela Domijan and Markus Kirkilionis cited above.

References

Some good online introduction include:

These are some introductory books:

  • James Lyle Peterson, Petri Net Theory and the Modelling of Systems, Prentice Hall, 1981.

  • D. Kartson, G. Balbo, G. Conte, S. Donatelli and G. Franceschinis, Modelling with Generalized Stochastic Petri Nets, Wiley, 1994.

  • W. Reisig and G. Rozenberg, eds., Lectures on Petri Nets, two volumes, Springer, Berlin, 1998. (I haven’t looked through this yet!)

These are some important introductory papers:

For applications to biology, see:

For applications of Petri nets to ecology, see this nice list of references, which is on a website devoted to the life and work of Bland Ewing:

Also see:

For Petri nets and other models of concurrency in computer science, try:

  • G. Winskel and M. Nielsen, Models for Concurrency, Handbook of Logic and the Foundations of Computer Science, vol. 4, Oxford U. Press, Oxford, pp. 1-148.

Apparently this paper is important reference on stability for reaction networks:

  • B.L. Clarke and I. Prigogine, Stability of complex reaction networks, Adv. Chem. Phys., Wiley, New York, 43 (1980), 1–-216.

There is an interesting relation between reaction networks (or Petri nets) and toric varieties. See:

On the category theory of Petri nets:

Software Reviews

Duggan, J., A Comparison of Petri Net and System Dynamics Approaches for Modelling Dynamic Feedback Systems

More references

Interesting papers:

Software

Petri Net Software

CPN Tools

CPN Tools is probably the most popular tool for editing, simulating, and analyzing Coloured Petri nets.

It has been developed over the past 25 years.

The tool features incremental syntax checking and code generation, which take place while a net is being constructed. A fast simulator efficiently handles untimed and timed nets. Full and partial state spaces can be generated and analyzed, and a standard state space report contains information, such as boundedness properties and liveness properties.

Dependencies
  • Milton

Snoopy

Snoopy is a software tool to design and animate hierarchical graphs, among others Petri nets. The tool has been developed - and is still under development - at the University of Technology in Cottbus, Dep. of Computer Science, ”Data Structures and Software Dependability“.

The tool is in use for the verification of technical systems, especially software-based systems, as well as for the validation of natural systems, i.e. biochemical networks as metabolic, signal transduction, gene regulatory networks, compare poster “overview on the research activities of our working group”.“

Basic Properties
  • extensible
  • generic design facilitates add on of new graph types
  • adaptive
  • simultaneous use of several graph types
  • GUI adopts dynamically to graph type in active window
  • platform independent
Main Features
  • hierarchies by subgraphs
  • logical (fusion) nodes
  • different shapes for net elements
  • colouring of graph elements (e.g. paths or invariants)
  • automated layout by Graphviz library
  • digital signature by md5 hash function
  • animation of place/transition Petri nets
  • simulation of stochastic/continuous Petri nets
  • printing support: eps, Xfig, FrameMaker
  • import/export from/to analysis tools, see related software
  • SBML import/export (rules, events, functions not supported)
  • support of web-based Petri net animation, see sampler
Availability
  • Windows
  • OS X
  • Debian varieties of Linux.
Dependencies
  • Javascript
  • C++
  • wxWidgets
  • Xerces

Abstract Petri Net Notation (APNN)

ADAM

Analysis of Dynamic Algebraic Models.

Charlie

Helena

Dependencies
References

Abstract

In this paper we advocate a unifying technique for description of Petri net semantics. Semantics, i.e. a possible behaviour, is basically a set of node-labelled and arc-labelled directed acyclic graphs, called token flows, where the graphs are distinguished up to isomorphism. The nodes of a token flow represent occurrences of transitions of the underlying net, so they are labelled by transitions. Arcs are labelled by multisets of places.

Namely, an arc between an occurrence x of a transition a and an occurrence y of a transition b is labelled by a multiset of places, saying how many tokens produced by the occurrence x of the transition a is consumed by the occurrence y of the transition b. The variants of Petri net behaviour are given by different interpretation of arcs and different structure of token flows, resulting in different sets of labelled directed acyclic graphs accepted by the net.

We show that the most prominent semantics of Petri nets, namely processes of Goltz and Reisig, partial languages of Petri nets introduced by Grabowski, rewriting terms of Meseguer and Montanari, step sequences as well as classical occurrence (firing) sequences correspond to different subsets of token flows.

Finally, we discuss several results achieved using token flows during the last four years, including polynomial test for the acceptance of a partial word by a Petri net, synthesis of Petri nets from partial languages and token flow unfolding.

Abstract

Reaction systems are a formal model for processes inspired by the functioning of the living cell.The underlying idea of this model is that the functioning of the living cell is determined by the interactions of biochemical reactions, and these interactions are based on the mechanisms of facilitation and inhibition. In this paper we first review the main notions of the basic model of reaction systems which is a qualitative model.Then we discuss various ways of taking into account quantitative properties.

Abstract

Communication structured occurrence nets (CSON) are an extension of occurrence nets. They can be used to represent the execution behaviours of complex evolving systems. Communication structured place transition nets (CSPT-nets) provide a system-level model for describing the interaction between different systems, and CSONs can model individual runs of CSPT-nets. I

n this paper, we investigate branching processes of CSPT-nets which provide a complete information about their behaviours. We also outline an algorithm for the construction of unfoldings of CSPT-nets.

CSONs are acyclic and conflict-free.

INA

Integrated Net Analyzer

Marcie

Model checking And Reachability analysis done effiCIEntly.

{}

GreatSPN

“GreatSPN is a suite of tools for the design and analysis (qualitative and quantitative) of Generalized Stochastic Petri Nets and Stochastic Well-formed nets. First released by the University of Torino in the late 1980’s, GreatSPN has been a widely used tool in the research community since it provides a breadth of solvers for computing net structural properties, the set of Reachable States (RS), the Reachability Graph (RG) with and without symmetry exploitation, and performance evaluation indices using both simulation and numerical solution for steady state and transient measures.

Over the years, GreatSPN functionality has been extended, also thanks to the collaboration with University of Paris 6 and the Universit`a del Piemonte Orientale, by improving and enhancing its solution algorithms, and by providing new solution methods for new formalisms and property languages defined over the years.

The latest enhancements include:

  • Model checking. A Computational Tree Logic (CTL) model checker for Petri nets with priorities and a CSL-TA stochastic model checker for SPN. The CTL model checker implementation is based on the Meedly library from University of Iowa
  • Optimization problem analyzer. Integration of the Markov Decision Well-formed Net formalism and associated solution algorithms, which allow the study of optimization problems based on Discrete Time Markov Decision Process.
  • Fluidification analysis. The addition of the PN2ODE module, which allows to automatically derive from an SPN model a corresponding set of ODEs (in Matlab format), whose solution provides the expected values of the performance indices, as a function of time.
  • Dynamic SRG and Extended SRG. The algorithms for the construction of the Symbolic RG have been extended to include Dynamic SRG and Extended SRG construction, two non trivial extensions of the SRG construction which can provide a reduction of the state space size in case of partially symmetrical SWN models.“
References
  • S. Baarir, M. Beccuti, D. Cerotti, M. D. Pierro, S. Donatelli, and G. Franceschinis. The greatspn tool: recent enhancements. SIGMETRICS Performance Evaluation Review, 36(4):4-9, 2009.
  • J. Babar, M. Beccuti, S. Donatelli, and A. S. Miner. Greatspn enhanced with decision diagram data structures. In Proc. of 31st International Conference, volume 6128 of Lecture Notes in Computer Science. Springer, pages 308-317, 2010.

ITS-Tools

  • Univ. Pierre & Marie Curie, France

ITS-tools is a suite of model-checking tools, developed in the team MoVe at LIP6. Written in C++, it is available under the terms of the GNU General Public Licence.

It features state-space generation, reachability analysis, LTL and CTL checking. ITS-tools accept a wide range of inputs: (Time) Petri Nets, ETF (produced by the tool LTSmin), DVE (input format to the tool DiVinE, used in the BEEM database), and a dedicated C-like format known as GAL. The input models can also be given as compiled object files. This allows for large possibilities of interaction with other tools.

Models, even in different formats, can also be easily composed, through the formalism of Instantiable Transition Systems (ITS) [Itstools3]. This ease the modeling process. ITS-tools also features a graphical interface, as an Eclipse plug-in, to further help the modeler, especially with compositions.

As for the back-end, ITS-tools rely on decision diagrams [Itstools1] to handle efficiently the combinatorial explosion of the state space. The decision diagrams manipulation is performed by the libDDD library, that features several mechanisms for the efficient manipulation of decision diagrams [Itstools2,Itstools4]. References

  • Hierarchical decision diagrams to exploit model structure, J. M. Couvreur and Y. Thierry-Mieg, Formal Techniques for Networked and Distributed Systems-FORTE 2005 443-457 (2005)
  • Hierarchical set decision diagrams and automatic saturation, A. Hamez and Y. Thierry-Mieg and F. Kordon, Applications and Theory of Petri Nets 211-230 (2008)
  • Hierarchical set decision diagrams and regular models, Y. Thierry-Mieg and D. Poitrenaud and A. Hamez and F. Kordon, Tools and Algorithms for the Construction and Analysis of Systems 5505 1-15 (2009)
  • Towards Distributed Software Model-Checking using Decision Diagrams, M. Colange and S. Baarir and F. Kordon and Y. Thierry-Mieg, Computer Aided Verification, to appear (2013)

LoLA

  • Univ. Rostock, Germany

“LoLA [Lola1] provides explicit state space verification for place/transition nets. It supports various simple properties. For the contest, mainly the reachability verification features are used.

LoLA offers several techniques for alleviating state explosion, including various stubborn set methods, symmetries (which it can determine fully automated), the sweep-line method (where it computes its own progress measure), bloom filters, and linear algebraic compressions. To our best knowledge, LoLA is the only tool worldwide that provides this large number of explicit state space techniques in this high degree of automaton, and with these possibilities for joint application.

In the MCC, we neither use symmetries nor the sweep-line method. For these methods, performance is too volatile for the black box scenario implemented in the MCC.

NOTE: associated to he main version, three variants (described below) were provided.“

References
  • K. Wolf. Generating Petri net state spaces. In J. Kleijn and A. Yakovlev, editors, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency (ICATPN), June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 29-42. Springer-Verlag, June 2007. Invited lecture

Variant: lola_optimistic

This variant uses a goal oriented stubborn set method and linear algebraic state compression. Goal oriented stubborn sets perform best on reachability queries that are ultimately satisfied in the net under investigation. A heuristics takes care that a satisfying state is reached with high probability already in very early stages of state space exploration. This way, only a tiny portion of the state space is actually explored. If the satisfying states are missed, however, or no satisfying state is reachable, a significantly larger state space is produced than the one produced by lola-pessimistic. Witness paths tend to be very small. Variant: lola_optimistic_incomplete

In addition to lola-optimistic, we use a bloom filter for internal representation of states. That is, only the hash value of a state is marked in several hash tables, each belonging to an independent hash function. The state itself is not stored at all. This way, we can handle a larger number of states within a given amount of memory. In the rare case of a hash collision, the colliding state is not explored, so parts of the state space may be missed and false negative results are possible.

The user can specify the number of hash tables to be used and thus control the probability of hash collisions. Variant: lola_pessimistic

This variant computes stubborn sets using a standard deletion algorithm. Deletion algorithms are much slower than goal-oriented stubborn sets (quadratic instead of linear) but yield better reduction. This better reduction pays off when the whole state space needs to be explored (i.e. there are no reachable satisfying states). If reachable states exist, this variant is outperformed by the optimistic variant since it has no goal-orienting heuristics and tends to miss reachable states in early phases of state space exploration.

Witness paths are often much longer than in the optimistic variant.

MARCIE

  • Univ. Cottbus, Germany

MARCIE [Marcie1] is a tool for the analysis of Generalized Stochastic Petri Nets, supporting qualitative and quantitative analyses including model checking facilities. Particular features are symbolic state space analysis including efficient saturation-based state space generation, evaluation of standard Petri net properties as well as CTL model checking.

Most of MARCIE’s features are realized on top of an Interval Decision Diagram (IDD) implementation [Marcie4]. IDDs are used to efficiently encode interval logic functions representing marking sets of bounded Petri nets. This allows to efficiently support qualitative state space based analysis techniques [Marcie3]. Further, MARCIE applies heuristics for the computation of static variable orders to achieve small DD representations.

For quantitative analysis MARCIE implements a multi-threaded on-the-fly computation of the underlying CTMC [Marcie2]. It is thus less sensitive to the number of distinct rate values than approaches based on, e.g., Multi-Terminal Decision Diagrams. Further it offers symbolic CSRL model checking and permits to compute reward expectations. Additionally MARCIE provides simulative and explicit approximative numerical analysis techniques. References

  • M. Heiner, C. Rohr, and M. Schwarick. MARCIE - Model checking And Reachability analysis done effiCIEntly. In J. Colom and J. Desel, editors, Proc. PETRI NETS 2013, volume 7927 of LNCS, pages 389-399. Springer, June 2013.
  • M. Schwarick, C. Rohr, and M. Heiner. MARCIE - Model checking And Reachability analysis done effiCIEntly. In Proc. 8th International Conference on Quantitative Evaluation of SysTems (QEST 2011), pages 91 - 100. IEEE CS Press, September 2011.
  • M. Schwarick and A. Tovchigrechko. IDD-based model validation of biochemical networks. TCS 412, pages 2884-2908, 2010.
  • A. Tovchigrechko. Model Checking Using Interval Decision Diagrams. PhD thesis, BTU Cottbus, Dep. of CS, 2008.

Neco

  • Univ. Evry-Val-d’Essone, France

“Neco is a suite of Unix tools to compile high-level Petri nets into libraries for explicit model-checking. These libraries can be used to build state spaces. It is a command-line tool suite available under the GNU Lesser GPL.

Neco compiler is based on SNAKES [Neco1] toolkit and handles high-level Petri nets annotated with arbitrary Python objects. This allows for big degree of expressivity. Extracting information form models, Neco can identify object types and produce optimized Python or C++ exploration code. The later is done using the Cython language. Moreover, if a part of the model cannot be compiled efficiently a Python fallback is used to handle this part of the model.

The compiler also performs model based optimizations using place bounds [Neco3] and control flow places for more efficient firing functions. However, these optimizations are closely related to a modelling language we use which allows them to be assumed by construction. Because the models from the contest were not provided with such properties, these optimizations could not be used.

The tool suite provides tools to compile high-level Petri nets and build state spaces but this year we also provide a LTL model-checker: Neco-spot. It builds upon Neco and upon Spot [Neco2, Neco4], a C++ library of model-checking algorithms.“

References
  • F. Pommereau. SNAKES is the net algebra kit for editors and simulators. http://www.ibisc.univ- evry.fr/ fpommereau/snakes.htm
  • A. Duret-Lutz and D. Poitrenaud. SPOT: an Extensible Model Checking Library using Transition-based Generalized Buchi Automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pages 76-83, 2004. IEEE Computer Society Press.
  • L. Fronc and F. Pommereau. Optimizing the compilation of Petri nets models. In Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO), volume 726. CEUR, 2011.
  • L. Fronc and A. Duret-Lutz. LTL Model Checking with Neco. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA), to appear in Lecture Notes in Computer Science, Hanoi, Vietnam, 2013. Springer.

PNXDD

  • Univ. Pierre & Marie Curie, France

“PNXDD is CTL model-checker based on Set Decision Diagrams (SDD) [PNXDD1] for PT-nets, a variant of the decision diagrams (DD) family with hierarchy. Symmetric Petri Nets are handled via an optimized unfolding PNXDD2laces structurally detected as always empty and the associated transitions).

Hierarchy paradigm, used together with DDs offers greater sharing possibilities compared to traditional DDs. The ordering of variables in the diagram, a crucial parameter to obtain good performances in DDs, becomes a new challenge since portions of the model offering similar comportments must be statically identified to obtain a good hierarchical order. PNXDD relies on heuristics that are described in [PNXDD3].“

References
  • Y. Thierry-Mieg, D. Poitrenaud, A. Hamez and F. Kordon. Hierarchical Set Decision Diagrams and Regular Models. Proc. of TACAS 2009, volume 5505 of LNCS, pages 1-15, Springer.
  • F. Kordon, A. Linard and E. Paviot-Adet. Optimized Colored Nets Unfolding. Proc. of FORTE 2006, volume 4229 of LNCS, pages 339-355, Springer.
  • S. Hong, F. Kordon, E. Paviot-Adet and S. Evangelista. Computing a Hierarchical Static order for Decision Diagram-Based Representation from P/T Nets. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), volume V, pages 121-140, Springer Verlag 2012.

Sara

  • Univ. Rostock, Germany

“Sara [Sara1] answers reachability queries using the Petri net state equation. From this equation and inequations derived from the query, a linear programming problem is generated and solved using a standard package. If the system does not have solutions, we conclude that there are no reachable states satisfying the query. Other wise, we obtain a firing count vector which describes candidate firing sequences.

We check whether there is an executable firing sequence for the given vector. If so, we have a reachable satisfying state and a witness path. If not, we add inequalities that are not satisfied by the spurious solution. We result in one or more new linear programming problems which enable less serious solutions but still cover all feasible solutions. We proceed recursively with the new problems.

Sara has excellent performance if the state equation as such rules out reachability, or if an early solution reveals reachability. It may be used for unbounded Petri nets. since it does not try to represent or to explore the state space.

In worst case, Sara will not terminate (otherwise, our approach would contradict the known EXPSPACE hardness of the general reachability problem).“

References
  • H. Wimmel and K. Wolf. Applying CEGAR to the Petri net state equation. In Tools and Algorithms for the Construction and Analysis of Systems, 17th International Conference, TACAS, volume 6605 of Lecture Notes in Computer Science, pages 224-238. Springer-Verlag, 2011.

Maria

Maria is a reachability analyzer for concurrent systems that uses Algebraic System Nets (a high-level variant of Petri nets) as its modelling formalism. It has been written in C++, and its is freely available under the terms of the GNU General Public License.

References

MC2 (PLTLc)

Monte Carlo Model Checker for PLTLc

McKit

The Model-Checking Kit

METATOOL

PInA

References
  • Implementation of Joint Commitment Theory through Petri Net Plans. P. F. Palamara, V.A. Ziparo, L. Iocchi, D. Nardi, P. Lima. In Proc. of RoboCup Symposium, 2008.

  • Petri net plans: a formal model for representation and execution of multi-robot plans. V. A. Ziparo, L. Iocchi, D. Nardi, P. F. Palamara , H. Costelha. In Proc. of the 7th international joint conference on Autonomous Agents and MultiAgent Systems (AAMAS 2008). Volume 1. pp 79-86

  • A Robotic Soccer Passing Task Using Petri Net Plans (Demo Paper). P.F. Palamara, V. A. Ziparo, L. Iocchi, D. Nardi, P. Lima, H. Costelha. In Proc. of 7th Int. Conf. on Autonomous Agents and Multiagent Systems (AAMAS 2008), pp.1711-1712. Best Robotic Demo Award.

PRISM

Probabilistic Symbolic Model Checker

PROD

  • univ. hamburg

  • PROD

The Pr/T-net reachability analysis tool PROD implements several methods for efficient reachability analysis.

PROD is a text-based tool that can be used in UNIX (any system of that kind) and in Windows (3.1, 3.11, ‘95, NT, ‘98, 2000, XP). Currently no graphical user-interface exists. PROD supports the following reduced reachability graph generation methods that may also be combined:

The stubborn set method.
The sleep set method.
Priority definitions.
The use of symmetries.

PROD supports verification of CTL formulas from the reachability graph, and on-the-fly verification of LTL formulas using e.g. the stubborn set method.

  • Last updated 2007.

SBML

Matrix Methods

TINA

Timed Petri Net Analyzer

PEP

Availability

Sourceforge repo

Dependencies
  • C++ compiler
  • Tcl/Tkk Unix interface libraries

JPetriNet

Dependencies
  • Java

Mason

“A fast discrete-event multiagent simulation library core, designed to be the foundation for large custom-purpose simulations.”

Dependencies
  • Java

SimPy

“An open source process-oriented discrete event simulation package based on Simula concepts, but goes significantly beyond Simula in its synchronization constructs.”

Dependencies
  • Python

Haskell Coloured Petri Net Editor

Haskell-Coloured Petri Net is a graphical editor and simulator for Coloured Petri Nets, using Haskell as inscription and implementation language.“

“Dormant (great potential, but needs funding for intensive development, and to go beyond coloured Petri nets). Last updated to build with GHC/WxHaskell 0.8 (I do have a version that builds with GHC 6.10.3 and WxHaskell 0.11, but the binary releases of WxHaskell for Windows were missing a critical component, last I checked). More recently, I’ve started on a simple browser-based GUI alternative (Javascript+SVG), but that hasn’t been hooked up to code-generator and simulator yet.”

Availability
Dependencies
  • wxWidgets-2.9.

ePNK

OWLSPNML

PNML Framework

Coloane

  • Coloane
  • Université Pierre et Marie Curie.

Tina

Petri Web

  • Petri Web
  • Technische Universiteit Eindhoven

WoPed

  • WoPeD
  • Berufsakademie Karlsruhe.

ProM

“ProM is a generic open-source framework for implementing process mining tools in a standard environment.”

Dependencies
AIS
IS

CosyVerif

Dependencies:
  • Coloane
  • Virtual Box (Oracle) or other VM
  • BenchKit
References

AlPINA

AlPINA stands for Algebraic Petri Nets Analyzer and is a model checker for Algebraic Petri Nets created by the SMV Group at the University of Geneva. It is 100% written in Java and it is available under the terms of the GNU general public license. Our goal is to provide a user friendly suite of tools for checking models based of the Algebraic Petri Net formalism. AlPiNA provides a user-friendly user interface that was built with the latest metamodeling techniques on the eclipse platform.

Usually, the number of states of concurrent systems grows exponentially in relation to the size of the system. This is called the State Space Explosion. Symbolic Model Checking (SMC) and particularly SMC based on Decision Diagrams is a proven technique to handle the State Space Explosion for simple formalisms such as P/T Petri nets./p>

Algebraic Petri Nets (APN : Petri Nets + Abstract Algebraic Data Types) are a powerful formalism to model concurrent systems. The State Space Explosion is even worse in the case of the APNs than in the P/T nets, mainly because their high expressive power allows end users to model more complex systems. To tackle this problem, AlPiNA uses evolutions of the well known Binary Decision Diagrams (BDDs), such as Data Decision Diagrams, Set Decision Diagrams and Sigma-DDs. It also includes some optimizations specific to the APN formalism, such as algebraic clustering and partial algebraic unfolding, to reduce the memory footprint. With these optimisations, AlPiNA provides a good balance between user-friendliness, modeling expressivity and computational performances.

References
  • D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi. AlPiNA: A symbolic model checker. In J. Lilius and W. Penczek, editors, Applications and Theory of Petri Nets, volume 6128 of Lecture Notes in Computer Science, pages 287-296. Springer, 2010.
  • D. Buchs, S. Hostettler, A. Marechal, and M. Risoldi. Alpina: An algebraic petri net analyzer. In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 349-352. Springer, 2010.
  • S. Hostettler, A. Marechal, A. Linard, M. Risoldi, and D. Buchs. High-level petri net model checking with alpina. Fundamenta Informaticae, 113(3-4):229-264, Aug. 2011.

Cunf

  • École Normale Supérieure de Cachan, France.

Cunf is a set of programs for carrying out unfolding-based verification of Petri nets extended with read arcs, also known as contextual nets, or c-nets. The package specifically contains the following tools:

  • Cunf: constructs the unfolding of a c-net,
  • Cna: performs reachability and deadlock analysis using unfoldings constructed by Cunf,
  • Scripts such as pep2dot or grml2pep to do format conversion between various Petri net formats, unfolding formats, etc.

The unfolding of a c-net is another well-defined c-net of acyclic structure that fully represents the reachable markings of the first. Because unfolding represent behavior by partial orders rather than by interleaving, for highly concurrent c-nets, unfolding are often much (exponentially) smaller, which makes for natural interest in them for the verification of concurrent systems.

Cunf requires that the input c-net is 1-safe (i.e., no reachable marking puts more than one token on every place), and for the time being the tool will blindly assume this. It implements the c-net unfolding procedure proposed by Baldan et al.

Cna (Contextual Net Analyzer), checks for place coverability or deadlock-freedom of a c-net by examining its unfolding. The tool reduces these problems to the satisfiability of a propositional formula that it generates out of the unfolding, and uses Minisat as a back-end to solve the formula.

You may download the tool’s manual from the tool’s webpage, where you will find detailed instructions for installation. The tool is integrated in the Cosyverif environment, whose graphical editor you may want to use to analyze nets constructed by hand. Cunf also comes with Python libraries for producing c-nets programmatically, see Sec. 7 of the manual. References

  • Paolo Baldan, Andrea Corradini, Barbara Konig, and Stefan Schwoon. McMillan’s complete prefix for contextual nets. ToPNoC, 1:199-220, 2008. LNCS 5100.
  • P. Baldan, A. Bruni, A. Corradini, B. Konig, C. Rodriguez, and S. Schwoon. Efficient unfolding of contextual Petri nets. Theoretical Computer Science., 449:2-22, 2012.

libits

libITS is C++ library for model-checking of various formalisms using libDDD.

Main features include:

  • Instantiable Transition System as a framework, allow hierarchical composition of components specified in diverse formalisms.
  • User friendly GUI is provided as Eclipse plugins for modeling ITS compositions, (time) Petri nets, and rich-text editing of GAL models.
  • Optimized implementation taking full advantage of the features of libDDD, notably automatic saturation and hierarchy.
  • Support for Petri nets and some of their extensions
  • Support for discrete time in models such as Time Petri nets and their compositions
  • Support for GAL format input which offers rich data manipulation.
  • Support for ETF format input which is produced by the tool LTSmin from diverse formalisms.
  • Support for Divine format input which is native to the tool Divine and used in BEEM models.
  • Support for CTL model checking using saturation and forward transition relation.
  • Support for LTL model checking using some classic and some original algorithms that exploit saturation.

The ITS tools are distributed under the terms of the GNU Public License GPL. We have integrated modified versions of sources taken from other open-source projects such as Divine, VIS or LTSmin. See Acknowledgements section.

They are built using libDDD for model-checking of (labeled) Petri nets with some extensions (Time Petri nets, Queues, inhibitor arcs, rest arcs, self-modifying nets…), as well as their composition using a formalism called Instantiable Transition Systems. Composite ITS types offer a great flexibility in the definition of synchronized products of transitions systems. Scalar and Circular compositions express common symmetric synchronization patterns (a pool of processes, a ring topology), and are exploited by the tool to provide superior performance. The GAL language complements ITS by providing a model for high-level data manipulation. It offers a rich C-like syntax and direct support for arithmetic and arrays. Systems can be provided using mixed formalisms, such as TPN for the control part and GAL for the data part synchronized using Composite ITS types. ITS-tools also support Divine models natively, thanks to an internal translation to GAL. Last but not least, ETF files produced by LTSmin from several high-level formalisms can be used as input for symbolic model-checking.

Discrete Event Simulation (DES) Software

There is, or was, a visual formalism called DEVS—Discrete Event System Specification—which has developed a host of visual tools for modelling and maybe code/stub generation.

Wikipedia carries a list of open source and commercial DES software:

aDevs

aDevs (a discrete event simulator) is a C++ library for constructing discrete event simulations based on the Parallel DEVS and Dynamic DEVS (dynDEVS) formalisms.

DEVS has been applied to the study of social systems, ecological systems, computer networks and computer architecture, military systems at the tactical and theater levels, and in many other areas.

Recent advances in quantized approximations of continuous systems suggest promising computational techniques for high performance scientific computing (e.g. in the field of computational fluid dynamics).“

Dependencies
  • C++ compiler

CD++

“An open source tool based on the DEVS and Cell-DEVS formalisms (a discrete-event specification of cellular automata models). Hundreds of model samples are available. Varied 2D and 3D visualization engines can be used to improve the analysis of the simulation results.”

PowerDEVS

An integrated tool for hybrid systems modeling and simulation based on the DEVS formalism.

Dependencies
  • Java

Facsimile

A free, open-source discrete-event simulation/emulation library.

Galatea

An Agent-based simulation platform.

Chemical reaction software

Cain

Cain performs stochastic and deterministic simulations of chemical reactions. It can spawn multiple simulation processes to utilize multi-core computers. It stores models, simulation parameters, and simulation results in an XML format. In addition, SBML models can be imported and exported. The models and simulation parameters can be read from input files or edited within the program.

Cain offers a variety of solvers:

  • Gillespie’s direct method.
  • Gillespie’s first reaction method.
  • Gibson and Bruck’s next reaction method.
  • Tau-leaping.
  • Hybrid direct/tau-leaping.
  • ODE integration.“
Dependencies
  • Python

Computer animations

JointJS

  • [JointJS(http://jointjs.org)]

Flexible tool with Petri net demo animation.

Dependencies
  • backbone.js
  • jquery.hs

Computer Animations, U. Waterloo is a browser applet to simulate properties of gases.

“A user can choose one of several gases to investigate at a time. The temperature and volume are two independent variables that can be altered, and the pressures calculated by the two models are presented. This is a deterministic simulation, but the calculated pressures may be misleading.”

One of the suggested application is to ask students to formulate a general statement regarding the conditions, under which the model is valid. Gases such as He, H2, N2, H2O, CO2, etc are included in the applet.

Dependencies
  • Java

Molecular dynamics

PyMol

Molecular modelling tool.

Dependencies
  • Python

Chemsuite

Chemsuite is a set of programs designed for the processing of chemical information on Linux/X11.

Availability

Free software released under the GPL license.

Dependencies
  • QT GUI library version 2.3.1 from Trolltech Inc. .
  • Linux

CHIMP

CHIMP is a generic tool for the modeling of chemical phenomena. Eventually, chemical reaction modeling, molecular mechanics, and quantum mechanic modules will be implemented, along with an easy to use graphical-user interface (GUI). At present, CHIMP has the ability to perform dynamic Monte Carlo simulations on chemical reactions, in particular heterogeneous catalytic reactions.”

VASP

“This is a scientific visualization package for examining output files generated by the Vienna Ab-initio Simulation Package, a package for performing ab-initio quantum-mechanical molecular dynamics using pseudopotentials and a plane wave basis set. The project was initiated when a chemical engineering professor requested assitance in visualizing output files produced by the above package. It displays iso-surfaces and slices of a three-dimensional data set, along with the atoms that make up the molecule the calculations were performed for, and allows symbolic bonds to be inserted between them.”

BIGMAC

“Configurational Bias Monte Carlo (CBMC) is a recent technique to compute thermodynamic properties of flexible molecules. It has been used by several academic groups to study the adsorption behavior of linear and branched alkanes in zeolites and the vapor-liquid equilibrium of linear and branched alkanes. In Cerius2 version 4.0 there is a CBMC utility for calculating adsorption properties of linear and brached molecules. However, Cerius2 is platform dependent and quite expensive.

The group of Prof. Berend Smit has developped BIGMAC, which is a general-purpose CBMC code. You can download a version of this code for grand-canonical and gibbs ensemble simulations of simple linear alkanes (approximately 7.6 MB).“

References

Abinit

“ABINIT is a package whose main program allows one to find the total energy, charge density and electronic structure of systems made of electrons and nuclei (molecules and periodic solids) within Density Functional Theory (DFT), using pseudopotentials and a planewave or wavelet basis.

ABINIT also includes options to optimize the geometry according to the DFT forces and stresses, or to perform molecular dynamics simulations using these forces, or to generate dynamical matrices, Born effective charges, and dielectric tensors, based on Density-Functional Perturbation Theory, and many more properties.

Excited states can be computed within the Many-Body Perturbation Theory (the GW approximation and the Bethe-Salpeter equation), and Time-Dependent Density Functional Theory (for molecules). In addition to the main ABINIT code, different utility programs are provided.

ABINIT is a project that favours development and collaboration (short presentation of the ABINIT project - 10 pages in pdf).“

GROMACS

GROMACS is a versatile package to perform molecular dynamics, i.e. simulate the Newtonian equations of motion for systems with hundreds to millions of particles.

It is primarily designed for biochemical molecules like proteins, lipids and nucleic acids that have a lot of complicated bonded interactions, but since GROMACS is extremely fast at calculating the nonbonded interactions (that usually dominate simulations) many groups are also using it for research on non-biological systems, e.g. polymers.

GROMACS supports all the usual algorithms you expect from a modern molecular dynamics implementation, (check the online reference or manual for details), but there are also quite a few features that make it stand out from the competition:

  • Supports CUDA-based GPU access.
  • No scripting language, all programs use a simple interface.“

AlChemy

Fontana et al. represent molecules as λ-calculus expressions. Reactions are defined by the operations of “application” of one λ-term to its reaction partner. The result is a new λ-term.

It is worth noting in this context that chemical reactions can in turn be regarded as a model of computation, a possibility that is realized for example in the Chemical Abstract Machine.

  • Walter Fontana and Leo W. Buss, Towards a theory of biological organisation, A programmatic statement
  • W. Fontana. Algorithmic chemistry. In C. G. Langton, C. Taylor, J. D. Farmer, and S. Rasmussen, editors, Artificial Life II, pages 159–210, Redwood City, CA, 1992. Addison-Wesley.
  • [20] W. Fontana and L. W. Buss. What would be conserved if ‘the tape were played twice’? Proc. Natl. Acad. Sci. USA, 91:757–761, 1994.

Chemical Abstract Machine

[6] G. Berry and G. Boudol. The chemical abstract machine. Theor. Comp. Sci., 96:217–248, 1992.

Electric circuit emulation

LTSpice

Uses net list data file input.

Availability
  • open source
  • Windows
  • OS X

Synthetic biology

VANTED

  • Leibniz Institute of Plant Genetics and Crop Plant Research (IPK).

VANTED (2006) is a framework for systems biology applications, which comprises a comprehensive set of seven main tasks. These range from network reconstruction, data visualization, integration of various data types, network simulation to data exploration combined with a manifold support of systems biology standards for visualization and data exchange. The offered set of functionalities is instantiated by combining several tasks in order to enable users to view and explore a comprehensive dataset from different perspectives. We describe the system as well as an exemplary workflow.”

References
Dependencies
  • Java VM

Tortuga

Hybrid modelling tools

Hybrid modelling tools support Petri nets and other formalisms.

Hybrid Petri nets refer to Petri nets which support both discrete and continuous transitions.

OpenModelica

ExtendedPetriNet
Features
  • transitions allowing for deterministic or stochastic time delays before their firing (using builit-in random number generators BIRNG or custom made ones),
  • and places capable of containing more than one token such that timed, stochastic Petri nets can be modeled.
  • supports uniform, exponential, normal and Weibull distributions for random time delays.
  • multiple tokens per place as needed for flow and store nets..
Dependencies

InsightMaker

Availability
  • open source
Dependencies
  • any modern browser
  • javascript

Hydra

Hydra is a high level, declarative language for modelling and simulation of physical systems. Systems in Hydra are being modelled using implicitly formulated (undirected) Differential Algebraic Equations (DAEs). While, physical modelling is our main focus any domain is fine where problems can be formulated using DAEs.

The language provides constructs for definition and composition of model fragments that enable modelling and simulation of large, complex, hybrid and highly structurally dynamic systems.

The first outline of Hydra was given by Nilsson et al. in the framework called Functional Hybrid Modelling (FHM). Subsequently, a number of papers have been published about the design and implementation of Hydra that can be accessed on the following web pages:

Dependencies

Haskell compiler (ghc).