Showing changes from revision #62 to #63:
Added | Removed | Changed
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.
Here is an example of a Petri net taken from chemistry:
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 + O_{2} $\to$ CO_{2}
CO_{2} + NaOH $\to$ NaHCO_{3}
NaHCO_{3} + HCl $\to$ H_{2}O + NaCl + CO_{2}
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
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 CO_{2}, NaHCO_{3}, H_{2}O 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:
If the carbon dioxide combines with the sodium hydroxide to form sodium bicarbonate, we obtain:
If the sodium bicarbonate and hydrochloric acid react, we then obtain:
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.
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, \dots, x_n$ and a set of morphisms between tensor products of these objects, for example:
Here $1$ 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.
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:
Peter J. E. Goss and Jean Peccoud, Quantitative modeling of stochastic systems in molecular biology by using stochastic Petri nets, Proc. Natl. Acad. Sci. USA 95 (June 1998), 6750-6755.
Peter J. Haas, Stochastic Petri Nets: Modelling, Stability, Simulation, Springer, Berlin, 2002.
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:
The basic idea here is very simple. Consider, for example, the following Petri net:
If we use $x_1$ to denote “rabbit” and $x_2$ to denote “fox”, the transitions are:
in which one rabbit becomes two,
in which a fox eats a rabbit and reproduces, resulting in two foxes, and
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]$ denote the concentration of rabbits (say, in rabbits per hectare) and let $[x_2]$ the concentration of foxes as a function of time. Then following the standard procedure in chemistry, we would get these equations:
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]$ is given by a sum over all transitions.
Each transition contributes to the time derivative of $[x_i]$ in the obvious way: we take the rate at which that transition occurs, and multiply it by the number of times $x_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,\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^{-18}$ of a wolf, we should not expect wolves to survive, even if the model predicts that their numbers rise later.
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:
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, B$ and $C$ are three molecular species, and we have four reactions between them:
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:
Martin Feinberg, Lectures on reaction networks.
F. Horn and R. Jackson, General mass action kinetics, Archive for Rational Mechanics and Analysis 47 (1972), 81–116.
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.
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:
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:
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.
G. Craciun, M. Feinberg and Y. Tang, Understanding bistability in complex enzyme-driven reaction networks, Proc. Nat. Acad. Sci. USA 103 (2006), 8697-8702.
M. Feinberg, Multiple steady states for chemical reaction networks of deficiency one, Arch. Rational Mech. Analysis 132 (1995), 371-406.
For oscillations, see:
There is an interesting relation between chemical reaction networks (or, better, Petri nets) and toric varieties. See:
Craciun, Dickenstein, Shiu and Sturmfels, Toric dynamical systems.
Leonard Adleman, Manoj Gopalkrishnan, Ming-Deh Huang, Pablo Moisset and Dustin Reishus, On the mathematics of the law of mass action.
and also the paper by Mirela Domijan and Markus Kirkilionis cited above.
Some good online introduction include:
Petri Net, Wikipedia
Petri net in $n$Lab
Carl Adam Petri and Wolfgang Reisig, Petri net, Scholarpedia.
Wil van der Aalst, Vincent Almering, and Hermen Wijbenga, Interactive tutorials on Petri nets.
The Petri Nets World, Department of Informatics, University of Hamburg.
John Baez and Jacob Biamonte, A course on quantum techniques for stochastic physics.
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:
Martin Feinberg, Lectures on reaction networks.
F. Horn and R. Jackson, General mass action kinetics, Archive for Rational Mechanics and Analysis 47 (1972), 81–116.
Jeremy Gunawardena, Chemical reaction network theory for in-silico biologists.
For applications to biology, see:
P. Goss and J. Peccoud, Quantitative modeling of stochastic systems in molecular biology by using stochastic Petri nets, Proc. Natl. Acad. Sci. USA 98 (1998), 6750–6755.
P. Dodd and N. Ferguson, A many-body field theory approach to stochastic models in population biology, PLoS ONE 4 (2009).
Ina Koch, Petri nets – a mathematical formalism to analyze chemical reaction networks, Molecular Informatics 29 (2010), 838–843.
D. Wilkinson, Stochastic Modelling for Systems Biology, Taylor and Francis, 2006.
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:
Apparently this paper is important reference on stability for reaction networks:
There is an interesting relation between reaction networks (or Petri nets) and toric varieties. See:
Georghe Craciun, Dickenstein, Anne Shiu and Bernd Sturmfels, Toric dynamical systems.
Leonard Adleman, Manoj Gopalkrishnan, Ming-Deh Huang, Pablo Moisset and Dustin Reishus, On the mathematics of the law of mass action.
On the category theory of Petri nets:
Vladimiro Sassone, An axiomatization of the category of Petri net computations
Eric Fabre, On the construction of pullbacks for safe Petri nets
Interesting papers:
Gil Benkö, Florian Centler, Peter Dittrich, Christoph Flamm, Bärbel M. R. Stadler, A Topological Approach to Chemical Organizations
Andrew Phillips, Matthew Lakin, Loïc Paulevé, Stochastic Simulation of Process Calculi for Biology, arxiv.
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.
“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”.“
Analysis of Dynamic Algebraic Models.
Model of Concurrency, Communication and Conputation, DISCo, Unimib
Gabriel Juhas, Robert Lorenz and Jorg Desel Unifying Petri Nets Semantics with Token Flows
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.
Jetty Kleijn (Leiden Univ.) and Joerg Desel (Hagen Univ.)
L.M.F. Bertens, J. Kleijn, S.C. Hille, M. Koutny, M. Heiner, F.J. Verbeek. Modeling biological gradient formation: combining partial differential equations and Petri nets. School of Computing Science, University of Newcastle upon Tyne, Technical Report Series 1379, 2013.
Ehrenfeucht A, Kleijn J, Koutny M, Rozenberg G, Qualitative and Quantitative Aspects of a Model for Processes Inspired by the Functioning of the Living Cell (2011)
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.
Integrated Net Analyzer
Model checking And Reachability analysis done effiCIEntly.
“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:
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
“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.“
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 [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
“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.“
“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].“
“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).“
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.
Monte Carlo Model Checker for PLTLc
The Model-Checking Kit
Universite di Roma
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.
Probabilistic Symbolic Model Checker
univ. hamburg
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.
Matrix Methods
Timed Petri Net Analyzer
“A fast discrete-event multiagent simulation library core, designed to be the foundation for large custom-purpose simulations.”
“An open source process-oriented discrete event simulation package based on Simula concepts, but goes significantly beyond Simula in its synchronization constructs.”
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.”
“ProM is a generic open-source framework for implementing process mining tools in a standard environment.”
E. André, Y. Lembachar, L. Petrucci, F. Hulin-Hubard, A. Linard, L.-M. Hillah, and F. Kordon. CosyVerif : an Open Source Extensible Verification Environment. In 18th IEEE International Conference on Engineering of Complex Computer Systems - ICECCS, IEEE Computer Society, July 2013.
J. Gogen and Luqi, “Formal methods: Promises and problems,” IEEE Software, vol. 14, no. 1, pp. 75–85, 1997
C. Girault and R. Valk, Eds., Petri Nets and System Engineer- ing. Springer Verlag, 2003, ch. 2, pp. 9–23.
K. Jensen and L. Kristensen, Coloured Petri Nets - Modeling and Validation of Concurrent Systems. Springer, 2009.
M. Diaz, Petri Nets: Fundamental Models, Verification and Applications. Wiley, 2009.
[Petri Net Community, The Petri Net Tool Database]
“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.
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:
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
libITS is C++ library for model-checking of various formalisms using libDDD.
Main features include:
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.
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 (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).“
“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.”
An integrated tool for hybrid systems modeling and simulation based on the DEVS formalism.
A free, open-source discrete-event simulation/emulation library.
An Agent-based simulation platform.
“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:
Flexible tool with Petri net demo animation.
“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.
Molecular modelling tool.
“Chemsuite is a set of programs designed for the processing of chemical information on Linux/X11.
Free software released under the GPL license.
“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.”
“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.”
“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).“
“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 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:
Fontana et al. represent molecules as λ-calculus expressions. Reactions are deﬁned 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.
[6] G. Berry and G. Boudol. The chemical abstract machine. Theor. Comp. Sci., 96:217–248, 1992.
Uses net list data file input.
“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.”
Hybrid modelling tools support Petri nets and other formalisms.
Hybrid Petri nets refer to Petri nets which support both discrete and continuous transitions.
Swiss Federal Institue of Technology Zurich (ETHZ)
Stefan M.O.Fabricius, Extensions to the Petri net library in Modelica (2001)
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 has have been published about the design and implementation of Hydra that can be accessed on the following web pages:
George Georgidze, Giorgidze,Hydra
Haskell compiler (ghc).