Checking for Open Bisimilarity in the -Calculus
Ulrik Frendrup
February 2001 |

## Abstract:
This paper deals with algorithmic checking of open bisimilarity
in the -calculus. Most bisimulation checking algorithms are based on the
partition refinement approach. Unfortunately the definition of open
bisimulation does not permit us to use a partition refinement approach for
open bisimulation checking directly, but in the paper
A Partition
Refinement Algorithm for the -Calculus Marco Pistore and Davide
Sangiogi present an iterative method that makes it possible to check for open
bisimilarity using partition refinement. We have implemented the algorithm
presented by Marco Pistore and Davide Sangiorgi. Furthermore, we have
optimized this algorithm and implemented this optimized algorithm. The
time-complexity of this algorithm is the same as the time-complexity for the
first algorithm, but performance tests have shown that in many cases the
running time of the optimized algorithm is shorter than the running time of
the first algorithm.
Our implementation of the optimized open bisimulation checker algorithm and a user interface have been integrated in a system called the OBC Workbench. The source code and a manual for it is available from www.cs.auc.dk/research/FS/ny/PR-pi/
Available as |

Last modified: 2003-06-08 by webmaster.