Modal Logics for Nominal Transition Systems

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. In Marino Miculan, editor, MeMo 2015 - 2nd International Workshop on Meta Models for Process Languages, Grenoble, June 5, 2015, Part of DisCoTec 2015, pages 44-61, 2015.

Abstract

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. 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.

Download

BibTeX

@inproceedings{parrow15modal-memo,
  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    = {Marino Miculan},
  booktitle = {MeMo 2015~-- 2nd International Workshop on Meta Models for Process Languages, Grenoble, June~5, 2015, Part of DisCoTec 2015},
  pages     = {44--61},
  year      = {2015},
  url       = {https://webconf.inrialpes.fr/wp-content/uploads/sites/9/2015/06/memo2015-preproc.pdf}
}

Note

A revised version of this paper is available.


Last modified: 2016-07-06