対象は、ランク付き有向非巡回グラフ上で、各エージェントの出発位置・出発時刻・到着位置・到着時刻が指定される厳密到着型の多エージェント経路探索である。各セルは、中央で経路を復号するのではなく、自分が有効な共同経路支持マスクに含まれるかどうかを出力する。セルラーマシンはトポロジーとスロット写像を事前に知り、セルごとに状態を持ち、固定された局所配線上で同期通信するが、問い合わせに応じて出力ラウンドを変えることはできない。問題の核心は、あるセルについて単独では合法な選択が、後の時刻に別エージェントと衝突するため、共同解では不適切になることである。
第一に、二つのエージェントと十二セルからなる深さ三の構成に対し、大域チャネルを持たない正方向専用機械は、任意のラウンド数でも二つの実行可能な問い合わせを同時には正しく処理できないことを示す。時間反転した構成により、逆方向専用機械にも対応する下界を与える。第二に、構成を複数個並べることで、正方向専用機械について、目標側の局所円錐に届く問い合わせ情報量と大域一ビットフラグの総量に関するトレードオフを示し、一定の深さでは必要な情報量がコピー数に比例することを述べる。第三に、逆方向通信やフラグ逐次送信による上界を示し、単一方向性を捨てる代わりに長い実行時間や広い大域チャネルを支払う逃げ道を整理する。
各セルには、自身のエージェントについての最大個別経路支持であるキャビティのビットを実行時入力として与える。この入力により単一エージェント問題はゼロラウンドで解けるため、主張はエージェント間衝突に依存する。交差する衝突選択器では、問い合わせに応じて一方の枝だけが完全な共同経路支持になり、対象セルの正しい出力が変化する一方、その対象の局所的な観測は一定になるように配置する。局所性と因果円錐の不変性から対象の出力が変わらないことを導き、強制出力との矛盾を作る。複数コピーでは、対象へ届かない情報を大域フラグで送る場合のトランスクリプト数を数え、必要な帯域を下界化する。
有限なガジェットの補題とペア不変性に基づく矛盾はLean 4で検査されている。意味論との接続、因果円錐の補題、情報量の数え上げは論文中の証明である。単一エージェントの帰結は全探索で確認されたと記載されている。論文はベンチマークを報告しておらず、標準MAPFデータセット、既存アルゴリズムとの比較、実行時間や成功率などの実験的指標も提示していない。
結果は、すべての経路探索アルゴリズムが単方向通信で失敗するという意味ではない。トポロジーが既知で、ラウンド数と状態資源を十分に許せば、正方向だけでも情報を集約し、候補マスクを列挙して検査する機械を構成できるため、主張は特定のトポロジー上で問い合わせ族全体を一定の資源条件で処理することに関するものである。したがって本論文の結論は、双方向伝播を採用するか、長い実行時間、大域帯域、外部助言、逐次列挙、共有メモリなどを支払う必要があるという資源会計として理解すべきである。抜粋は、実機のタイル配置や一般トポロジーでのより鋭い双方向上界を確立しておらず、容量・運動学・辺衝突を含むモデルも今後の課題としている。
厳密到着型の経路探索では、各エージェントの経路が個別には合法でも、他エージェントとの時空間上の衝突によって共同解として不適切になり得る。局所通信だけで各セルが自分の出力ビットを決める場合、正しい判断に必要な情報が時間的にも別エージェント上にも存在し得る。
固定された局所配線、同期ラウンド、セルごとに分解された状態、問い合わせに依存しない出力ラウンドを持つ機械を考える。問題は、実行可能なすべての問い合わせに対して、各セルが有効な共同経路支持マスクの自分のビットを出力できるかである。抜粋は、非実行可能な問い合わせや、特定の実装環境での性能については確立していない。
キャビティは、単一エージェントが取り得る最大の経路支持であり、これを各セルに与えると単一エージェントの方向性下界は消える。主たる下界は、対象セルのキャビティを変えずに衝突相手側の問い合わせビットだけを変え、対象の正しい出力を反転させる構成に依存する。複数コピーでは、正方向専用機械について、目標の因果円錐に届く情報量を表す量をJ_R、大域フラグ数をk、ラウンド数をRとすると、J_R+kR≥pという制約が示され、ここではJ_R=0である。逆方向機械はこの族を一定ラウンドで解き、フラグ逐次送信機械はおおむねコピー数をフラグ数で割ったラウンドと定数オーバーヘッドを要する。
報告された検証は、有限ガジェットの形式化、補題のLean 4によるチェック、有限な単一エージェント事例の全探索である。数値ベンチマーク、標準データセット、ベースライン比較、学習や実行時間の測定は報告されていない。後半の一節には有限列挙とシミュレーションが含まれるとされるが、抜粋だけではその条件や数値結果を確定できない。したがって、有限検証を超える経験的性能主張は導けない。
十二セル・二エージェント・深さ三の構成では、フラグなしの正方向専用機械は、ラウンド数によらず二つの実行可能な問い合わせを正しく処理できない。時間反転した構成は逆方向専用機械に同じ障害を与え、両方の構成を直和すると、どちらか一方の時間方向を全体で捨てることができない。複数コピーでは、正方向専用機械に必要な情報量がコピー数に比例し、逆方向機械は一定ラウンド、フラグ逐次送信機械はコピー数をフラグ数で割った程度のラウンドで解けるとされる。これは通常の実行時間ベンチマークではなく、情報資源のオーダーが一致するという結果である。
厳密到着では、早い時刻のセルの判断が、後の時刻に別エージェントが何をするかで決まることがある。個別キャビティと少数の大域フラグを与えても、局所因果を一方向に制限した機械には、明示的な構成上の情報障害が残る。双方向性は表現力そのものの必要条件ではなく、一定深さ・一定帯域・問い合わせ族全体で解くための有力な資源要件として現れる。
主張は、ランク付き有向非巡回グラフ、頂点衝突、実行可能な問い合わせ、固定トポロジーを知る非一様セルラーマシンという狭いモデルに依存する。抜粋は、厳密到着型と自由到着型または締切型との間に分離があることを示しておらず、一般トポロジーにおける最適な双方向上界も与えていない。関連研究の調査は抄録と書誌記録を中心とする第一段階であり、網羅的な優先権主張ではない。
本研究は、局所分散型MAPFで、個々の到達可能性を前計算してもエージェント間の衝突依存性が消えないことを明確にする。ハードウェアやセルラーネットワークを設計する際、双方向配線を追加するか、帯域・ラウンド・共有記憶を増やすかを比較するための理論的な資源下界を与える。小さくパラメータ化され、部分的に形式検証された構成は、将来の分散MAPF機械のベンチマーク候補になり得るが、論文自身はその用途を実施していない。
セルラーネットワーク、分散計算、MAPFの厳密到着制約、因果円錐、通信下界に関心のある研究者に向いている。標準ベンチマークでのアルゴリズム性能や実装比較を探している読者には、実験結果がないため直接の代替にはならない。形式手法に関心がある読者には、有限補題をLean 4で検査する構成が参考になる。