Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/42326
Title: A Symbolic Justice Violations Transition System for Unrealizable GR(1) Specifications
Authors: Kuvent, Aviv
Maoz, Shahar
Ringert, Jan Oliver
First Published: 2017
Presented at: 11th Joint Meeting of European Software Engineering Conference (ESEC) / ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), Paderborn, GERMANY
Start Date: 4-Sep-2017
End Date: 8-Sep-2017
Publisher: Association for Computing Machinery (ACM)
Citation: Proceeding ESEC/FSE 2017 Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, 2017, pp. 362-372
Abstract: One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. Existing approaches to deal with unrealizability, in the context of GR(1), an expressive assume-guarantee fragment of LTL that enables efficient synthesis, include the generation of concrete counter-strategies and the computation of an unrealizable core. Although correct, such approaches produce large and complicated counter-strategies, often containing thousands of states. This hinders their use by engineers. In this work we present the Justice Violations Transition System (JVTS), a novel symbolic representation of counter-strategies for GR(1). The JVTS is much smaller and simpler than its corresponding concrete counter-strategy. Moreover, it is annotated with invariants that explain how the counter-strategy forces the system to violate the specification. We compute the JVTS symbolically, and thus more efficiently, without the expensive enumeration of concrete states. Finally, we provide the JVTS with an on-demand interactive concrete and symbolic play. We implemented our work, validated its correctness, and evaluated it on 14 unrealizable specifications of autonomous Lego robots as well as on benchmarks from the literature. The evaluation shows not only that the JVTS is in most cases much smaller than the corresponding concrete counter-strategy, but also that its computation is faster.
DOI Link: 10.1145/3106237.3106240
ISBN: 978-1-4503-5105-8
Links: https://dl.acm.org/citation.cfm?doid=3106237.3106240
http://hdl.handle.net/2381/42326
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2017, ACM. Deposited with reference to the publisher’s open access archiving policy. (http://www.rioxx.net/licenses/all-rights-reserved)
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

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


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