Maximum realizability for linear temporal logic specifications

DOI10.1007/978-3-030-01090-4_27zbMATH Open1517.68229arXiv1804.00415OpenAlexW2964122198MaRDI QIDQ6109602FDOQ6109602

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)

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.

Full work available at URL: https://arxiv.org/abs/1804.00415

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

Mathematics Subject Classification ID

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

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)