We investigate the hybrid extension of CaRet, denoted HyCaRet, obtained by adding the standard existential binder operator ∃. We show that the one variable fragment 1-HyCaRet of HyCaRet is expressively complete for the first-order logic FO μ which extends FO over words with a binary matching predicate. While all the known FO μ -complete and elementary extensions of CaRet can be linearly translated in 1-HyCaRet, 1-HyCaRet can be exponentially more succinct than them. Moreover, the complexity of its satisfiability and pushdown model-checking problems are 2Exptime-complete, which is the same complexity as that of two known FO μ -complete extensions of CaRet suitable for compositional and modular reasoning, namely CaRet + ‘within’ and CaRet + ‘forgettable past’. Finally, we show that for each h ≥ 1, satisfiability and pushdown model-checking of the fragment HyCaRet h of HyCaRet consisting of formulas with nesting depth of ∃ at most h is exactly (h+1)-Exptime-complete.

Hybrid and First-Order Complete Extensions of CaRet

LANOTTE, RUGGERO
2011

Abstract

We investigate the hybrid extension of CaRet, denoted HyCaRet, obtained by adding the standard existential binder operator ∃. We show that the one variable fragment 1-HyCaRet of HyCaRet is expressively complete for the first-order logic FO μ which extends FO over words with a binary matching predicate. While all the known FO μ -complete and elementary extensions of CaRet can be linearly translated in 1-HyCaRet, 1-HyCaRet can be exponentially more succinct than them. Moreover, the complexity of its satisfiability and pushdown model-checking problems are 2Exptime-complete, which is the same complexity as that of two known FO μ -complete extensions of CaRet suitable for compositional and modular reasoning, namely CaRet + ‘within’ and CaRet + ‘forgettable past’. Finally, we show that for each h ≥ 1, satisfiability and pushdown model-checking of the fragment HyCaRet h of HyCaRet consisting of formulas with nesting depth of ∃ at most h is exactly (h+1)-Exptime-complete.
Kai Brunnler, George Metcalfe (Eds)
Lecture Notes in Computer Science
9783642221187
TABLEAUX 2011
Bern, Switzerland
July 4-8, 2011
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/11383/1789323
 Attenzione

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

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