Quasi-open bisimilarity with mismatch is intuitionistic

Ross Horne; Ki Yung Ahn; Shang-wei Lin; Alwen Tiu

doi:10.1145/3209108.3209125

Quasi-open bisimilarity with mismatch is intuitionistic

Ross Horne, Ki Yung Ahn, Shang-wei Lin, Alwen Tiu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

11 Citations (Scopus)

18 Downloads (Pure)

Abstract

Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-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 checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.

Original language	English
Title of host publication	Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18)
Publisher	Association for Computing Machinery (ACM)
Pages	26-35
Number of pages	10
ISBN (Print)	9781450355834
DOIs	https://doi.org/10.1145/3209108.3209125
Publication status	Published - 9 Jul 2018
Event	33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18 - Oxford , United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Conference

Conference	33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18
Abbreviated title	LICS '18
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

Keywords

mismatch
bisimilarity
intuitionistic modal logic
theory of computation
process calculi
modal and temporal logics

Access to Document

10.1145/3209108.3209125

Horne-etal-LICS2018-Quasi-open-bisimilarity-mismatch-intuitionisticAccepted author manuscript, 733 KB

https://satoss.uni.lu/members/ross/pdf/lics18.pdf

Cite this

@inproceedings{7a1737031abe44a19125cdd7c94415ce,

title = "Quasi-open bisimilarity with mismatch is intuitionistic",

abstract = "Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-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 checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.",

keywords = "mismatch, bisimilarity, intuitionistic modal logic, theory of computation, process calculi, modal and temporal logics",

author = "Ross Horne and Ahn, {Ki Yung} and Shang-wei Lin and Alwen Tiu",

note = "Copyright {\textcopyright} 2018 ACM Ross Horne, Ki Yung Ahn, Shang-wei Lin, and Alwen Tiu. 2018. Quasi-Open Bisimilarity with Mismatch is Intuitionistic . In Proceedings of LICS {\textquoteright}18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9–12, 2018 (LICS {\textquoteright}18), 10 pages. https://doi.org/10.1145/3209108.3209125 ; 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18, LICS '18 ; Conference date: 09-07-2018 Through 12-07-2018",

year = "2018",

month = jul,

day = "9",

doi = "10.1145/3209108.3209125",

language = "English",

isbn = "9781450355834",

pages = "26--35",

booktitle = "Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18)",

publisher = "Association for Computing Machinery (ACM)",

address = "United States",

}

Horne, R, Ahn, KY, Lin, S & Tiu, A 2018, Quasi-open bisimilarity with mismatch is intuitionistic. in Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18). Association for Computing Machinery (ACM), pp. 26-35, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18, Oxford , United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209125

Quasi-open bisimilarity with mismatch is intuitionistic. / Horne, Ross; Ahn, Ki Yung; Lin, Shang-wei et al.
Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18). Association for Computing Machinery (ACM), 2018. p. 26-35.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Quasi-open bisimilarity with mismatch is intuitionistic

AU - Horne, Ross

AU - Ahn, Ki Yung

AU - Lin, Shang-wei

AU - Tiu, Alwen

N1 - Copyright © 2018 ACM Ross Horne, Ki Yung Ahn, Shang-wei Lin, and Alwen Tiu. 2018. Quasi-Open Bisimilarity with Mismatch is Intuitionistic . In Proceedings of LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9–12, 2018 (LICS ’18), 10 pages. https://doi.org/10.1145/3209108.3209125

PY - 2018/7/9

Y1 - 2018/7/9

N2 - Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-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 checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.

AB - Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-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 checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.

KW - mismatch

KW - bisimilarity

KW - intuitionistic modal logic

KW - theory of computation

KW - process calculi

KW - modal and temporal logics

U2 - 10.1145/3209108.3209125

DO - 10.1145/3209108.3209125

M3 - Conference contribution book

SN - 9781450355834

SP - 26

EP - 35

BT - Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18)

PB - Association for Computing Machinery (ACM)

T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18

Y2 - 9 July 2018 through 12 July 2018

ER -

Quasi-open bisimilarity with mismatch is intuitionistic

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this