论文标题
使用加权信号时间逻辑指定用户首选项
Specifying User Preferences using Weighted Signal Temporal Logic
论文作者
论文摘要
我们扩展信号时间逻辑（STL），以实现重要性和优先级的规范。该扩展称为加权STL（WSTL），具有与STL相同的定性（布尔）语义，但还定义了与布尔和临时算子相关的权重，这些权重调节其定量语义（稳健性）。我们表明，WSTL的鲁棒性可以定义为所有已知兼容鲁棒性功能的加权概括（即，在公式上递归定义的稳健性得分）可以考虑WSTL公式中的权重。我们利用这种加权的鲁棒性来区分具有所需的WSTL公式的信号，该公式具有不同的重要性或优先级和时间偏好，并证明其在无法实现所有任务满意的任务的问题上有用。我们还在优化框架中采用WSTL鲁棒性来综合控制器，以最大程度地利用用户指定的首选项满足规范的满意度。
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.
