Hybrid and First-Order Complete Extensions of CaRet

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.