Modal Logics for Nominal Transition Systems

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1-4, 2015, volume 42 of LIPIcs, pages 198-211. Schloss Dagstuhl Leibniz-Zentrum fuer Informatik, 2015.


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 and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.



  author    = {Joachim Parrow and Johannes Borgstr{\"{o}}m and Lars{-}Henrik Eriksson and Ram{\={u}}nas Gutkovas and Tjark Weber},
  title     = {Modal Logics for Nominal Transition Systems},
  editor    = {Luca Aceto and David de Frutos{-}Escrig},
  booktitle = {26th International Conference on Concurrency Theory, {CONCUR} 2015, Madrid, Spain, September~1-4, 2015},
  volume    = {42},
  series    = {LIPIcs},
  pages     = {198--211},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2015},
  url       = {},
  doi       = {10.4230/LIPIcs.CONCUR.2015.198}

Last modified: 2016-07-06