Modal Logics for Nominal Transition Systems

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. Technical Report 2015-021, Department of Information Technology, Uppsala University, June 2015. Accepted for CONCUR 2015. This version includes proofs in an appendix.


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},
  number      = {2015-021},
  institution = {Department of Information Technology, Uppsala University},
  department  = {Computing Science Division},
  month       = jun,
  year        = {2015},
  note        = {Accepted for CONCUR 2015. This version includes proofs in an appendix.}


A conference version of this paper is available.

Last modified: 2016-07-06