Authors: Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen Tiu
Paper Information
Title: | Quasi-Open Bisimilarity with Mismatch is Intuitionistic |
Authors: | Ki Yung Ahn, Ross Horne, Shang-Wei Lin and Alwen Tiu |
Proceedings: | LICS PDF files |
Editors: | Anuj Dawar and Erich Grädel |
Keywords: | pi-calculus, bisimulation, intuitionistic logic, modal logic, mechanised theorem proving |
Abstract: | ABSTRACT. Quasi-open bisimilarity is the coarsest notion of bisimilarity for the pi-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity allows fresh names to be manufactured to provide constructive evidence that an inequality holds. The extension of quasi-open bisimilarity is canonical and robust --- coinciding with open barbed bisimilarity (an objective notion of bisimilarity congruence) and characterised by an intuitionistic variant of an established modal logic. The more famous open bisimilarity is also considered, for which the coarsest extension for handling mismatch is identified. Applications to symbolic equivalence checking and symbolic model checking are highlighted, e.g., for verifying privacy properties. Theorems and examples are mechanised using the proof assistant Abella. |
Pages: | 10 |
Talk: | Jul 09 15:00 (Session 49E) |
Paper: |