判定CTL与LTL的公共片段（含过去时算子）

语言理论的一个核心目标是通过理解形式化的相对表达能力来比较它们。这方面的一个挑战性问题是确定两个形式化 $F_1$ 和 $F_2$ 的\emph{公共片段}，即有效地刻画可以在两种形式化中表达的属性类 $F_1\cap F_2$。与此密切相关的一个问题是\emph{成员资格问题}，记为 $F_1 \membership F_2$，询问以 $F_1$ 表达的属性是否也能用 $F_2$ 表达。当涉及\emph{分支时间}形式化时，这些问题变得特别困难。在这项工作中，我们证明了 $\LTL \cap \PCTL$ 是可判定的，其中 \PCTL 表示 \CTL 扩展了\emph{过去时算子}。我们通过证明两个成员资格问题 $\LTL \membership \PCTL$ 和 $\PCTL \membership \LTL$ 都是可判定的来做到这一点。方向 $\PCTL \membership \LTL$ 遵循已知结果的适当组合。相反的方向 $\LTL \membership \PCTL$ 需要 \PCTL 的自动机理论刻画。具体来说，我们引入了一类新的自动机，称为\emph{无计数器犹豫弱树自动机}（$\HWTcf$），它精确地捕捉了 \PCTL 的表达能力，并且是通过结合交替奇偶树自动机上的两个正交限制，即\emph{无计数器犹豫性}和\emph{弱性}而获得的。我们证明，对于由 \LTL 公式定义的每个单词语言 $L$，相关的树语言 $\triangle[L]$ 能被 \HWTcf 识别，当且仅当 $L$ 能被 \DBW 识别。由于后者的可识别性问题是可判定的，前者也是如此。这一结果推进了判定 $\LTL \cap \CTL$ 这一长期悬而未决的问题。实际上，该问题现在可以归约为 $\PCTL \membership \CTL$，即何时可以消除过去时算子的问题。