A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
| Autor: | Dale Miller, Matteo Cimini, Kaustuv Chaudhuri |
|---|---|
| Přispěvatelé: | Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Indiana University [Bloomington], Indiana University System, ACM-SIGPLAN, Xavier Leroy and Alwen Tiu, European Project: 291592,EC:FP7:ERC,ERC-2011-ADG_20110209,PROOFCERT(2012), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Soundness
Bisimulation Computer science ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory Process calculus [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Mathematical proof Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Closure (mathematics) ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.5: Specification techniques Proof theory Metatheory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Calculus Algorithm |
| Zdroj: | 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP) 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), ACM-SIGPLAN, Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693170⟩ CPP |
| DOI: | 10.1145/2676724.2693170⟩ |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|