Computing Maximal Weak and Other Bisimulations

Organisation:	University of Oxford (UK)
Method:	VLTS benchmark suite
Tools used:	FDR3 CADP (Construction and Analysis of Distributed Processes)
Domain:	Concurrency Theory.
Period:	2016
Size:	up to 33,949,609 states and 165,318,222 transitions.
Description:	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.
Conclusions:	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 compression.
Publications:	[Boulgakov-GibsonRobinson-Roscoe-16] 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
Contact:	Thomas Gibson-Robinson Senior Researcher Department of Computer Science University of Oxford Robert Hooke Building, Parks Road Oxford OX1 3PR United Kingdom Tel: +44 (0)1865 610753 Email: thomas.gibson-robinson@cs.ox.ac.uk
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page