发表机构
University of Auckland（奥克兰大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种与时间视界无关的几何决策程序，通过将STL约束转化为空间可达集并解析求逆动态扩展，实现快速可行性检查与精确时间延迟修复，实验显示毫秒级执行与大幅加速。
AI 中文摘要
信号时序逻辑控制综合常因执行器限制或任务截止时间设定不当而遭遇物理不可行性。标准优化方法通过对时间视界进行离散化来建模时间，这导致计算量呈指数增长，并阻碍了连续时间调整的提取。本文提出一种几何决策程序，其评估物理可行性的过程完全独立于时间视界的长度。该方法通过将显式时序逻辑约束转化为在零时刻评估的连续空间后向可达集来运作。它解析地求逆Bhat-Bernstein沉降时间积分，将时间窗口映射为连续空间边界，从而将可行性检查简化为局部矩阵与向量的包含性评估。当规范不可行时，该程序提取Farkas对偶证书以隔离冲突约束，并识别最大几何空间间隙。随后，它解析地求逆系统动态扩展，将该最大几何间隙映射为精确的闭式时间延迟，精确修复边界赤字以恢复物理可实现性。我们正式证明了该程序的严格可靠性、数学上有界的完备性以及与时间视界无关的可扩展性。在六维无人机运动学上的实验评估表明，其执行时间低于毫秒级，相比最先进的优化编码实现了大幅加速，并且对深层嵌套的逻辑公式具有计算免疫性。
英文摘要
Signal Temporal Logic control synthesis frequently encounters physical infeasibility due to actuator limits or flawed task deadlines. Standard optimization methods model time by discretizing the horizon, which leads to exponential computational growth and prevents the extraction of continuous temporal adjustments. This paper presents a geometric decision procedure that evaluates physical feasibility completely independently of the temporal horizon length. The method operates by transforming explicit temporal logic constraints into continuous spatial backward reachable sets evaluated at time zero. It analytically inverts the Bhat-Bernstein settling-time integral to map temporal windows into continuous spatial boundaries, reducing the feasibility check to a local matrix and vector inclusion evaluation. When a specification is infeasible, the procedure extracts a Farkas dual certificate to isolate conflicting constraints and identifies the maximum geometric spatial gap. It then analytically inverts the system's dynamic expansion to map this largest geometric gap into an exact, closed-form temporal delay, precisely fixing the boundary deficit to restore physical realizability. We formally prove the strict soundness, mathematically bounded completeness, and horizon-independent scalability of this procedure. Experimental evaluations on six-dimensional drone kinematics demonstrate sub-millisecond execution times, massive speedups over state-of-the-art optimization encodings, and computational immunity to deeply nested logical formulas.
Comments11 pages, 2 figures
