Interpolation-Based GR(1) Assumptions Refinement

DOI10.1007/978-3-662-54577-5_16zbMath1452.68115arXiv1611.07803OpenAlexW2554196169MaRDI QIDQ3303899

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

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

Related Items (4)

GR(1)*: GR(1) specifications extended with existential guarantees ⋮ A weakness measure for GR(1) formulae ⋮ A weakness measure for GR(1) formulae ⋮ Performance heuristics for GR(1) synthesis and related algorithms

Uses Software

• MathSAT
• RATSY
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Synthesis of Reactive(1) designs
• Learning regular sets from queries and counterexamples
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Environment Assumptions for Synthesis
• Craig Interpolation for Linear Temporal Languages
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Interpolation theorems for some variants of LTL
• Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
• Diagnostic Information for Realizability
• A Hybrid Algorithm for LTL Games
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Interpolation-Based GR(1) Assumptions Refinement