Joachim Parrow ; Johannes Borgström ; Lars-Henrik Eriksson ; Ramūnas Forsberg Gutkovas ; Tjark Weber - Modal Logics for Nominal Transition Systems

lmcs:5353 - Logical Methods in Computer Science, January 28, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:6)2021
Modal Logics for Nominal Transition SystemsArticle

Authors: Joachim Parrow ; Johannes Borgström ; Lars-Henrik Eriksson ; Ramūnas Forsberg Gutkovas ; Tjark Weber

    We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.


    Volume: Volume 17, Issue 1
    Published on: January 28, 2021
    Accepted on: November 13, 2020
    Submitted on: April 5, 2019
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1358 times.
    This article's PDF has been downloaded 258 times.