LTL(線形時相論理)を満たしつつ「ある並び」を長期的にどれだけ訪れるかを設計する方法
この論文は、ロボットなどのシステムが高レベルの行動規則を満たしながら、ある特定の原子命題の並び(たとえば「AのあとにBが続く」)を長期にわたってどれくらいの割合で起こすかを目標として同時に達成する計画問題を扱います。通常のLTL(線形時相論理)は個々の実行の性質を指定できますが、この「長期の発生割合」を直接表現することはできません。そこで著者らは新しい量的要求を導入し、その達成法を示します。
彼らはまず「長期訪問割合」という概念を定義しました。これは無限に続く軌跡を「接頭部(prefix)」と周期的に繰り返される「接尾部(suffix)」に分けたとき、接尾部の繰り返しの中で関心のある命題列がどのくらいの割合で現れるかを表す指標です。システムの運動能力は有限の状態と遷移にコストを割り当てた有限重み遷移系(WTS)で抽象化します。経路の総コストは遷移ごとのコストの合計として定義されます。
計画手法はオートマトン(具体的にはLTLを受理する非決定性ブーチオートマトン)に基づきます。LTL仕様は対応するブーチオートマトンに変換されます。そこから、LTLを満たす接頭・接尾構造の経路を探し、同時に総コスト制約を守りながら、接尾部における長期訪問割合が目標値から許容誤差内に入るように合成します。論文ではこの手法の正しさと最適性についても理論的に解析しています。
なぜ重要かというと、この長期訪問割合を使えば単に「いつか訪れる」「常に避ける」といった定性的な指定だけでなく、運用上の注意配分を数値として調整できます。たとえば補給地点や検査点の巡回頻度を増やす/減らすといった運用の柔軟化につながります。従来の定式化(状態ごとの定常訪問割合や確率系の手法)では、特定の「並び」や順序情報を直接指定できない点が本手法の特徴です。
重要な制約や不確かさもあります。この研究は有限で決定的な重み遷移系と、接頭・接尾構造を仮定しています。従って確率的な環境や完全に未知のモデルへはそのまま適用できない可能性があります。また、論文は四足ロボットでの実験を報告し、有用性を示していますが、ここで示された実験の詳細や規模の情報は要約に限られており、応用範囲や一般化の程度については今後の検証が必要です。