Interpolation-based GR(1) assumptions refinement

DOI10.1007/978-3-662-54577-5_16MaRDI QIDQ3303899zbMATH OpenOpenAlexFDO

Authors Davide G. Cavezza, Dalal Alrajeh

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.07803

zbMATH Keywords

interpolationreactive synthesisassumption refinement

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Interpolation, preservation, definability (03C40)

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.

Recommendations

• Environment Assumptions for Synthesis
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• GR(1)*: GR(1) specifications extended with existential guarantees
• A weakness measure for GR(1) formulae
• Revisiting Synthesis of GR(1) Specifications

Cites work

• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• A Hybrid Algorithm for LTL Games
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Craig Interpolation for Linear Temporal Languages
• Diagnostic Information for Realizability
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Environment Assumptions for Synthesis
• Interpolation and SAT-based model checking.
• Interpolation theorems for some variants of LTL
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Learning regular sets from queries and counterexamples
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• Synthesis of Reactive(1) designs
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

• GR(1)*: GR(1) specifications extended with existential guarantees
• GR(1)*: GR(1) specifications extended with existential guarantees
• Performance heuristics for GR(1) synthesis and related algorithms
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• Revisiting Synthesis of GR(1) Specifications
• A weakness measure for GR(1) formulae
• A weakness measure for GR(1) formulae
• ACoRe: automated goal-conflict resolution

Describes a project that uses

Uses Software

• GitHub
• RATSY
• MathSAT

This page was built for publication: Interpolation-based GR(1) assumptions refinement

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303899)