License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.198
URN: urn:nbn:de:0030-drops-53823
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5382/
Parrow, Joachim ;
Borgström, Johannes ;
Eriksson, Lars-Henrik ;
Gutkovas, Ramunas ;
Weber, Tjark
Modal Logics for Nominal Transition Systems
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. 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.
BibTeX - Entry
@InProceedings{parrow_et_al:LIPIcs:2015:5382,
author = {Joachim Parrow and Johannes Borgstr{\"o}m and Lars-Henrik Eriksson and Ramunas Gutkovas and Tjark Weber},
title = {{Modal Logics for Nominal Transition Systems}},
booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)},
pages = {198--211},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-91-0},
ISSN = {1868-8969},
year = {2015},
volume = {42},
editor = {Luca Aceto and David de Frutos Escrig},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5382},
URN = {urn:nbn:de:0030-drops-53823},
doi = {10.4230/LIPIcs.CONCUR.2015.198},
annote = {Keywords: Process algebra, nominal sets, bisimulation, modal logic}
}
Keywords: |
|
Process algebra, nominal sets, bisimulation, modal logic |
Collection: |
|
26th International Conference on Concurrency Theory (CONCUR 2015) |
Issue Date: |
|
2015 |
Date of publication: |
|
26.08.2015 |