Checking for Open Bisimilarity in the pi-Calculus
DOI:
https://doi.org/10.7146/brics.v8i8.20463Resumé
This paper deals with algorithmic checking of open bisimilarity in the pi-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 pi-Calculus' Marco Pistore and Davide Sangiorgi 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 http://www.cs.auc.dk/research/FS/ny/PR-pi/.
Downloads
Publiceret
Citation/Eksport
Nummer
Sektion
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).