University of Oxford (UK)
VLTS benchmark suite
CADP (Construction and Analysis of Distributed Processes)
up to 33,949,609 states and 165,318,222 transitions.
Many different variations on bisimulation have been described in the
literature on process algebra. They are typically used to characterise
equivalences between nodes of a labelled transition system (LTS), but
they can also be used to calculate state-reduced LTSs that represent
equivalent processes. This work introduces novel algorithms for
computing maximal divergence-respecting delay bisimulations (DRDB) and
divergence-respecting weak bisimulations (DRWB) based on dynamic
programming and incorporating the idea of change tracking originally
introduced in the context of strong bisimulation.
An extensive set of tests was carried out to compare the performances of the proposed algorithms implemented in FDR3 to each other, as well as to implementations provided by the BCG_MIN tool of CADP. The primary source for example LTSs is the Very Large Transition Systems (VLTS) Benchmark Suite provided alongside CADP. Regarding strong bisimulation, CADP's implementation was comparable to the FDR3 change-tracking iterative refinement with sorted vectors, performing better on some examples and worse on others. Regarding weak bisimulation, the approach used by CADP consisting in reducing by branching bisimulation followed by weak bisimulation was found to be slower or faster depending on the example.
This study has shown that explicitly constructing a tau-closed
transition relation for weak bisimulations (the current state of the
art) is prohibitively memory-intensive and provided an efficient
alternative based on dynamic programming that is particularly
effective when used in conjunction with change-tracking iterative
refinement. CADP's attempt to reduce this potential explosion by
applying branching bisimulation reduction first, thus reducing the
size of the input to weak bisimulation, was effective in some cases,
but not others. The proposed approach brings a useful contribution,
since it is able to cope with large transition systems without
requiring them to be pre-compressed by a more time-efficient
A. Boulgakov, T. Gibson-Robinson, and A. W. Roscoe.
Computing Maximal Weak and Other Bisimulations.
Formal Aspects of Computing 28(3):381-407, May 2016.
Available on-line from https://www.cs.ox.ac.uk/files/8113/Bisimulation%20FAoC%20Revisions%205.pdf
and from the CADP Web site in PDF or PostScript
Department of Computer Science
University of Oxford
Robert Hooke Building, Parks Road
Oxford OX1 3PR
Tel: +44 (0)1865 610753
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|