This paper deals with the extension of Kozen's μ-calculus with the so-called “existential bisimulation quantifier”. By using this quantifier one can express the uniform interpolant of any formula of the μ-calculus. In this work we provide an explicit form for the uniform interpolant of a disjunctive formula and see that it belongs to the same level of the fixpoint alternation hierarchy of the μ-calculus than the original formula. We show that this result cannot be generalized to the whole logic, because the closure of the third level of the hierarchy under the existential bisimulation quantifier is the whole μ-calculus. However, we prove that the first two levels of the hierarchy are closed. We also provide the μ-logic extended with the bisimulation quantifier with a complete calculus.

On modal $mu$-calculus with explicit interpolants

LENZI, Giacomo;
2006-01-01

Abstract

This paper deals with the extension of Kozen's μ-calculus with the so-called “existential bisimulation quantifier”. By using this quantifier one can express the uniform interpolant of any formula of the μ-calculus. In this work we provide an explicit form for the uniform interpolant of a disjunctive formula and see that it belongs to the same level of the fixpoint alternation hierarchy of the μ-calculus than the original formula. We show that this result cannot be generalized to the whole logic, because the closure of the third level of the hierarchy under the existential bisimulation quantifier is the whole μ-calculus. However, we prove that the first two levels of the hierarchy are closed. We also provide the μ-logic extended with the bisimulation quantifier with a complete calculus.
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/1954287
 Attenzione

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

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