加权事件信号时序逻辑到无时间几何控制的可靠编译
Sound Compilation of Weighted Event Signal Temporal Logic to Timeless Geometric Control
浏览论文内容
中文总结 AI 辅助
针对传统时序逻辑控制器依赖全局时钟易受异步异常影响的问题，提出weSTL+语言及无时间几何控制范式，通过两遍编译器将公式转为几何约束，消除时钟依赖，并在机器人案例中验证了安全性与活性。
中文摘要 AI 辅助
从标准时序逻辑综合出的网络物理系统（CPS）控制器依赖刚性全局时钟，使其易受异步时序异常（如时钟跳变、抖动和网络延迟）的影响。为克服这些脆弱性，我们引入了一种根本性的无时间几何控制范式，以及一种新颖的规范语言：加权事件信号时序逻辑（weSTL+）。这种新的weSTL+逻辑结合了事件时序逻辑（Event-STL）的事件触发特性与加权时序逻辑（weighted-STL）的加权用户偏好，使其适用于实际自主CPS的规范。利用两遍编译器，我们的框架通过有限时间水平集反演，将weSTL+公式直接转换为C^1可微的时间无关几何替代约束。通过将时间窗口直接映射到与物理时间无关的几何边界，该方法完全消除了显式的运行时时钟监控。我们的自主机器人案例研究表明，所提出的几何架构在严重宏观时序不连续下保证安全性和活性，在传统时间索引控制器失效的场景中取得成功。
英文摘要
Cyber-Physical Systems (CPS) controllers synthesized from standard temporal logics rely on rigid global clocks, rendering them vulnerable to asynchronous timing anomalies like clock snaps, jitter, and network delays. To overcome these vulnerabilities, we introduce a fundamentally timeless geometric control paradigm alongside a novel specification language: Weighted Event-Based Signal Temporal Logic (weSTL+). This new weSTL+ logic combines the event triggered nature of Event-STL with weighted user preferences of weighted-STL making it suitable for specification of practical autonomous CPS. Using a two-pass compiler, our framework translates weSTL+ formulae directly into C^1-differentiable time-invariant geometric surrogate constraints via finite-time level-set inversion. By mapping temporal windows directly into physical time independent geometric boundaries, this approach entirely eliminates explicit runtime clock monitoring. Our autonomous robotics case study demonstrates that the proposed geometric architecture guarantees enforcement of safety and liveness under severe macroscopic timing discontinuities, succeeding where traditional time-indexed controllers fail.
发表机构
- University of Auckland（奥克兰大学）
机构由 AI 辅助整理，请以论文原文为准。
