Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

技術的サマリー：データ単語上の二変数論理における集合オートマトンと決定可能性の限界

問題提起
本論文は、データ単語上の二変数一階論理（$FO_2$）の拡張に対する充足可能性問題の決定可能性に取り組む。データ単語とは、有限アルファベット $\Sigma$ から来る $a_i$ と無限領域 $D$ から来る $d_i$ の対 $(a_i, d_i)$ の有限列であり、$D$ 上でテスト可能な性質は等号のみである。データ単語上の標準的な $FO_2$ 論理（順序、後続、データ等号を含む）は決定可能であることが知られている（具体的には $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1]$ である）。しかし、著者らは、この論理にガード付き正則述語を追加した場合の決定可能性の限界を調査する。

これらの述語 $eL(x, y)$は、位置$x$と$y$が同じデータクラスに属し（すなわち$x \sim y$）、かつそれらの間の文字列の因子が正則言語$L$に属する場合に真となる。中心的な問いは、これらの述語に使用される正則言語の族を認識するモノイド（または半群）$M$ のどのクラスに対して、充足可能性問題が決定可能かという点である。

手法
著者らは、決定可能性の境界を特徴づけるために、オートマトン理論と代数的半群理論の組み合わせを用いる。

1. 集合オートマトン: 著者らは集合オートマトンと呼ばれる新しいオートマトン形式を導入する。これらは、データ値を格納できる固定数の集合を備えた有限状態オートマトンである。遷移は以下を可能にする：

   • 局所更新: 特定の集合から現在のデータ値を追加または削除する。
   • 大域更新: 全ての集合の内容に対して同時に関係（または変換）を適用する（例：データ値を集合 $X_i$ から $X_j$ へ移動させる）。
     著者らは、集合オートマトンが、空集合問題が決定不可能であることで知られているモデルであるクラスオートマトン（Bojańczyk と Lasota によって導入された）と表現力において同等であることを確立する。

2. 部分クラスと決定可能性: 決定可能性を回復するために、著者らは順序付き準正規集合オートマトンと呼ばれる部分クラスを定義する。

   • 準正規: データ値が、特定の「不安定」集合のサブセットのうち、高々一つの集合にのみ存在することを保証する。
   • 順序付き: 不安定集合に線形順序を課し、大域更新がこれらの集合の先頭部分の内容を空にして、順序でより上位の集合へ移動させることを意味する。
     順序付き準正規集合オートマトンの空集合問題は、既知の決定可能な問題である順序付きマルチカウンターオートマトンの空集合問題への帰着によって決定可能であることが示される。

3. 論理からオートマトンへの翻訳: 本論文は、論理式とオートマトンの間の翻訳を提供する：

   • 任意の集合オートマトンは、ガード付き正則述語を持つ $EMSO_2$ 式として表現できる。
   • 逆に、モノイド $M$ によって認識される述語を用いる式は、接尾語格納集合オートマトン（準正規オートマトンの特定のタイプ）に変換できる。

4. 代数的特徴付け: 著者らはモノイド $M$ の代数的構造を分析する。線形バンドを、両側イデアルが線形に順序付けられている幂等モノイド（すなわち、任意の二つのイデアル $I, J$ について、$I \subseteq J$ または $J \subseteq I$ のいずれかが成り立つもの）として定義する。

主要な貢献と結果

• 主要定理（定理 6）: データ単語上の $EMSO_2[\Sigma, <, +1, \sim, \twoheadrightarrow_1, \tilde{F}_M]$ 式の充足可能性は、モノイド $M$ が線形バンドである場合に限って決定可能である。

  • 決定可能性方向: $M$ が線形バンドである場合、著者らは等価な順序付き準正規集合オートマトンを構成する。そのようなオートマトンの空集合問題は決定可能であるため、その論理も決定可能である。
  • 決定不可能性方向: $M$ が線形バンドでない場合、それは $U_1^2$（零を持つ二要素モノイドの二つの直積）または $N_2$（特定の零モノイド）のいずれかに同型な部分構造を含まなければならない。著者らは、これらの特定のモノイドによって認識されるガード付き正則述語が、二カウンター機械の停止問題の符号化を可能にし、論理を決定不可能にすることを示す。

• 表現力の同等性: 本論文は、集合オートマトンがガード付き正則述語を持つ $EMSO_2$ と表現力において同等であることを証明する。さらに、モノイド $M$ によって認識される正則述語を持つ任意の式は、別のモノイド $M'$（具体的には冪集合モノイド $P(M)$）によって認識されるガード付き正則述語を用いて等価に書き換えられることを示す。

• 厳密な拡張: 特定された決定可能フラグメントは、[4] からの元の $FO_2$ 論理の厳密な拡張である。例えば、同じクラス内のインクリメントとデクリメント間のゼロテストを要求しない言語 $L_2$ は、標準的な $FO_2$ やデータオートマトンでは定義不可能であるが、基礎となるモノイドが線形バンドである場合、この拡張論理では定義可能となる。

意義と主張
本論文は、ガード付き正則述語で拡張されたデータ単語上の二変数論理の決定可能性の境界を正確に特徴づけることを主張する。論理的な決定可能性を、認識するモノイドが「線形バンド」という代数的性質を持つことに関連付けることで、この研究は論理的表現力と代数的構造の間のギャップを埋めている。

著者らは、線形バンドに対する決定可能性は確立されたものの、一般の半群に対する特徴付けは未解決であると指摘している。また、線形バンドによって認識される正則言語のクラスは文献で十分に研究されていないことを強調し、その代数的領域におけるさらなる探求の必要性を示唆している。決定手続きの複雑さは、基礎となる $FO_2$ やデータオートマトンの結果から継承され、非初等的なままである。

この研究は、データクラス内の特定の正則性質を捉える決定可能な一階論理の拡張を提供することで、フリーズ-LTL などの時相論理とは区別される。これらは以前は決定不可能であったか、異なる論理フレームワークを必要としていた。