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 \(LTL ^{ \mathcal {T}}\) specifications (i.e., \(LTL \) with propositions replaced by literals from a theory \( \mathcal {T} \) ), 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 \( \mathcal {T} \) and outputs valuations of system variables from \( \mathcal {T} \) . 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 \(LTL ^{ \mathcal {T}}\) specification. We also show that our method allows adaptive 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 \( LTL ^{ \mathcal {T}} \) , which is a deterministic program (hence predictable and efficient).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

  • Andoni Rodríguez,
  • Felipe Gorostiaga,
  • César Sánchez

摘要

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 \(LTL ^{ \mathcal {T}}\) specifications (i.e., \(LTL \) with propositions replaced by literals from a theory \( \mathcal {T} \) ), 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 \( \mathcal {T} \) and outputs valuations of system variables from \( \mathcal {T} \) . 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 \(LTL ^{ \mathcal {T}}\) specification. We also show that our method allows adaptive 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 \( LTL ^{ \mathcal {T}} \) , which is a deterministic program (hence predictable and efficient).