CaRet With Forgettable Past

We study the extension of the full logic CaRet with the unary regular modality N (which reads “from now on”) which allows to model forgettable past. For such an extension, denoted NCaRet, we show the following: (1) NCaRet is expressively complete for the first-order fragment of MSOμ, which extend MSO over words with a binary matching predicate, (2) satisfiability and pushdown model checking are 2Exptime-complete, and (3) pushdown model checking against the regular fragment of NCaRet remains 2Exptime-hard.