Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/44602
Title: Maximum Realizability for Linear Temporal Logic Specifications
Authors: Dimitrova, Rayna
Ghasemi, Mahsa
Topcu, Ufuk
First Published: 30-Sep-2018
Presented at: 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018)
Publisher: Springer Verlag (Germany)
Citation: Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science, 2018, vol 11138.
Abstract: Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning and control of autonomous systems. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis problem in settings where the overall specification is unrealizable, more precisely, when some of the desirable properties have to be (temporarily) violated in order to satisfy the system’s objective. We provide a quantitative semantics of sets of safety specifications, and use it to formalize the “best-effort” satisfaction of such soft specifications while satisfying the hard LTL specification. We propose an algorithm for synthesizing implementations that are optimal with respect to this quantitative semantics. Our method builds upon the idea of bounded synthesis, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the soft specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks.
Series/Report no.: Lecture Notes in Computer Science (LNCS);11138
DOI Link: 10.1007/978-3-030-01090-4_27
ISSN: 0302-9743
Links: https://link.springer.com/chapter/10.1007/978-3-030-01090-4_27
http://hdl.handle.net/2381/44602
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2018, Springer Verlag (Germany). Deposited with reference to the publisher’s open access archiving policy. (http://www.rioxx.net/licenses/all-rights-reserved)
Description: The code is available at https://github.com/MahsaGhasemi/max-realizability
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

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


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