Abstract. We consider the positive mu-calculus with successors PmS, namely a variant of Kozen's modal mu-calculus L, [9] where negation is suppressed and where the basic modalities are a sequence of successor operators. In particular we are interested in the sublanguages of PmS determined by the value of the Emerson-Lei alternation depth [6]. For every n E N we exhibit a formula r whose expression in PmS requires at least alternation depth n. In particular our result gives a new proof of the strict hierarchy theorem for PmS which follows from [1].
A hierarchy theorem for the mu-calculus
LENZI, Giacomo
1996-01-01
Abstract
Abstract. We consider the positive mu-calculus with successors PmS, namely a variant of Kozen's modal mu-calculus L, [9] where negation is suppressed and where the basic modalities are a sequence of successor operators. In particular we are interested in the sublanguages of PmS determined by the value of the Emerson-Lei alternation depth [6]. For every n E N we exhibit a formula r whose expression in PmS requires at least alternation depth n. In particular our result gives a new proof of the strict hierarchy theorem for PmS which follows from [1].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.
