Succinct graph representations of µ-calculus formulas

Clemens Kupke, Johannes Marti, Yde Venema

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

4 Citations (Scopus)
23 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publication30th EACSL Annual Conference on Computer Science Logic, CSL 2022
EditorsFlorin Manea, Alex Simpson
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages18
ISBN (Electronic)9783959772181
DOIs
Publication statusPublished - 19 Feb 2022
Event30th EACSL Annual Conference on Computer Science Logic, CSL 2022 - Virtual, Gottingen, Germany
Duration: 14 Feb 202219 Feb 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume216
ISSN (Print)1868-8969

Conference

Conference30th EACSL Annual Conference on Computer Science Logic, CSL 2022
Country/TerritoryGermany
CityVirtual, Gottingen
Period14/02/2219/02/22

Keywords

  • alternating tree automata
  • hierachical equation systems
  • modal mu-calculus
  • model checking

Fingerprint

Dive into the research topics of 'Succinct graph representations of µ-calculus formulas'. Together they form a unique fingerprint.

Cite this