Model Checking of Optimal LTL and ASAP properties

Model checking has long been employed as a method for the formal verification of control systems, with a focus on ensuring correctness and safety. However, in practical scenarios (e.g., robotics, aviation and aerospace), simply verifying whether a control system satisfies a given property may not suffice. There is often the requisite to optimize system behavior with respect to certain criteria, such as response time. For instance, in verifying a reachability property, one may be interested in knowing if the controller reaches the goal as soon as possible (ASAP). Despite the simplicity of such requirement, its formalization has not yet been addressed in the literature and requires to reason about the strategy of the controller and the cost of the executions in closed-loop with the given environment. More in general, this paper proposes the formalization and verification of properties for controllers that must satisfy a temporal logic specification optimally, i.e., in the best way possible given the behavior on the plant to be controlled. This relies on and is parametrized by a quantitative semantics for temporal logic. We focus on linear-time temporal logic (LTL), for which various quantitative semantics have been defined. In order to characterize the fulfillment of LTL properties as soon as possible (ASAP), we introduce a new quantitative semantics related to the length of the shortest informative prefix. Finally, we focus on ASAP co-safety properties and reduce the optimal model checking to standard qualitative reactive synthesis. We provide a proof of concept demonstration of the reduction with nuXmv.