Please use this identifier to cite or link to this item:
Title: On Well-Separation of GR(1) Specifications
Authors: Maoz, Shahar
Ringert, Jan Oliver
First Published: 2016
Presented at: 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), Seattle, WA
Start Date: 13-Nov-2016
End Date: 18-Nov-2016
Publisher: Association for Computing Machinery (ACM)
Citation: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016), 2016, pp. 362-372
Abstract: Specifications for reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, consist of assumptions and guarantees. One way a controller may satisfy the specification is by preventing the environment from satisfying the assumptions, without satisfying the guarantees. Although valid this solution is usually undesired and specifications that allow it are called non-well-separated. In this work we investigate non-well-separation in the context of GR(1), an expressive fragment of LTL that enables efficient synthesis. We distinguish different cases of non-well-separation, and compute strategies showing how the environment can be forced to violate its assumptions. Moreover, we show how to find a core, a minimal set of assumptions that lead to non-well-separation, and further extend our work to support past-time LTL and patterns. We implemented our work and evaluated it on 79 specifications. The evaluation shows that non-well-separation is a common problem in specifications and that our tools can be efficiently applied to identify it and its causes.
DOI Link: 10.1145/2950290.2950300
ISBN: 978-1-4503-4218-6
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2016, Association for Computing Machinery (ACM). Deposited with reference to the publisher’s open access archiving policy. (
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
MR16separation.pdfPost-review (final submitted author manuscript)855.91 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.