Reactive synthesis is used to automatically generate circuits or programs from temporal logic specifications. In propositional reactive synthesis, generalized reactivity(1) (GR(1)) has proven to be a good compromise between expressiveness and performance. In domains like cyber-physical systems, however, programs must operate on data such as integers or reals, resulting in an infinite state space. This paper shows how to achieve the advantages of GR(1) to infinite-state reactive synthesis. We show how to use an SMT solver to solve the synthesis problem and present techniques to efficiently compute the enforceable predecessor and optimize the fixpoint computation. We show how to generate efficient programs as the result of the synthesis procedure, using techniques that are different from the circuit generation methods used in the propositional domain. We have implemented our method as a prototype to show its efficiency on several existing and new benchmarks.

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

Synthesis from Infinite-State Generalized Reactivity(1) Specifications

  • Benedikt Maderbacher,
  • Felix Windisch,
  • Roderick Bloem

摘要

Reactive synthesis is used to automatically generate circuits or programs from temporal logic specifications. In propositional reactive synthesis, generalized reactivity(1) (GR(1)) has proven to be a good compromise between expressiveness and performance. In domains like cyber-physical systems, however, programs must operate on data such as integers or reals, resulting in an infinite state space. This paper shows how to achieve the advantages of GR(1) to infinite-state reactive synthesis. We show how to use an SMT solver to solve the synthesis problem and present techniques to efficiently compute the enforceable predecessor and optimize the fixpoint computation. We show how to generate efficient programs as the result of the synthesis procedure, using techniques that are different from the circuit generation methods used in the propositional domain. We have implemented our method as a prototype to show its efficiency on several existing and new benchmarks.