Forgetting the Time in Timed Process Algebra - Appendix

Equivalence Proof

We have proven that partially timed branching bisimilarity is an equivalence relation. The proof can be found here.


The µCRL toolset version 2.18.5 for Linux extended with techniques supporting absolute time stamps can be downloaded here.

The LTSmin toolset can be downloaded here. Instructions how to use the toolset can also be found there.

The µCRL specification and .tbf file of the sliding window protocol case study can be downloaded here.

For instructions how to use the µCRL modelling language see the official website.

How to compile the µCRL toolset

Unpack the tool archive and cd to the main folder. We recommend compiling the µCRL toolset

by typing the following at the command line (as root):

1. ./configure --enable-development

2. ./make

3. ./make install

Action-hiding actions in a specification

At the bottom of the specification, the initialisation line is written. Let's call this line init.

To action-hide actions in a set I, change this line to the following:

hide( I, init )

How to obtain the .tbf file from the specification

The .tbf file (which is a linearised version of the µCRL specification)

of the specification without action-hidden actions is provided in the case study package above.

It can be generated from the µCRL specification with some additional optimisations, by typing the following

at the command line:

mcrl -stdout -regular -nocluster slidingwindow_nrm.mcrl | constelm | parelm | sumelm | constelm | stategraph | constelm > slidingwindow_nrm.tbf

How to use the generation algorithm in the µCRL toolset

Type the following at the command line to run the generation algorithm with support

for absolute time stamps (use option -local for a local, i.e. not distributed, generation;

for a distributed generation, write the names of the n machines you want to use in a

file ~/hosts (this n must match the n in the minimisation phase later on)):

Exhaustive breadth-first generation

instantiators (-local) -abstime slidingwindow_nrm.tbf

Time-hiding transitions in an LTS

Once the LTS is obtained (in a directory called slidingwindow_nrm.dmp), we can time-hide some of

the transition labels as follows:

1. convert the directory to one of type '.dir' as follows:

dmp2dir slidingwindow_nrm

2. create a new text file called 'thideset' in the directory where the .dir directory is located, and write

the transition labels you want to time-hide in this file, one label per line;

3. now, the following command will create the time-hidden LTS:

ltscp slidingwindow_nrm.dir slidingwindow_nrm.ath

Once the new LTS is created, please rename slidingwindow_nrm.ath to something with a .dir extension.

Minimising an LTS

We describe two ways to minimise an LTS 'a.dir' in .dir format.

1. For a local, i.e. not distributed, minimisation method to a file 'a2.dir', use the ltsmin tool:

Local strong bisimulation reduction:

ltsmin -s a.dir a2.dir

Local branching bisimulation reduction:

ltsmin -b a.dir a2.dir

2. For a distributed minimisation method, use the ltsmin-mpi tool of the LTSmin toolset

(note that n-1 after -np relates to the n from the generation phase):

Distributed strong bisimulation reduction:

mpirun -np n-1 -hostfile <hostfile> -mca blt tcp,self ltsmin-mpi -s <path to a.dir> <path to a2.dir>

Distributed branching bisimulation reduction:

mpirun -np n-1 -hostfile <hostfile> -mca blt tcp,self ltsmin-mpi -b <path to a.dir> <path to a2.dir>