The problem of \(\mathsf {LTL_f}\) reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given \(\mathsf {LTL_f}\) specification. We describe the implementation of an \(\mathsf {LTL_f}\) synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from \(\mathsf {LTL_f}\) to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.

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

Engineering an  \(\mathsf {LTL_f}\) Synthesis Tool

  • Alexandre Duret-Lutz,
  • Shufang Zhu,
  • Nir Piterman,
  • Giuseppe De Giacomo,
  • Moshe Y. Vardi

摘要

The problem of \(\mathsf {LTL_f}\) reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given \(\mathsf {LTL_f}\) specification. We describe the implementation of an \(\mathsf {LTL_f}\) synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from \(\mathsf {LTL_f}\) to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.