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.
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 )
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
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)):
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>