Succinct graph representations of µcalculus formulas
Kupke, Clemens and Marti, Johannes and Venema, Yde; Manea, Florin and Simpson, Alex, eds. (2022) Succinct graph representations of µcalculus formulas. In: 30th EACSL Annual Conference on Computer Science Logic, CSL 2022. Leibniz International Proceedings in Informatics, LIPIcs . Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing, DEU. ISBN 9783959772181 (https://doi.org/10.4230/LIPIcs.CSL.2022.29)
Preview 
Text.
Filename: Kupke_etal_EACSL_2022_Succinct_graph_representations_of_calculus_formulas.pdf
Final Published Version License: Download (875kB) Preview 
Abstract
Many algorithmic results on the modal mucalculus 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 mucalculus formula. We propose the notion of a parity formula as a natural way of representing a mucalculus 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 wellknown size measures for mucalculus 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 FischerLadner 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 blowup 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 alternationdepth but (c) does not assume the input formula to be clean.


Item type: Book Section ID code: 79928 Dates: DateEvent19 February 2022Published1 February 2022Published Online30 September 2021AcceptedKeywords: alternating tree automata, hierachical equation systems, modal mucalculus, model checking, Electronic computers. Computer science, Software Subjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 22 Mar 2022 10:43 Last modified: 12 May 2022 00:12 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/79928