Synthesis of Infinite State Systems

技術的概要：無限状態システムの合成

問題定義
本論文は、有限状態システムに対して Büchi および Landweber によって解決された古典的な Church 合成問題を、無限状態システムに拡張した一般化された Church 合成問題を取り扱います。

• 古典的コンテキスト: 元の問題は、$\omega = (\mathbb{N}, <)$ 上の単一述語第二階（MSO）論理で記述された仕様 $S(I, O)$ が与えられたとき、その仕様を満たす因果的演算子（有限状態オートマトンによって実装可能）が存在するかどうかを問うものです。
• 一般化されたコンテキスト: 著者らは、状態空間および/または入力/出力アルファベットが無限であるシステムの合成を調査します。目標は、無限構造 $M$ 上の MSO 定義可能なパリティゲームで定義された関係を実装する因果的演算子が存在するかどうかを決定し、存在するならば、それ自体が $M$ において MSO 定義可能なトランスデューサ（無限状態機械）を構築することです。

方法論
著者らは、無限構造に適応された論理、ゲーム、オートマトンの相互作用に基づいた体系的なアプローチを採用します。この方法論は、主に 3 つの段階で進行します。

1. 無限アリーナにおけるゲーム合成:
   核心的な技術的課題は、アリーナ（頂点と辺）が構造 $M$ 上の MSO 論理式によって定義されるパリティゲームを解くことです。著者らは、$M$ において定義可能である一様な記憶なし勝利戦略の発見に焦点を当てます。

   • 選択性: 構造 $M$ の選択性（selection property）が中心的な概念です。構造がこの性質を持つとは、満たされる MSO 論理式すべてが、満たされるタプルを一意に選ぶ「セレクタ」（論理式）を定義可能に持つ場合を指します。
   • 有界次数と無界次数:
     • 有界次数（または有界出力次数）のゲームの場合、著者らは $M$ が選択性を持つならば、定義可能な一様な記憶なし勝利戦略が存在することを示します。これは、選択性を用いてグラフの辺の定義可能な局所線形順序を構築することに依存します。
     • 無界次数のゲームの場合、著者らは表現スキームを導入します。$M$ で定義された無界次数ゲーム $G$ を、$M$ の「コピー」（例：$M \times k$）で定義された有界次数ゲーム $\tilde{G}$ によって表現します。$\tilde{G}$ が定義可能な戦略を持つならば、それらを $G$ へ転送できることを証明します。
   • 正規表現による定義可能性: 順序数 $<\omega^\omega$ や完全 $k$ 分木 $T_k$ といった特定の構造を扱うために、著者らはこれらの構造における任意の MSO 定義グラフが、正規表現を介して定義可能な有界次数グラフで表現できることを示します。これにより、一般的な MSO 定義可能性と戦略合成に必要な有界次数要件との間のギャップが埋められます。

2. 戦略からトランスデューサへ（一般化された Church 問題）:
   ゲームアリーナにおいて「出力」プレイヤーの勝利戦略が見つかった後、著者らはこの戦略を実装するトランスデューサへ変換する課題に取り組みます。

   • 有限アルファベット: アルファベットが有限の場合、戦略は直接トランスデューサを導き出します。
   • 無限アルファベット: アルファベットが無限の場合、勝利戦略は次の状態を決定しますが、必ずしも出力する特定のラベル（記号）を決定するわけではありません。なぜなら、同じ状態に至る複数のラベルが存在する可能性があるからです。これを解決するため、著者らは弱第一階一様化（weak first-order uniformization）という条件を導入します。$M$ がこの性質を持つならば、勝利戦略と両立する特定の出力記号を定義可能に選択でき、それによって MSO 定義可能なトランスデューサを構築できます。

3. 構造分析:
   本論文は、必要な条件（選択性、選択の決定可能性、弱第一階一様化）を満たすかどうかを判断するために、特定の構造を分析します。

   • 順序数: $\alpha < \omega^\omega$ に対する $(\alpha, <)$。
   • 木: 完全 $k$ 分木 $T_k$、および選択性を維持するレベル述語や他のパラメータによるその拡張。

主要な貢献と結果

• 理論的枠組み: 本論文は、基礎となる構造 $M$ によってパラメータ化された、無限状態システムの合成のための統合された枠組みを確立します。これは $M$ に対する「ゲーム合成問題」を形式化し、勝者の決定と MSO 定義可能な記憶なし勝利戦略の発見を扱います。
• 決定可能性と定義可能性定理:
  • 定理 1.2 および 1.3: $M$ が選択性を持つならば、$M$ 内の有界次数（およびその後、表現を介した無界次数）の MSO 定義パリティゲームは、MSO 定義の一様な記憶なし勝利戦略を許容します。
  • 定理 1.4（定義可能な無限状態システムの合成）: 順序数 $<\omega^\omega$ や完全 $k$ 分木などの構造 $M$ に対して、一般化された Church 合成問題は決定可能です。さらに、因果的演算子が存在するならば、その関係を実装するMSO 定義可能なトランスデューサが存在します。
• 既知の結果の一般化:
  • 本結果は、完全二分木で定義可能なプッシュダウンパリティゲームに関する Walukiewicz の定理を、より広範なクラスの構造とゲームに一般化します。
  • この枠組みは、N-オートマトンや接頭辞認識グラフに関する先行結果を包含し、それらの決定可能性と構成可能性のより体系的な導出を提供します。
• 無限アルファベットのための条件: 本論文は、勝利戦略から無限アルファベット上のトランスデューサを合成するために必要な決定的な条件として弱第一階一様化を特定します。

意義と主張
著者らは、この仕事が一般化された Church 合成問題の最初の体系的な研究であると主張します。古典的な問題は有限状態システムに対して広範に研究されてきましたが、無限状態システムの合成は、プッシュダウンオートマトンや高階プッシュダウンなど、孤立した事例でのみ取り扱われており、統一された理論は存在しませんでした。

• 元の文脈への回帰: 本論文は、Church の元の定式化が無限状態システム（「回路」および「論理システム」）を許容していたことに留意しつつ、Büchi と Landweber の後にコミュニティが有限状態に焦点を絞ったことを指摘します。この仕事は、その元のより広範な文脈へと議論を戻すものです。
• 実用的意義: 著者らは、有限状態システムがハードウェアをモデル化するのに対し、ソフトウェアは頻繁に無限状態システムとして表現されると指摘します。したがって、無限状態システムの合成に関する体系的な理論は、自然かつ必要な一般化です。
• 謙虚さ: 本論文は、すべての可能な無限構造に対する必要十分条件ではなく、十分条件（選択性、一様化）を提供することを認めています。すべての無限構造に対する合成問題を解決するとは主張していませんが、$\omega^\omega$ 未満の順序数や特定のパラメータを持つ木など、重要なクラスの構造に対して堅牢な解決策を提供します。

要約すると、本論文は無限ゲームのアルゴリズム理論を無限状態システムの合成へと成功裏に拡張し、重要な論理構造における定義可能な実装の生成のための決定可能性結果と構成手法を提供しています。