使用加权信号时序逻辑的用户偏好
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
