Preferences on Partial Satisfaction using Weighted Signal Temporal Logic Specifications

This work presents partial satisfaction control synthesis over an extension of Weighted Signal Temporal Logic wSTL called wSTL+. The new specification language wSTL+ enables the definition of preferences and importance of subformulae as weights over-inclusive (soft) operators (i.e., standard Boolean and temporal operators from wSTL). Furthermore, it includes exclusive operators that impose hard constraints to disallow specific subformulas to be partially satisfied. All subformulae must be fully satisfied or violated for conjunctive operators (conjunction and always). In the case of disjunctive operators (disjunction and eventually), mutual exclusive satisfaction is imposed, i.e., exactly one subformula holds. The weights in the specification capture the preferences and importance of fully satisfiable specifications and modulate the solution over conflicting or infeasible specifications. We formulate the partial satisfaction problem over wSTL+ specifications as a bilevel optimization problem. The inner level is modeled as a MILP and captures the customized satisfaction of the wSTL+ specification. The outer level is a linear program that maximizes the robustness of the satisfiable solution found in the inner level. Finally, we show the performance of our method in different case studies involving robot navigation in planar environments.