Deciding the Common Fragment of CTL with Past and LTL

問題提起
本論文は、言語理論における根本的な問題である、2つの形式体系 $F_1$ と $F_2$ の共通部分を決定することに取り組んでいる。具体的には、線形時相論理（LTL）と計算木論理（CTL）の交差に焦点を当てており、これは40年近く未解決のまま残されている問題である。著者らはこれをメンバーシップ問題として定式化している。すなわち、ある形式体系で表現された性質が、もう一方の形式体系（あるいはそれらの交差）において等価に表現可能であるかどうかという問題である。この困難さは、分岐時相の形式体系が関与することによって増大する。これらは、線形時間の理論に見られるような同等の代数的特性を一般に欠いている。$CTL^* \to LTL$ の決定可能性は既知であるが、逆方向の $LTL \to CTL$ および交差 $LTL \cap CTL$ の特徴付けは依然として未解明である。

手法
著者らはオートマトン理論的アプローチを採用し、counter-free hesitant weak tree automata (HWTcf) と呼ばれる新しいクラスのオートマトンを導入している。このモデルは、交互作用を持つパリティ木オートマトン（alternating parity tree automata）に対して、2つの直交する制限を課すことで構築される。

1. 弱さ（Weakness）: 遷移グラフの強連結成分が単一の優先度を持つように受理条件を制限すること（これは Weak MSO および alternation-free $\mu$-calculus に関連する）。
2. Counter-free Hesitancy: カウンティング能力を排除し、特定の「hesitant（躊躇する）」挙動を強制するために構造を制限すること（これは $CTL^*$ および Monadic Path Logic に関連する）。

手法は主に以下の3つのフェーズで進行する：

1. 論理的特徴付け: 著者らは、HWTcf が PCTL（過去演算子が拡張された CTL）と実質的に等価であることを確立する。彼らは、universal HWTcf が APCTL（普遍的なパス量化のみ）に対応し、existential HWTcf が EPCTL に対応することを証明する。
2. オートマトン問題への帰着: 著者らは、論理的なメンバーシップ問題をオートマトン理論的な問題へと結びつける Rabin の還元定理を利用する。具体的には、分岐時相論理の交差におけるメンバーシップを判定することは、パリティ木オートマトンを等価な弱交互作用木オートマトン（$APT \to AWT$）で置き換えられるかどうかを判定することに帰着することを示す。
3. 決定可能性の証明: LTL で定義可能な語の言語と木の言語との関係を分析することにより、木の言語 $\triangle[L]$（木のすべてのパスが LTL 言語 $L$ に属する）が HWTcf によって認識可能であるための必要十分条件は、$L$ が決定性 counter-free Büchi 語オートマトン（DBWcf）によって認識可能であることであることを証明する。

主な貢献と結果

• HWTcf と PCTL の等価性: 本論文は、HWTcf と PCTL が実質的に等価な形式体系であることを証明している（定理2）。これにより、HWTcf が正確に $CTL^*$ と alternation-free $\mu$-calculus ($AFL_\mu$) の交差を捉えるという予想に基づき、PCTL がその自然な論理的候補であることを特定している。
• $LTL \leftrightarrow PCTL$ の決定可能性: 著者らは、$LTL \to PCTL$ および $PCTL \to LTL$ の両方のメンバーシップ問題が決定可能であることを証明している（定理5）。
  • $LTL \to PCTL$ は ExpSpace に属し、PSpace-hard であることが示されている。この証明は、LTL 式が定義する木の言語が HWTcf によって認識可能であるための必要十分条件は、その基礎となる語の言語が DBWcf によって認識可能であることである、という事実に依拠している。
  • $PCTL \to LTL$ は、$ObligationCTL^*$ フラグメントへの帰着と $CTL^* \to LTL$ に関する既存のアルゴリズムを通じて決定可能である。
• 共通部分の特徴付け: 本論文は、$LTL \cap APCTL = LTL \cap PCTL = LTL \cap AFL_\mu$ という等式を確立している（定理4）。注目すべきは、この結果が、過去演算子が許容される場合、LTL との交差においては存在的なパス量化は不要であることを示唆している。すなわち、共通部分は普遍的なパス量化と過去演算子のみを用いて捉えることができる。
• $LTL \to CTL$ 問題の帰着: 著者らは、$PCTL \to CTL$ の決定可能性が $LTL \to CTL$ の決定可能性を導くことを示している（系6）。これにより、40年来の未解決問題である $LTL \cap CTL$ を、PCTL 式から等価な CTL 式を得るための過去演算子の除去という問題へと再構成している。
• 表現力の境界: 本論文は、PCTL が一階述語論理（FO）よりも厳密に表現力が高く、Weak Tree Logic（WMTL、既知の Weak MSO のフラグメント）よりも厳密に表現力が低いことを示している。その結果、現在知られている WMSO のフラグメントの中で、PCTL と表現的に等価なものは存在しない（定理7）。

意義
本論文は、過去演算子の観点を通じた新しい視点を提供することで、LTL と CTL の共通部分を決定するという長年の未解決問題を進展させると主張している。$LTL \to PCTL$ の決定可能性を証明することにより、著者らは元の問題を、過去演算子を除去するという分岐時相の問題（$PCTL \to CTL$）へと帰着させている。これは、$LTL \cap CTL$ 問題を解決するための、より扱いやすい経路を提供している。なぜなら、過去の除去に関する部分的なケースは、他の研究ですでに進展が見られているからである。

さらに、HWTcf の導入は、パス量化された論理と弱モノディック論理との交差の構造的な特徴付けを提供する。著者らは、HWTcf が正確に $CTL^* \cap AFL_\mu$（または $MPL \cap WMSO$）を捉えるという予想（予想1）を維持しているが、この予想を完全に解決せずとも、このオートマトンクラスが線形/分岐時相のインターフェースに対して重要な決定可能性の結果をもたらすことを示している。本研究は、パス量化された木時相論理における過去演算子の予期せぬ力を浮き彫りにしている。すなわち、過去演算子は、LTL との交差において PCTL を標準的な CTL から区別する特徴である「存在的なパス量化」を必要とせずに、複雑な交互作用を捉えることができるのである。