DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2017.30

Modal mu-Calculus with Atoms

Authors: Bartek Klin and Mateusz Lelyk

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.

Cite as

Bartek Klin and Mateusz Lelyk. Modal mu-Calculus with Atoms. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CSL.2017.30,
  author =	{Klin, Bartek and Lelyk, Mateusz},
  title =	{{Modal mu-Calculus with Atoms}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.30},
  URN =		{urn:nbn:de:0030-drops-76991},
  doi =		{10.4230/LIPIcs.CSL.2017.30},
  annote =	{Keywords: modal mu-calculus, sets with atoms}
}

Search Results

Documents authored by Lelyk, Mateusz

Modal mu-Calculus with Atoms

Abstract

Cite as

Thanks for your feedback!

Could not send message