A major challenge of reactive synthesis, an automated process for deriving correct-by-construction reactive systems from temporal specifications, is debugging unrealizable specifications. One way to debug them in the context of GR(1), an LTL fragment that balances efficient synthesis complexity and expressiveness, is the computation of unrealizable cores. Although work has been done to accelerate core computation, it remains a costly operation, despite being commonly used during specification development. In this paper, we first examine a version of the existing QuickCore core computation algorithm, where we replace the classic DDMin algorithm with CDD, a state-of-the-art domain-agnostic minimization algorithm. Then, we present two novel GR(1)-specific heuristics to improve the core computation time by exploiting attributes of the realizability checking algorithm. These heuristics include (1) quickly discarding unneeded justice guarantees, and (2) reusing realizability check results to make subsequent checks faster. We implemented our work on top of the Spectra language and synthesizer and evaluated it over hundreds of specifications. Our evaluation shows that while using CDD in our context was ineffective, the new heuristics improve core computation times for 80% of the specifications, with an average improvement of more than three times compared to the baseline QuickCore algorithm.

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

Performance Heuristics for GR(1) Unrealizable Core Computation

  • Shachaf Cohen,
  • Shahar Maoz

摘要

A major challenge of reactive synthesis, an automated process for deriving correct-by-construction reactive systems from temporal specifications, is debugging unrealizable specifications. One way to debug them in the context of GR(1), an LTL fragment that balances efficient synthesis complexity and expressiveness, is the computation of unrealizable cores. Although work has been done to accelerate core computation, it remains a costly operation, despite being commonly used during specification development. In this paper, we first examine a version of the existing QuickCore core computation algorithm, where we replace the classic DDMin algorithm with CDD, a state-of-the-art domain-agnostic minimization algorithm. Then, we present two novel GR(1)-specific heuristics to improve the core computation time by exploiting attributes of the realizability checking algorithm. These heuristics include (1) quickly discarding unneeded justice guarantees, and (2) reusing realizability check results to make subsequent checks faster. We implemented our work on top of the Spectra language and synthesizer and evaluated it over hundreds of specifications. Our evaluation shows that while using CDD in our context was ineffective, the new heuristics improve core computation times for 80% of the specifications, with an average improvement of more than three times compared to the baseline QuickCore algorithm.