Specifying User Preferences using Weighted Signal Temporal Logic

TL;DR

This paper introduces Weighted Signal Temporal Logic (wSTL), an extension of STL that incorporates importance weights, enabling nuanced specification of user preferences and priorities in signal analysis and controller synthesis.

Contribution

The paper develops weighted robustness semantics for STL, allowing for preference-aware signal evaluation and controller synthesis, addressing conflicting tasks with prioritized specifications.

Findings

Weighted robustness generalizes existing STL robustness measures.

wSTL effectively distinguishes signals based on importance weights.

Controller synthesis using wSTL improves satisfaction of prioritized specifications.

Abstract

We extend Signal Temporal Logic (STL) to enable the specification of importance and priorities. The extension, called Weighted STL (wSTL), has the same qualitative (Boolean) semantics as STL, but additionally defines weights associated with Boolean and temporal operators that modulate its quantitative semantics (robustness). We show that the robustness of wSTL can be defined as weighted generalizations of all known compatible robustness functionals (i.e., robustness scores that are recursively defined over formulae) that can take into account the weights in wSTL formulae. We utilize this weighted robustness to distinguish signals with respect to a desired wSTL formula that has sub-formulae with different importance or priorities and time preferences, and demonstrate its usefulness in problems with conflicting tasks where satisfaction of all tasks cannot be achieved. We also employ wSTL robustness in an optimization framework to synthesize controllers that maximize satisfaction of a specification with user specified preferences.