Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

要約

リアクティブ合成は、時相論理仕様から正しいコントローラーを生成するプロセスです。
古典的な LTL リアクティブ合成は、(提案) LTL を仕様言語として処理します。
ブール抽象化により、LTLt 仕様 (つまり、命題が理論計算からのリテラルに置き換えられた LTL) を等価実現可能な LTL 仕様に減らすことができます。
この論文では、これらの結果を完全な静的合成手順に拡張します。
合成されたシステムは、豊富な理論 calT から環境から変数の評価を受け取り、calT からシステム変数の評価を出力します。
抽象化手法を使用して LTL 仕様からリアクティブ ブール コントローラーを合成し、それを関数合成と組み合わせて、元の LTLt 仕様の静的コントローラーを取得します。
また、たとえば常に最小の安全な値を提供するためにコントローラーが出力を最適化できるという意味で、私たちの方法が応答を可能にすることも示します。
これは、LTLt の最初の完全な静的合成方法であり、決定論的なプログラムです (したがって、予測可能で効率的です)。

要約(オリジナル)

Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google