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
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 treesFile 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.
