Quasi-open bisimilarity with mismatch is intuitionistic

Ross Horne, Ki Yung Ahn, Shang Wei Lin, Alwen Tiu

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    11 Citations (Scopus)

    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 languageEnglish
    Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
    PublisherInstitute of Electrical and Electronics Engineers Inc.
    Pages26-35
    Number of pages10
    ISBN (Electronic)9781450355834, 9781450355834
    DOIs
    Publication statusPublished - 9 Jul 2018
    Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
    Duration: 9 Jul 201812 Jul 2018

    Publication series

    NameProceedings - Symposium on Logic in Computer Science
    ISSN (Print)1043-6871

    Conference

    Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
    Country/TerritoryUnited Kingdom
    CityOxford
    Period9/07/1812/07/18

    Fingerprint

    Dive into the research topics of 'Quasi-open bisimilarity with mismatch is intuitionistic'. Together they form a unique fingerprint.

    Cite this