LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

要約

この論文では、任意の到達可能性と安全性特性の環境仕様の下での LTLf 合成を研究します。
エージェントのタスクと環境仕様の両方について両方の種類のプロパティを考慮し、合成アルゴリズムの完全な状況を提供します。
それぞれのケースに対して、特定のアルゴリズム (問題の複雑さを考慮した最適なアルゴリズム) を考案し、その正しさを証明します。
アルゴリズムは、共通の構成要素をさまざまな方法で組み合わせます。
いくつかの事例はすでに文献で研究されていますが、他の事例はここで初めて研究されます。

要約(オリジナル)

In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google