| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
Abstract : Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the under-lying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the π-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports λ-tree syntax and generic reasoning using the ∇-quantifier, our treatment of the π-calculus is both direct and natural.
Cited literature [27 references]
https://hal.inria.fr/hal-01091524
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, December 5, 2014 - 3:31:01 PM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Monday, March 9, 2015 - 6:03:58 AM
Contributor : Kaustuv Chaudhuri <>
Submitted on : Friday, December 5, 2014 - 3:31:01 PM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Monday, March 9, 2015 - 6:03:58 AM
Files
cpp-hal.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License