Interpolation-Based GR(1) Assumptions Refinement

TL;DR

This paper introduces an interpolation-based method for refining assumptions in unrealizable GR(1) specifications, effectively identifying causes of unrealizability and computing assumptions without user input, leading to weaker assumptions and improved convergence.

Contribution

It presents a novel counterstrategy-guided synthesis approach using Craig's interpolants for assumptions refinement in GR(1) specifications, reducing convergence steps and improving assumptions quality.

Findings

Yields weaker assumptions than baseline techniques

Reduces steps to achieve realizability

Solves cases unsolvable by existing methods

Abstract

This paper considers the problem of assumptions refinement in the context of unrealizable specifications for reactive systems. We propose a new counterstrategy-guided synthesis approach for GR(1) specifications based on Craig's interpolants. Our interpolation-based method identifies causes for unrealizability and computes assumptions that directly target unrealizable cores, without the need for user input. Thereby, we discuss how this property reduces the maximum number of steps needed to converge to realizability compared with other techniques. We describe properties of interpolants that yield helpful GR(1) assumptions and prove the soundness of the results. Finally, we demonstrate that our approach yields weaker assumptions than baseline techniques, and finds solutions in case studies that are unsolvable via existing techniques.