Quantitative Assume Guarantee Synthesis
- Submitting institution
-
The University of Leicester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1424
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-319-63390-9_19
- Title of conference / published proceedings
- Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II
- First page
- 353
- Volume
- 10427
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Deposit exception
- Month of publication
- -
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
https://doi.org/10.1007/978-3-319-63390-9_19
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper extends the popular GR(1) fragment quantitatively and still provide efficient synthesis that made GR(1) popular and practical. Many groups use GR(1), e.g., at Cornell (Kress-Gazit), Gothenburg (Piterman), Imperial (Alrajeh), Luxembourg (Menghi), Texas (Topcu). It showed how to extend their work to the quantitative setting. Ringert gave an invited presentation at SYNT’17 on this paper. Our work was adopted by Camacho et al. (KR’18) for finite LTL synthesis and compared to by others, e.g., works published in ATVA, CAV, FMCAD, IJCAI, and TACAS. The research leading to this work had received funding from two ERC grants (278410 / 648701).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -