Experiments of Novel Algorithms for Stubborn Sets and Reachability

                                           

This webpage is used to give more details of the experiments in Novel Algorithms for Stubborn Sets and Reachability.  The approach has been implemented in LLTS module of PAT model checker. The version of PAT that contains the LLTS module can be downloaded here. All the experiment files in this paper are available here.

We construct experiments to evaluate efficiency of our method proposed in paper. All the experiments are run on a PC with Intel® CoreTM i5-2410 CPUs @2.3GHz and 4GB RAM, on a 64-bit Windows system.

 

This page is maintained by Tian Huat Tan.

Please contact with us if you have any question about this webpage or these experiments. We will reply your enquiries as soon as possible.

 

Experiment

Consider the system as followed:
There are three processes running concurrently, and each has simply one action, we shall refer to them as a, b, and c. There are three variables, x, y, and z. and a constant k. Initially x = y = z = 0.
– a = (x < k, x := x + 1)
– b = (y < k, y := y + 1)
– c = (x = 0 && y = 0, x := k)
– d = (true, z :=1 − z)

This example can be represented by the following Labeled Transition System:

 

Experiment results:

 

 

Model

Full

DL (sym)

DL (asym) (our approach)

Cycle

Mixed (our approach)

#States

#Trans

Time(s)

#States

#Trans

Time(s)

#States

#Trans

Time(s)

#States

#Trans

Time(s)

#States

#Trans

Time(s)

Run(10)

288

818

0.06

88

136

0.02

35

58

0.03

288

689

0.08

36

59

0.07

Run(100)

20808

62018

0.62

808

1216

0.05

305

508

0.04

full

51764

1.33

306

509

0.3

Run(200)

81608

244018

2.78

1608

2416

0.17

605

1008

0.07

full

203514

6.6

606

1009

0.92

 

For the model, Run(a) represents the above LTS models with constant k = a. The model is deadlock free. For verification of reachability, we choose a condition that no state would satisfy; therefore resulting in full exploration of the state-space. The Full scenario denotes the situation for verification of deadlock-freeness as well as reachability checking in unreduced state space.  Other scenarios represent different approaches to verify deadlock-freeness and reachability with partial order reduction. DL (sym) and DL (asym) are the scenarios where symmetric and asymmetric disabling relations are used respectively to verify deadlock-freeness. Cycle is the scenario where simple cycle condition and symmetric disabling relation are used to verify reachability. Mixed represents the scenario where mixed strategy with Tarjan algorithm and asymmetric disabling relation are used to verify reachability.

 

Discussion:

The running example state space is quadratic in the parameter k. The symmetric partial order reduction brings this down to linear. The asymmetric reduction seems similarly linear, but produces less than half the states. The simple cycle condition does not allow for any reduction in our examples, whereas using the algorithm compatible with the S-condition performs almost identically to the asymmetric deadlock checking algorithm.