fond

jQuery Multi Level CSS Menu Css3Menu.com

Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
MCC�2013, Participating Tools
Last Updated
Apr. 26, 2013

Introduction

This page summarizes some facts about the elaboration of the MCC'2013. There were twelve submissions from five countries this year, including several variants of a tool (LoLA). The organizers thanks the tool developers for their effort and cooperation during the evaluation of their submission.

A short description of these tools, as well as some references are provided below. We also provide a link to the official web site and to the disk image that was submitted.

AlPiNA (Univ. Geneva, Switzerland)

AlPiNA [Alpina1, Alpina2, Alpina3] 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

Links

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:

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. in [Cunf1], the algorithms and data structures actually implemented have been partially described in [Cunf2].

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

Links

GreatSPN (Univ. Torino, Italy)

GreatSPN [Greatspn1, Greatspn2] 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 last enhancements include:

References

Links

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

Links

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

Links

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

Links

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

Links

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 [PNXDD2] (removing places 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

Links

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

Links