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.
Our programs are tested on OpenJDK 64Bit Server VM and Java HotSpot(TM) 64Bit 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 TestUsage: java jar jar_file Aut_file TimeoutThe 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 TestUsage: java jar jar_file Aut1_file Aut2_file TimeoutThe 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 "tdadno.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.
*
The execution times are stored separately respectively for the universal and the nonuniversal 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,
** U for "Universal", N for "Nonuniversal", 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.
* The execution times are summed up respectively for the universal and the nonuniversal 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 "lengthprops.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.
* The execution times are summed up respectively for the universal and the nonuniversal 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:
How to translate a DVE model to a Büchi automatonFor 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, {25532}]\n[0,2]\n[3, 3]"In this state, the values of global variables are 0 and {25532} (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.
The BA file formatFor 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 fileAssume that in the DOT file there is a transition"[0, {25532}]\n[0]\n[3]\n[2]\n[1]">"[0, {25521}]\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 25532][0][3][2][1] to state [0 25521][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 25532][0][3][2][1]>[0 25521][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)
*: The model is obtained from the BEEM [1] database. Setting 2: All states are accepting. (tgz)
