Supplementary Materials for Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing

This is a supplementary page for the experiment in Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. In the page, you can find the following:

This page is maintained by Chih-Duo Hong (ericpony) and Yu-Fang Chen. Any questions about the experiments are welcome. We are eager to have discussions/take questions about the experiments, so please do not hesitate to do it. We will be very responsive.

THE EXECUTABLE FILES AND SOURCE CODE

Both the simulation subsumption algorithm and the subsumption algorithm of Fogarty and Vardi [3] are implemented in Java. The programs are compiled for environment compatible with Sun's JRE with version ≥ 1.5.

  • Checking Universality with Subsumption (jar)
  • Checking Universality with Simulation Subsumption (jar)
  • Checking Inclusion with Subsumption (jar)
  • Checking Inclusion with Simulation Subsumption (jar)
The source code is available here.
Our programs are tested on OpenJDK 64-Bit Server VM and Java HotSpot(TM) 64-Bit Server VM. We use the getCurrentThreadCpuTime method to get the CPU time. Note that some JVMs (e.g. gij, the GNU libgcj) do not support this function. Our programs, while they will give the correct answer if the computation ever stops, will not give the correct computation time on these JVMs.

Universality Test

Usage: 

	java -jar jar_file Aut_file Timeout
The program will test if L(Aut) = Σω, where Aut is a Büchi automaton described by a BA file. Timeout is given in second; zero value indicates no timeout.

Example: 

	java -jar CheckingUniversality_SimulationSubsumption.jar peterson.crtcl.ba 1000

	Program output:

	Not Universal
	Time for the Simulation Subsumption algorithm(ms): 10.

Inclusion Test

Usage: 

	java -jar jar_file Aut1_file Aut2_file Timeout
The program will test if L(Aut1) ⊆ L(Aut2), where Aut1 and Aut2 are two Büchi automata described by BA files. Timeout is given in second; zero value indicates no timeout.

Example: 

	java -jar CheckingInclusion_SimulationSubsumption.jar peterson.1.crtcl.ba peterson.crtcl.ba 1000

	Program output:

	Aut1: # of Trans. 33, # of States 20.
	Aut2: # of Trans. 34, # of States 20.
	Included
	Time for the Simulation Subsumption algorithm(ms): 330.

THE LOG FILES

Here we list the log files of our experiments that are based on random models. In the all experiments below, we allowed a program to use at most 2048MB memory. The timeout period is set as 3500 seconds.

Universality checking on Tabakov and Vardi's random model (tgz)

Tabakov and Vardi's random model [4] has a fixed alphabet size 2 and two parameters: transition density td (the average number of outgoing transitions per alphabet symbol from a state) and acceptance density ad (the percentage of accepting states). For each combination of td=0.5, 1,..., 4, and ad=0.1,0.2,...,1.0, we generate 100 random BA instances. The naming rule of the log files is "td-ad-no.log", where td is transition density, ad is acceptance density, and no is the serial number of the experiment.

The following is an example of the log file.

DescriptionFile contents (0.5-0.1-1.log)
Computation time information* 
Format, Universal (ms), Non-universal (ms), Timeout cases
Subsumption, 0, 10, 0
Simulation Subsumption, 0, 80, 0
Tell if the automata is universal** 
	N
A description of the automata in BA format 
	[100]
	0,[1]->[30]
	...
	0,[99]->[71]
	[1]
	[37]
	...

* The execution times are stored separately respectively for the universal and the non-universal cases. If last column is set to one, it means that the answer can not be computed in 3500 seconds, in which cases the execution time is set to zero. For example, "Subsumption, 0, 0, 1 \n Simulation Subsumption, 0, 358620, 0" means the subsumption algorithm cannot find the answer in 3500 seconds while the simulation subsumption algorithm can find the answer in 358.62 seconds.

** U for "Universal", N for "Non-universal", and D for "Don't know". We get the result D when both algorithms fail to finish the task within the timeout period.

Universality checking with random LTL formulae (tgz)

In this experiment, we generate Büchi automata from random valid LTL formulae in the form of ~f\/f. The formulae have lengths among 12, 18, 24, and 30. The number of propositions in a formula is among 1, 2, 3, and 4, which corresponds to a Büchi automaton with alphabet size 2, 4, 8, and 16, respectively. For each configuration, we generate 100 automata and compute the total execution time needed to get the results. The names of the log files are in the form of "(length/2)-props.log", where "length" and "props" are the length of and number of propositions in a formula, respectively. Each log file is a summary of the result from 100 random LTL formulae.

The following is an example of the log file.

DescriptionFile contents (12-1.log)
The LTL formula (100 instances in each log) 
	~(<><>( ((<>~p /\ p)) W (()( p R p )) ))\/(<><>( ((<>~p /\ p)) W (()( p R p )) ))
Tell if the automata is universal (always U) 
	U
The automaton translated from LTL
(in BA format) 
	[17]
	0,[17]->[17]
	0,[17]->[3]
	0,[17]->[2]
	...
	[13]
	[15]
	[16]
A summery of the total execution time* 
Total Number of Trans.: 8045, Total Number of States: 1770
Total Time for Subsumption algorithm (Random LTL in the form of ~f\/f),
Universal (ms): 1320 Non-universal (ms): 0 TO cases: 0
Total Time for Simulation subsumption algorithm (Random LTL in the form of ~f\/f),
Universal (ms): 230 Non-universal (ms): 0 TO cases: 0

* The execution times are summed up respectively for the universal and the non-universal cases. The number of instances that cannot be computed within 3500 seconds is given in the "TO cases" field.

Language inclusion checking with random LTL formulae (tgz)

In this experiment, we generate pairs of Büchi automata (A,B) from random LTL formulae and test whether L(A) ⊆ L(B). The formulae we used are of length among 10, 15, and 20. The number of propositions in a formula ranging from 1 to 3, which corresponds to a Büchi automaton with alphabet size among 2, 4, and 8. For each configuration, we generate 10 pairs of automata. The names of the log files are in the form of "length-props.log", where "length" and "props" are the length of and number of propositions in a formula, respectively. Each log file is a summary of the result from 10 pairs of LTL formulae.

The following is an example of the log file.

DescriptionFile contents (10-1.log)
The LTL formula of automaton A 
	()( (<>~( (()p /\ p) ) /\ []p) )
Automaton A translated from LTL
(in BA format) 
	[4]
	0,[1]->[2]
	...
	1,[4]->[4]
	[3]
	[4]
The LTL formula of automaton B 
	(((~p) U ((p /\ p)) /\ p R p)
Automaton B translated from LTL
(in BA format) 
	[6]
	0,[1]->[3]
	...
	0,[6]->[2]
	[2]
	...
	[6]
Separator between pairs of automata 
	============================
A summery of the total execution time* 
Total Number Trans: 460, Total Number States: 140
Total Time for Subsumption algorithm,
Included (ms): 40 Not Included (ms): 120 TO cases: 0
Total Time for Simulation subsumption algorithm,
Included (ms): 0 Not Included (ms): 0 TO cases: 0

* The execution times are summed up respectively for the universal and the non-universal cases. The number of instances that cannot be computed within 3500 seconds is given in the "TO cases" field.

HOW WE GENERATE THE MODELS

The models we used are from BEEM [1], BEnchmarks for Explicit Model checkers. We have conducted our experiments on models of mutual exclusion algorithms including:

  • Fischer's mutual exclusion algorithm (link)
  • Peterson's mutual exclusion protocol for 2 processes
  • MCS queue lock mutual exclusion algorithm (link)
  • Bakery mutual exclusion algorithm (link)
  • Dining philosophers problem (link)
Each model is described using the DVE modeling language. (A sample: Peterson's Algorithm.) Each DVE model is essentially a set of guarded commands. In this set of experiment, we inject (artificial) errors to the DVE models by randomly weaken or strengthen the guards of some commands, translate both the original and the error version into Büchi automata, and test if their control flows (w.r.t. the occupation of the critical section) are identical.

How to translate a DVE model to a Büchi automaton

For each DVE model, we use the tool DiVinE Cluster [2] to generate a file (in DOT format) that describes all of the reachable states (Here is the DOT file generated from the Peterson's Algorithm example). Each state in the DOT file is labeled by the valuation of all variables separated using square brackets. The numbers insides the first square brackets are the valuation of global variables and the numbers insides the square brackets followed by the first one are the the valuation of private variables of each process. Below is an example of a state in a DOT file. 
"[0, {255|3|2}]\n[0,2]\n[3, 3]"
In this state, the values of global variables are 0 and {255|3|2} (the value of an integer array) and the values of the private variables of the 2 participating processes are (0, 2) and (3, 2), respectively. The value of the program counter (line number) is the first value of the private variables of each process.

Here we explain how we translate the state space of a model (described in a DOT file) into a Büchi automaton. Each state in a Büchi automaton is a valuation of all variables. We have a transition from a state to another one if we have the same transition in the DOT file. The transition label is defined as follows. If a state transits to another state, then the transition occurs over symbol 1 if at least one process in the source state is in the critical section; otherwise the transition occurs over symbol 0 (Note that we use model of mutual exclusion algorithm. Each process has some specific line numbers denoting that it is in the critical section). We have two different ways of defining accepting states.
  • When our goal is to observe all possible behaviors of a model, we let all states be accepting.
  • When we are only interested in the behaviors where at least one competing process enters the critical section infinitely often, we mark only the states that are least one process is in the critical section as the accepting states.

The BA file format

 For the purpose of more easily processing, we use the BA file to store a Büchi automaton. The format of a BA file is as follows. 
	(initial state)
	...
	transitions
	...	
	(accepting states)
A BA file consists of three parts in the following order: the initial state, the transitions, and the accepting states. When the initial state is ommited, the source state of the first transition is assumed to be the initial state. When the accepting states are ommitted, it is assumed that all states are accepting. A state consists of a set of variation of the variables in the model. A transition is of the form "transition label,source state->destinination state." The following is the content of an example BA file: 
	0,[1]->[2]
	1,[2]->[1]
	[2]
This BA file describes a Büchi automaton that has [1] as the initial state, [2] as an accepting state, a transition from [1] to [2] over word 0, and a transition from [2] to [1] over word 1. For a more complicated example, here you can get the BA file of Peterson's algorithm we use in our inclusion experiment.

Convert a DOT file to a BA file

Assume that in the DOT file there is a transition
	"[0, {255|3|2}]\n[0]\n[3]\n[2]\n[1]"->"[0, {255|2|1}]\n[0]\n[3]\n[2]\n[1]".
Also assume that the line number of the critical section is 2 in this model. The corresponding BA file should have a transition from state [0 255|3|2][0][3][2][1] to state [0 255|2|1][0][3][2][1]. Moreover, note that in the source state, the third process is in the critical section (i.e., its line number is 2). The transition label should be 1. Therefore, in the BA file the transition should read 
	1,[0 255|3|2][0][3][2][1]->[0 255|2|1][0][3][2][1]
One can obtain a DOT file from a DVE model using divine.draw_state_space from the DiVinE [2] tool. Given a DOT file, one may use this bash script to convert it to a BA file, and this script to convert it to an MH file. Moreover, one may also convert a BA file to an MH file using this script.

BUCHI AUTOMATA MODELS AND FURTHER EXPERIMENTAL RESULTS

Here we list the model files and the log files, as well as a brief table of the experiment results. In the all experiments below, we allowed a program to use at most 8192MB memory. The timeout period is set as 1 day.

Setting 1: A state p is accepting iff the CS is occupied by some process. (tgz)

Model OriginalError L(O)⊇L(E) L(O)⊆L(E)
Peterson's protocol 2 processes , DVE, BA 2 processes with 1 error (details), DVE, BA S: 2.7 sec (T)
SS: 0.9 sec (T) 		S: 1.4 sec (F)
SS: 0.2 sec (F)
The MCS algorithm 3 processes, DVE*, BA 3 processes with 2 errors (details), DVE, BA, S: out of memory
SS: 33 min 38 sec (T) 		S: 2 min 35 sec (F)
SS: 1 min 11 sec (F)
The bakery algorithm 2 processes, MAX[?] = 9, DVE*, BA 2 processes, MAX[?] = 6, 1 error (details), DVE*, BA S: > 1 day
SS: 57 min 55 sec (F) 		S: > 1 day
SS: > 1 day
The dining philosophers, version 1 4 processes , DVE*, BA 4 processes with 1 error: (details), DVE, BA S: > 1 day
SS: 52 sec (F) 		S: > 1 day
SS: > 1 day
The dining philosophers, version 2 4 processes , DVE*, BA 4 processes with 2 errors (details), DVE, BA S: > 1 day
SS: 4 min 50 sec (F) 		S: > 1 day
SS: > 1 day
Fischer's algorithm 3 processes, DVE*, BA 3 processes with 1 error (details), DVE, BA S: > 1 day
SS: > 1 day 		S: > 1 day
SS: > 1 day

*: The model is obtained from the BEEM [1] database.

Setting 2: All states are accepting. (tgz)

Model OriginalError L(O)⊇L(E) L(O)⊆L(E)
Peterson's protocol 2 processes , DVE, BA 2 processes with 1 error (details), DVE, BA S: 2.1 sec (T)
SS: 0.43 sec (T) 		S: 0.17 sec (F)
SS: 0.08 sec (F)
The MCS algorithm 3 processes, DVE*, BA 3 processes with 2 errors (details), DVE, BA, S: out of memory
SS: 25 min 55 sec (T) 		S: 3 min 10 sec (F)
SS: 1 min 39 sec (F)
The bakery algorithm 2 processes, MAX[?] = 9, DVE*, BA 2 processes, MAX[?] = 6, 1 error (details), DVE*, BA S: > 1 day
SS: 2 min 47 sec (F) 		S: > 1 day
SS: 20 min (F)
The dining philosophers, version 1 4 processes , DVE*, BA 4 processes with 1 error: (details), DVE, BA S: 1 min 18 sec (F)
SS: 3.7 sec (F) 		S: > 1 day
SS: > 1 day
The dining philosophers, version 2 4 processes , DVE*, BA 4 processes with 2 errors (details), DVE, BA S: 3 min 1 sec (F)
SS: 5 sec (F) 		S: > 1 day
SS: > 1 day
Fischer's algorithm 3 processes, DVE*, BA 3 processes with 1 error (details), DVE, BA S: > 1 day
SS: > 1 day 		S: > 1 day
SS: 14 hours 4 mins (F)

*: The model is obtained from the BEEM [1] database.

REFERENCES

  1. R Pelanek : BEEM: BEnchmarks for Explicit Model checkers (February 2007), http://anna.fi.muni.cz/models/index.html
  2. DiVinE - Distributed Verification Environment, Masaryk University Brno, http://anna.fi.muni.cz/divine-mc/
  3. S Fogarty, MY Vardi : Efficient Büchi Universality Checking - in Proc. of TACAS, 2010.
  4. D Tabakov, MY Vardi : Model Checking Büchi Specifications - in Proc. of LATA, 2007.