Interpolation-Based GR(1) Assumptions Refinement
From MaRDI portal
Publication:3303899
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
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
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
