We consider the propositional modal mu-calculus, a logic proposed by Kozen in 1983. In this logic two operators µ and ν are present, which express the least and greatest fixpoints of monotone operators on sets. Bradfield in 1998 proved for any n the existence of a mu-calculus formula that requires n alternations of µ and ν. In this paper we consider the particular case n = 3 and we exhibit a new formula requiring 3 alternations. Our proof is independent of the technique of Bradfield, and is based on a new kind of game on infinite trees

Mu--depth 3 is more than 2: a game-theoretic proof

LENZI, Giacomo
2001-01-01

Abstract

We consider the propositional modal mu-calculus, a logic proposed by Kozen in 1983. In this logic two operators µ and ν are present, which express the least and greatest fixpoints of monotone operators on sets. Bradfield in 1998 proved for any n the existence of a mu-calculus formula that requires n alternations of µ and ν. In this paper we consider the particular case n = 3 and we exhibit a new formula requiring 3 alternations. Our proof is independent of the technique of Bradfield, and is based on a new kind of game on infinite trees
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: https://hdl.handle.net/11386/1954313
 Attenzione

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

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