Document

**Published in:** LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Many algorithmic results on the modal mu-calculus use representations of formulas such as alternating tree automata or hierarchical equation systems. At closer inspection, these results are not always optimal, since the exact relation between the formula and its representation is not clearly understood. In particular, there has been confusion about the definition of the fundamental notion of the size of a mu-calculus formula.
We propose the notion of a parity formula as a natural way of representing a mu-calculus formula, and as a yardstick for measuring its complexity. We discuss the close connection of this concept with alternating tree automata, hierarchical equation systems and parity games. We show that well-known size measures for mu-calculus formulas correspond to a parity formula representation of the formula using its syntax tree, subformula graph or closure graph, respectively. Building on work by Bruse, Friedmann & Lange we argue that for optimal complexity results one needs to work with the closure graph, and thus define the size of a formula in terms of its Fischer-Ladner closure. As a new observation, we show that the common assumption of a formula being clean, that is, with every variable bound in at most one subformula, incurs an exponential blow-up of the size of the closure.
To realise the optimal upper complexity bound of model checking for all formulas, our main result is to provide a construction of a parity formula that (a) is based on the closure graph of a given formula, (b) preserves the alternation-depth but (c) does not assume the input formula to be clean.

Clemens Kupke, Johannes Marti, and Yde Venema. Succinct Graph Representations of μ-Calculus Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kupke_et_al:LIPIcs.CSL.2022.29, author = {Kupke, Clemens and Marti, Johannes and Venema, Yde}, title = {{Succinct Graph Representations of \mu-Calculus Formulas}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.29}, URN = {urn:nbn:de:0030-drops-157491}, doi = {10.4230/LIPIcs.CSL.2022.29}, annote = {Keywords: modal mu-calculus, model checking, alternating tree automata, hierachical equation systems} }

Document

**Published in:** LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.

Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform Interpolation for Coalgebraic Fixpoint Logic. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 238-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{marti_et_al:LIPIcs.CALCO.2015.238, author = {Marti, Johannes and Seifan, Fatemeh and Venema, Yde}, title = {{Uniform Interpolation for Coalgebraic Fixpoint Logic}}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)}, pages = {238--252}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-84-2}, ISSN = {1868-8969}, year = {2015}, volume = {35}, editor = {Moss, Lawrence S. and Sobocinski, Pawel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.238}, URN = {urn:nbn:de:0030-drops-55379}, doi = {10.4230/LIPIcs.CALCO.2015.238}, annote = {Keywords: mu-calculus, uniform interpolation, coalgebra, automata} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail