# 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

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

### Links

- Disk image submitted to MCC'2013@Petri Nets (634MB compressed),
- Official web page.

## 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. 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

- [Cunf1] Paolo Baldan, Andrea Corradini, Barbara Konig, and Stefan Schwoon. McMillan's complete prefix for contextual nets. ToPNoC, 1:199-220, 2008. LNCS 5100.
- [Cunf2] 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.

### Links

- Disk image submitted to MCC'2013@Petri Nets (607MB, compressed),
- Official web page.

## 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:

- 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

- [Greatspn1] 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.
- [Greatspn2] 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.

### Links

- Disk image submitted to MCC'2013@Petri Nets (2.1GB compressed),
- Official web page.

## 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

- [Itstools1] 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)
- [Itstools2] 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)
- [Itstools3] 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)
- [Itstools4] 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)

### Links

- Disk image submitted to MCC'2013@Petri Nets (640MB compressed),
- Official web page.

## 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

- [Lola1] 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

### Links

- Disk image submitted to MCC'2013@Petri Nets (926MB compressed),
- Official web page.

### 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

- [Marcie1] 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.
- [Marcie2] 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.
- [Marcie3] M. Schwarick and A. Tovchigrechko. IDD-based model validation of biochemical networks. TCS 412, pages 2884-2908, 2010.
- [Marcie4] A. Tovchigrechko. Model Checking Using Interval Decision Diagrams. PhD thesis, BTU Cottbus, Dep. of CS, 2008.

### Links

- Disk image submitted to MCC'2013@Petri Nets (621MB compressed),
- Official web page.

## 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

- [Neco1] F. Pommereau. SNAKES is the net algebra kit for editors and simulators. http://www.ibisc.univ- evry.fr/ fpommereau/snakes.htm
- [Neco2] 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.
- [Neco3] 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.
- [Neco4] 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.

### Links

- Disk image submitted to MCC'2013@Petri Nets (950MB compressed),
- Official web page.

## 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

- [PNXDD1] 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.
- [PNXDD2] F. Kordon, A. Linard and E. Paviot-Adet. Optimized Colored Nets Unfolding. Proc. of FORTE 2006, volume 4229 of LNCS, pages 339-355, Springer.
- [PNXDD3] 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.

### Links

- Disk image submitted to MCC'2013@Petri Nets (915MB compressed),
- Official web page.

## 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

- [Sara1] 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.

### Links

- Disk image submitted to MCC'2013@Petri Nets (926MB compressed),
- Official web page.