用三值逻辑重构行为树，实现自动系统可控性保障。
Ternary Logic Encodings of Temporal Behavior Trees with Application to Control Synthesis
- 引入未知值的三值时序逻辑，处理部分满足规范的情况
- 提出混合整数线性编码，支持线性系统控制策略生成
- 适合需要形式化验证与自动控制的智能系统研究者
行为树（BTs）为自主系统构建长期规划提供了直观的图形化界面。为确保其正确性和安全性，严格的正式模型和验证技术至关重要。时序行为树（TBTs）通过利用现有的时序逻辑形式化方法，为行为树的执行提供规格说明和验证，但当前分析仅限于离线事后分析和轨迹修复。本文将TBTs重新表述为适用于控制综合的三值信号时序逻辑（STL）。三值逻辑引入第三真值“未知”，形式化捕捉轨迹既未完全满足也未完全不满足规范的情形。我们提出了部分轨迹STL与TBT在三值逻辑下的混合整数线性编码，使线性动力系统可通过混合整数优化获得保证正确的控制策略。通过求解最优控制问题，展示了该框架的有效性。
原文摘要 · Abstract (English)
Behavior Trees (BTs) provide designers an intuitive graphical interface to construct long-horizon plans for autonomous systems. To ensure their correctness and safety, rigorous formal models and verification techniques are essential. Temporal BTs (TBTs) offer a promising approach by leveraging existing temporal logic formalisms to specify and verify the executions of BTs. However, this analysis is currently limited to offline post hoc analysis and trace repair. In this paper, we reformulate TBTs using a ternary-valued Signal Temporal Logic (STL) amenable for control synthesis. Ternary logic introduces a third truth value \textit{Unknown}, formally capturing cases where a trajectory has neither fully satisfied or dissatisfied a specification. We propose mixed-integer linear encodings for partial trajectory STL and TBTs over ternary logic allowing for correct-by-construction control strategies for linear dynamical systems via mixed-integer optimization. We demonstrate the utility of our framework by solving optimal control problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。