STL-GO を MIP/SMT に落として多エージェント計画を解く

多エージェント計画では、いつ何をするかだけでなく、だれとだれがつながるか、だれが何人を見ているか、通信や感知が成り立つかまで同時に決めたい。捜索救助なら、発見、割り当て、救助完了を時間制約つきで表す必要がある。

既存の手法では、時間条件は書けても、時間で変わる相互作用グラフを細かく扱う表現力や、ソルバにそのまま渡せる実装が足りなかった。

• 時間条件とグラフ条件を一緒に扱う必要がある。
• 捜索救助では役割分担と期限付きの割当てが要る。

一般の時相論理だけでは、近傍の数やグラフ型ごとの条件を自然に書きにくい。逆に、グラフだけを見ると、いつ成立するかという時間条件が抜ける。

この論文は、その両方を一つの言語にまとめるために STL を拡張し、グラフ演算子 In と Out、グラフ型の量化、近傍カーディナリティ述語を加える。

• 時相論理だけではグラフ制約が弱い。
• グラフだけでは時間の制約が抜ける。

まず、通常の STL にグラフ演算子を足した STL-GO を導入する。ここでは、時相条件に加えて、距離グラフ、感知グラフ、通信グラフ、タスク依存グラフのような相互作用を同じ枠で扱う。

原子述語は、emergency、near、atC、carry、task などのように、実際の役割や状態に近い意味で定義される。これにより、仕様は「いつまでに何を満たすか」と「誰と誰の関係が必要か」を一緒に書ける。

• STL をグラフ制約つきに拡張する。
• 役割と関係を原子述語として明示する。

グラフ演算子は、あるタイプのグラフ上で、ある重み範囲の辺が存在するか、近傍が何人いるか、条件を満たす近傍が何人いるかを数える。# によって存在量化と全称量化を切り替えられる。

直感的には、「この型の関係で、条件を満たす相手が少なくとも何人、あるいは全部の相手がどうか」を、時間ごとに書けるようにしている。

• 辺の有無だけでなく、近傍の個数も条件にできる。
• 存在量化と全称量化を # で切り替える。

著者は、マルチエージェント計画のために STL-GO を提案し、MIP ベースと SMT ベースの2種類の符号化を与えている。

STL-GO は、時間変化する重み付き多重グラフ上で、存在・全称量化と近傍カーディナリティ条件を扱えるよう STL を拡張したものとして記述されている。

定式化は、決定論的で既知の環境・動力学を前提とした中央集権的な開ループ有限ホライズン計画に限定されている。

確率的環境は扱わず、高確率保証への拡張は未対応。

MIP 側では、辺の存在、重みの範囲、近傍カウント、時相演算子を補助変数で表し、Big-M で真偽を結びつける。目的関数付き計画も扱え、論文では線形 L1 コストと二乗 L2 コストを比較している。

実験では Gurobi を使い、scenario ごとに複数のミッション仕様を連言した計画を解いている。最難設定では time limit に達したケースがあり、著者は best incumbent を報告している。

• MIP は目的関数付き最適化に向く。
• 大きい設定では time limit に達する場合がある。