Deciding the Common Fragment of CTL with Past and LTL

A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determining the \emph{common fragment} of two formalisms $F_1$ and $F_2$, that is, effectively characterise the class $F_1\cap F_2$ of properties that can be expressed in both formalisms. A question closely related to this is the \emph{membership problem}, denoted $F_1\text{membership}{F}_2$, which asks whether a property expressed in $F_1$ can be also expressed in $F_2$. These problems become particularly difficult when \emph{branching-time} formalisms are involved. In this work, we prove that $\text{LTL}\cap \text{PCTL}$ is decidable, where \PCTL denotes \CTL extended with \emph{past operators}. We do this by showing that both membership problems, $\text{LTL}\text{membership}\text{PCTL}$ and $\text{PCTL}\text{membership}\text{LTL}$, are decidable. The direction $\text{PCTL}\text{membership}\text{LTL}$ follows from suitable combinations of known results. The converse direction, $\text{LTL}\text{membership}\text{PCTL}$, requires an automata-theoretic characterisation of $\text{PCTL}$. Specifically, we introduce a new class of automata, called \emph{counter-free hesitant weak tree automata} ($\text{HWTcf}$) that capture precisely the expressiveness of $\text{PCTL}$, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, \emph{counter-free hesitancy} and \emph{weakness}. We prove that, for every word language $L$ defined by an \LTL formula, the associated tree language $\mathrm{△}[L]$ is recognisable by an \HWTcf if and only if $L$ is recognized by a \DBW. Since the latter recognisability problem is decidable, so is the former. This result advances the longstanding open problem of deciding $\text{LTL}\cap \text{CTL}$. Indeed, that problem can now be reduced to $\text{PCTL}\text{membership}\text{CTL}$, that is, the question of when past operators can be eliminated.