Size measures and alphabetic equivalence in the μ-calculus

Clemens Kupke, Johannes Marti, Yde Venema

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

2 Downloads (Pure)

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 blow-up 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 a-invariance 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 a-equivalent, then their respective FischerLadner closures have the same cardinality, up to a-equivalence. We then continue with the defnition of an a-invariant 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 a-equivalence. This defnition, which is itself based on a renaming of variables, solves the above-mentioned problem discovered by Kupke et al.

Original languageEnglish
Title of host publicationProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Subtitle of host publicationProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationNew York, NY, USA
Number of pages13
ISBN (Electronic)9781450393515
DOIs
Publication statusPublished - 5 Aug 2022
Event37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) - Technion, Haifa, Israel
Duration: 2 Aug 20225 Aug 2022
https://lics.siglog.org/lics22/

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Country/TerritoryIsrael
CityHaifa
Period2/08/225/08/22
Internet address

Keywords

  • modal mu-calculus
  • complexity
  • alphabetic equivalence
  • model checking

Fingerprint

Dive into the research topics of 'Size measures and alphabetic equivalence in the μ-calculus'. Together they form a unique fingerprint.

Cite this