
Expand, Enlarge and Check
Verification Group  Université Libre de Bruxelles


This web page offers additional material related to the "Expand, Enlarge and Check" approach to decide the coverability problem of WSTS.
Content of the page:
Papers available for download
 G. Geeraerts, J.F. Raskin,
L. Van Begin. Expand, Enlarge and Check: new
algorithms for the coverability problem of WSTS. In the
Proceedings of FSTTCS 2004: 24th International conference on
Foundations of Software Technology and Theoretical Computer
Science, Chennai, India. Lecture Notes in Computer Science, volume
3328, pages 287298. SpringerVerlag,
2004. [PDF
file]
 G. Geeraerts, J.F. Raskin,
L. Van Begin. Expand, Enlarge and Check: new
algorithms for the coverability problem of WSTS. Journal
version of the former. Journal of Computer and System Sciences,
volume 72(1), pp 180203, Elsevier,
2005. [PDF
file].
 G. Geeraerts, J.F. Raskin,
L. Van Begin. Expand, Enlarge and Check... made
efficient. in proc. CAV'05, 17th International Conference on
Computer Aided Verification. Lecture Notes in Computer Science,
volume 3576, pages 394407 Springer Verlag.
[PDF file]
 A. Finkel, G. Geeraerts, J.F. Raskin, L. Van Begin. A counterexample to
the minimal coverability tree algorithm. Technical report ULB 535.
[PDF
file]
Set of examples used in the experiments
Update (August, 18, 2010) ! The kanban
example that was formerly present on this page was not the same as the
one reported in the CAV 05 paper. The two versions are now present on
the page (see bounded and unbounded PNs) The leabasicapproach example
was incorrectly classified as Petri net with Transfer arcs. Many
thanks to Tim Strazny for pointing this out.
For each example, we mention the size (number of places and number
of transitions) and give a short description. The specification files
are available for download. They describe the examples under the form
of counter machines: a set of integer variables and a set of
transitions that modify the value of the counters. The formalism used
to describe the examples should be selfexplanatory. The property that
is verified (i.e. the reachability of a given upwardclosed set of
values of the counters) is also given in the file.
We study three category of examples:
Bounded Petri nets
Lamport 

#Places:11 
#Transitions:9 
[Download] 
The mutual exclusion protocol by Leslie Lamport, with two threads. 
newDekker 

#Places:16 
#Transitions:14 
[Download] 
The Dekker mutual exclusion protocol, with two threads 
newRTP 

#Places:9 
#Transitions:12 
[Download] 
A very basic communication protocol 
Peterson 

#Places:14 
#Transitions:12 
[Download] 
The Peterson mutual exclusion protocol, with two threads 
ReadWrite 

#Places:13 
#Transitions:9 
[Download] 
A simple "reader/writer" mutual exclusion example. 
Kanban (bounded version) 

#Places:16 
#Transitions:16 
[Download] 
A concurrent production
system. This version of the file has been used in the testsuite
of the CAV05 paper.
[Petri net] 
LeaBasicApproach 

#Places:16 
#Transitions:12 
[Download] 
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM):
Design, Principles and Patterns, second edition, Adison Wesley, 2000 
Petri nets
basicME 

#Places:5 
#Transitions:4 
[Download] 
A basic mutual exclusion protocol, with an unbound number of threads. The Petri net can be found as Fig. 1 of
Giorgio Delzanno, JeanFrançois Raskin an Laurent Van Begin, Attacking Symbolic State Explosion, in Proc. CAV'01, LNCS 2102.
[Download this paper] 
CSM 

#Places:14 
#Transitions:13 
[Download] 
This example describes a concurrent production system. It is taken from Fig.
76 of M. Ajmone Marsan, G. Balbo,
G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel
Computing  Chichester, 1995. [Petri net] 
Kanban (unbounded version) 

#Places:16 
#Transitions:16 
[Download] 
A concurrent production
system. This is not the example that occurs in the testsuite of
the CAV05 paper (see bounded version instead). The only
difference is in the initial marking.
[Petri net] 
Mesh2x2 

#Places:32 
#Transitions:32 
[Download] 
This example describes a system in which a set of processors share the execution of various processes. It is
taken from Fig. 130 of M. Ajmone Marsan, G. Balbo,
G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel
Computing  Chichester, 1995.
[Petri net] 
Mesh3x2 

#Places:52 
#Transitions:54 
[Download] 
This example is an extension of the former one. 
Multipoll 

#Places:18 
#Transitions:21 
[Download] 
This example comes from Andrew S. Miner and Gianfranco Ciardo, Efficient Reachability Set Generation and
Storage Using Decision Diagrams, in Proc. ICATPN'99, LNCS 1639. It describes a concurrent production system.
[Petri net] 
PNCSAcover 

#Places:31 
#Transitions:36 
[Download] 
This is the PNCSA protocol as described in example 4.7 of Alain Finkel, The minimal coverability graph for
Petri nets, Proc. APN'93, LNCS 674 
Petri nets with transfer arcs
CSMBroad 

#Places:13 
#Transitions:8 
[Download] 
The Control Server Monitor. A consistency protocol with atomic syncronization actions.
[Image] 
MOESI 

#Places:9 
#Transitions:11 
[Download] 
A cache coherency protocol.

German 

#Places:12 
#Transitions:8 
[Download] 
Steve German's cache coherency protocol. 
Java 

#Places:44 
#Transitions:37 
[Download] 
The counting abstraction of a Consumer/Producer multithread Java program, with two different kinds of consumers
and producers. Buggy. [Java source code] 
Javasanserreur 

#Places:44 
#Transitions:38 
[Download] 
The counting abstraction of a Consumer/Producer multithread Java program. Same as the previous
example but without the bug. [Java source code] 
ConsProd 

#Places:18 
#Transitions:14 
[Download] 
The counting abstraction of a Consumer/Producer multithreaded Java Program, taken from the
[Sun tutorial]. 
ConsProd2 

#Places:18 
#Transitions:14 
[Download] 
Same as the former example, with another property. 
DelegateBuffer 

#Places:50 
#Transitions:52 
[Download] 
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM):
Design, Principles and Patterns, second edition, Adison Wesley, 2000 
ExempleLea 

#Places:48 
#Transitions:42 
[Download] 
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM):
Design, Principles and Patterns, second edition, Adison Wesley, 2000 
QueuedBusyFlag 

#Places:80 
#Transitions:104 
[Download] 
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM):
Design, Principles and Patterns, second edition, Adison Wesley, 2000 
SimpleJavaExample 

#Places:32 
#Transitions:28 
[Download] 
An example of Java program where two threads share an object describing a point in 2dimensional space, and
increment or decrement its coordinates. [Java source code] 
TransThesis 

#Places:90 
#Transitions:117 
[Download] 
An example of conting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM):
Design, Principles and Patterns, second edition, Adison Wesley, 2000 
EFM 

#Places:6 
#Transitions:5 
[Download] 
The EsparzaFinkelMayr counter machine. Can be found at Fig. 2 of Javier Esparza, Alain Finkel, Richard Mayr,
On the verification of broadcast protocols, in Proc. LICS'99. IEEE Computer Society, 352359.

Experimental results
This page reports on the experiments we have carried out in order to assess the pratical usability of Expand, Enlarge and Check.
Download
The EEC algorithm for Petri nets
only has been implemented in the
mist
tool.
Warning ! Do not run the EEC
implementation of the mist2 tool on the examples that are not Petri
nets (i.e. Petri nets with transfers or broadcast protocols...), since
the tool will not detect that your source file is not
adequate, will not produce any warning, and will produce
incorrect results !!
Links
Mer aoû 18 16:56:34 CEST 2010