Maximum realizability for linear temporal logic specifications

DOI10.1007/978-3-030-01090-4_27MaRDI QIDQ6109602zbMATH OpenOpenAlexFDO

Authors Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Publication date 28 July 2023

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1804.00415, http://eprints.whiterose.ac.uk/156424/1/atva18.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Automated systems (robots, etc.) in control theory (93C85) Temporal logic (03B44)

Abstract: Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning, control of autonomous systems, and load distribution in power networks. 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 the bounded synthesis approach, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the safety specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks.

Recommendations

• Reactive synthesis with maximum realizability of linear temporal logic specifications
• Safraless LTL synthesis considering maximal realizability
• Reactive synthesis from signal temporal logic specifications
• Specification-guided controller synthesis for linear systems and safe linear-time temporal logic
• Synthesis from LTL specifications with mean-payoff objectives

Cited in

(2)

• Safraless LTL synthesis considering maximal realizability
• Reactive synthesis with maximum realizability of linear temporal logic specifications

This page was built for publication: Maximum realizability for linear temporal logic specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6109602)