Introduction

This page summarizes the techniques reported by the tool which participated to the MCC'2013.

Proposed Values to report techniques

A (non exhaustive) list of techniques was proposed in the call for tool submission to report the techniques used by tools:

Abstractions: the tool exploits the use of abstractions (on the fly state elimination),
Decision Diagrams: the tool uses any kind of decision diagrams,
Explicit: the tool does explicit model checking,
Net Unfolding: the tool uses MacMillan unfolding,
Parallel Processing*: the tool uses multithreading,
Structural Reduction: the tool uses structural reductions (Berthelot, Haddad, etc.),
SAT/SMT: the tool uses a constraint solver,
State Compression: the tool uses some compression technique (other than decision diagrams),
Stubborn Sets: the tool uses partial order technique,
Symmetries: the tool exploits symmetries of the system,
Topological: the tool uses structural informations on the Petri net itself (e.g. siphons, traps, S-invariants or T-invariants, etc.) to optimize model checking,
Unfolding to P/T net: the tool transforms colored nets into their equivalent P/T,

*: in fact, only one core was allocated to each Virtual Machine so no parallelism could be enabled in practice (but no tool reported this feature).

Report from tools is summarized below.

Techniques reported by tools
Tool Name	Reported Techniques
Apina	Decision Diagrams
Cunf	Net Unfolding, SAT/SMT
greatSPN	Decision Diagrams
ITS-Tools	Decision Diagrams Structural Reductions
LoLA (all variants)	Explicit model checking State compression Stubborn sets
Marcie	Decision Diagrams
Neco	Explicit model checking
PNXDD	Decision Diagrams Topological
Sara	SAT/SMT Stubborn Sets Topological