Showing changes from revision #1 to #2:
Added | Removed | Changed
This page is a blog article in progress, written by John Baez. To see discussions of this article while it is being written, go to the Azimuth Forum.
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 have been published about the design and implementation of Hydra that can be accessed on the following web pages:
George Giorgidze, Hydra
Haskell compiler (ghc).