interpolation based gr 1 assumptions refinement

• DOI: 10.48550/arxiv.1611.07803
• Publication Date: 2017-01-01
• Authors: Davide G. Cavezza; Dalal Alrajeh
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; 0102 computer and information sciences; 01 natural sciences; Logic in Computer Science (cs.LO)

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.<br/>Extension of the paper in TACAS 2017 proceedings with the same title; more comprehensive description; new experimental setting; additional case studies; additional evidence to support the original claim<br/>