Size measures and alphabetic equivalence in the μcalculus
Kupke, Clemens and Marti, Johannes and Venema, Yde; (2022) Size measures and alphabetic equivalence in the μcalculus. In: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. Proceedings  Symposium on Logic in Computer Science . ACM, ISR. ISBN 9781450393515 (https://doi.org/10.1145/3531130.3533339)
Preview 
Text.
Filename: Kupke_etal_LICS_2022_Size_measures_and_alphabetic_equivalence_in_the_calculus.pdf
Accepted Author Manuscript License: Strathprints license 1.0 Download (768kB) Preview 
Abstract
Algorithms for solving computational problems related to the modal µcalculus generally do not take the formulas themselves as input, but operate on some kind of representation of formulas. This representation is usually based on a graph structure that one may associate with a µcalculus formula. Recent work by Kupke, Marti & Venema showed that the operation of renaming bound variables may incur an exponential blowup of the size of such a graph representation. Their example revealed the undesirable situation that standard constructions, on which algorithms for model checking and satisfability depend, are sensitive to the specifc choice of bound variables used in a formula. Our work discusses how the notion of alphabetic equivalence interacts with the construction of graph representations of µcalculus formulas, and with the induced size measures of formulas. We introduce the condition of ainvariance on such constructions, requiring that alphabetically equivalent formulas are given the same (or isomorphic) graph representations. Our main results are the following. First we show that if two µcalculus formulas are aequivalent, then their respective FischerLadner closures have the same cardinality, up to aequivalence. We then continue with the defnition of an ainvariant construction which represents an arbitrary µcalculus formula by a graph that has exactly the size of the quotient of the closure of the formula, up to aequivalence. This defnition, which is itself based on a renaming of variables, solves the abovementioned problem discovered by Kupke et al.


Item type: Book Section ID code: 81875 Dates: DateEvent5 August 2022Published4 August 2022Published Online14 April 2022AcceptedKeywords: modal mucalculus, complexity, alphabetic equivalence, model checking, Electronic computers. Computer science, Mathematics, Computer Science(all), Computational Mathematics Subjects: Science > Mathematics > Electronic computers. Computer science
Science > MathematicsDepartment: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 16 Aug 2022 09:15 Last modified: 11 Aug 2023 14:54 URI: https://strathprints.strath.ac.uk/id/eprint/81875