Modal Logics for Nominal Transition Systems
(English)Manuscript (preprint) (Other academic)
We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main 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, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.
modal logic, process calculi, nominal transition system, adequacy, bisimulation
IdentifiersURN: urn:nbn:se:uu:diva-300027OAI: oai:DiVA.org:uu-300027DiVA: diva2:950711