We investigate the structure of the modal mu-calculus L-mu with respect to the question of how many different fixed point variables are necessary to define a given property. Most of the logics commonly used in verification, such as CTL, LTL, CTL*, PDL, etc. can in fact be embedded into the two-variable fragment of the mu-calculus. It is also known that the two-variable fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open problem whether the variable hierarchy is strict. Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential (i.e., rectangle-free) formulae. It is known that these characterize precisely the L-mu-definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question whether the finite variable fragments satisfy the existential preservation theorem.

On the variable hierarchy of the modal mu-calculus

LENZI, Giacomo
2002

Abstract

We investigate the structure of the modal mu-calculus L-mu with respect to the question of how many different fixed point variables are necessary to define a given property. Most of the logics commonly used in verification, such as CTL, LTL, CTL*, PDL, etc. can in fact be embedded into the two-variable fragment of the mu-calculus. It is also known that the two-variable fragment can express properties that occur at arbitrarily high levels of the alternation hierarchy. However, it is an open problem whether the variable hierarchy is strict. Here we study this problem with a game-based approach and establish the strictness of the hierarchy for the case of existential (i.e., rectangle-free) formulae. It is known that these characterize precisely the L-mu-definable properties that are closed under extensions. We also relate the strictness of the variable hierarchy to the question whether the finite variable fragments satisfy the existential preservation theorem.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11386/1954315
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 8
social impact