Our goal is to set up a library of examples of infinitestate systems
to be used to evaluate theoretical and practical
methods. For this purpose we have defined a very simple language based
counter machines that can be used to encode
different extensions of Petri Nets.
The lowlevel language (together with an highlevel language based on communication machines) is defined here.
All examples should be specified in the low level language, i.e., as a Counter Machine.
For our experiments we plan to consider the following data structures :
We plan to apply these data structure as Constraint Solver within the framework of Constraintbased Automated Verification:
Safety Properties: Given initial states S_{0} and target states T
Forward Reachability:
Dimensions
Phase 1: A Fair Benchmarking
The goal of this phase is to compare the tradeoff
between efficiency, robustness and usability of the constraint solvers.
More in detail, the idea is to consider the constraint
solvers as providers of services (set operations) we take as black box
and that we encorporate in a general scheme of
the standard verification algorithm used in symbolic model checking
(backward reachability).
This way, we try to guarantee the fairness of
the comparison of the performance of the different solvers (i.e.
we avoid optimizations
peculiar to the data structures we will reintroduce
later).
The structure of the algorithm and the nature of the services
 The algorithm must implement a BreadthFirst Search in which the accessibility relation is the preimage operator
 Since we restrict this phase at Petri Nets, we will consider a fixed representation of the transition system (at the level of the platform)
 The set of services we need here are:

EMPTY emptyset

INTERSECT intersection of denotations!

DIFFERENCE difference of denotations!

UNION union of denotations!

IS_EMPTY test of emptyness
 REPRESENT(F)
to represent the initial states and target states taken in input inside
the solver

PRE_{t }preimage computation over a single transition of
the input
 PRE_{T}
preimage computation over the whole transition system
Note1: REPRESENT
and the PREimage operators are the only nonstandard operators we expect
that the designer of the platform has to implement
in order to integrate the platform with the constrain solvers.
Concerning PRE, they will take as input a single transition/whole relation
and a set of states
the first parameter is the same for all libraries (the implementation of
PRe will take care of translating in the right format for the solver)
whereas the second parameter is peculiar of the considered data structure
(it is a var of the right type...).
We remove all the optimizations in the implementations of the different operators
 Based on the previous set of operators, we will focus our experiments on the following search algorithms:
There are (at least) two type of search: the plain
search in which we always `try' to compute a fixpoint
and then check for the initial states, and the
onthefly search in which we interleave the steps of the main loop with
a test for the initial states.
Here are the abstract algorithms:
Algorithm 1 Plain Backward Search
Let T be the set of transitions {t1,...,tk},
TS the target states, and I the initial states,
all read from input
F:=REPRESENT(TS);
I:=REPRESENT(IS);
R:=emptyset;
while (not(IS_EMPTY(F))) do
begin
R:=UNION(R,F);
L:=EMPTY;
for every transition t in T do
begin
AUX:=PRE_{t}(F);
L:=UNION(AUX,L);
end;
F:=DIFFERENCE(L,R);
end;
if IS_EMPTY(INTERSECT(I,R)) then VERIFIED
otherwise TRACE(?)
Algorithm 2 OntheFly Backward Search
TS the target states, and IS the initial states, all read from input
F:=REPRESENT(TS);
I:=REPRESENT(IS);
R:=emptyset;
Error:=false;
while (not(IS_EMPTY(F))) do
begin
R:=UNION(R,F);
if IS_EMPTY(INTERSECT(I,R)) then Error:=true;break
L:=EMPTY;
for every transition t in T do
begin
AUX:=PRE_{t}(F);
L:=UNION(AUX,L);
end;
F:=DIFFERENCE(L,R);
end;
If Error then TRACE
otherwise VERIFIED
Algorithm 3 Fully Symbolic Backward Search
TS the target states, and IS the initial states, all read from input
F:=REPRESENT(TS);
I:=REPRESENT(IS);
R:=emptyset;
Error:=false;
while (not(IS_EMPTY(F))) do
begin
R:=UNION(R,F);
if IS_EMPTY(INTERSECT(I,R)) then Error:=true;break
L:=PRE_{T}(F);
F:=DIFFERENCE(L,R);
end;
If Error then TRACE
otherwise VERIFIED
Models and Measures
What do we expect from the fair experiments?
Well, we expect to have a first selection w.r.t.
: performance of each library, compacteness of resulting data, flexibility
w.r.t. the set of models we have in mind.
Furthermore, for each library we'd like to know:
how much time did we spend in adapting it to export the adequate services?
In average how much time every operations takes
w.r.t. the whole computation? Peaks in memory usage and execution times.
Specifically, this is my proposal for models/measures
Models
In the first phase we will focus our attention
on Petri Nets (Bounded/Unbounded) and Petri Nets with Inhibitor Arcs
This way, we avoid many of the problems due to
optimizations and all other tricks.
The examples for the moment we have are (see
list below):
 Lamport, Dekker, Peterson
 CSM,FMS,CTS,Multipoll, Kanban, Mesh (different
sizes)
 Readers & writers
Measures
Based e.g. on the spy of Gilles we should measure (fixing the parameters discussed before, eg., swap space etc.)
Overall Computation:
 Execution time
 Number of Steps
 Memory used to store the fixpoint
 Features peculiar of the data structure: e.g.
nodes of CSTs, DDDs, size of automata of NDDs
 Number of symbolic states
Average
 Max size of intermediate set variables (wrt.
to the peculiarties of the data structure)
 Max execution time of each step
Services Profiling
 Execution time of each operation with max and
avg values
 Memory used for each operations with max and
avg values
 Sizes (again peculiar of the different data
structures) od the data structures used in the intermediate operations
I think this should give use good indicators for the performance of the solvers.
Invariants
Concerning the invariants we could run a second
series of experiments in which we
prune via invariants. However we must be careful
on how we prune.
Alternatively, we can see invariants as part of the optimizations (every
solver use them in its own and
more effective way).
Here
are some results.
Warning: we should turn all examples into one of the following specification languages: Global Machines and Counter Machines, both defined here
The examples we have are listed below (classified in terms of Petri Nets Extensions)
Bounded Petri Nets
Basic ME protocol Fig. 1 in Description
Abstract Multithreaded Java Programs
A beta version of CBP2GM is available. Click here to download CBP2GM (.tar.gz source file, 70 Kb).
CBP2GM is free software.