DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2022.64

Countdown μ-Calculus

Authors: Jędrzej Kołodziejski and Bartek Klin

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract

We introduce the countdown μ-calculus, an extension of the modal μ-calculus with ordinal approximations of fixpoint operators. In addition to properties definable in the classical calculus, it can express (un)boundedness properties such as the existence of arbitrarily long sequences of specific actions. The standard correspondence with parity games and automata extends to suitably defined countdown games and automata. However, unlike in the classical setting, the scalar fragment is provably weaker than the full vectorial calculus and corresponds to automata satisfying a simple syntactic condition. We establish some facts, in particular decidability of the model checking problem and strictness of the hierarchy induced by the maximal allowed nesting of our new operators.

Cite as

Jędrzej Kołodziejski and Bartek Klin. Countdown μ-Calculus. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kolodziejski_et_al:LIPIcs.MFCS.2022.64,
  author =	{Ko{\l}odziejski, J\k{e}drzej and Klin, Bartek},
  title =	{{Countdown \mu-Calculus}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{64:1--64:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.64},
  URN =		{urn:nbn:de:0030-drops-168624},
  doi =		{10.4230/LIPIcs.MFCS.2022.64},
  annote =	{Keywords: countdown \mu-calculus, games, automata}
}

Search Results

Documents authored by Kołodziejski, Jędrzej

Countdown μ-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message