发表机构
IMT Lucca; TU Wien; AIT Austrian Institute of Technology（卢卡高等研究学院; 维也纳工业大学; 奥地利技术研究院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究针对网络物理系统中STL公式一致性检查难题，指出原表格法缺陷，提出新树形表格法并证明其可靠性与完备性，基于此开发STLSat工具，能判定可满足性等，评估显示其性能优于现有工具。
AI 中文摘要
信号时序逻辑（STL）用于描述网络物理系统中实值信号的时序属性。在关键任务和安全关键领域，规范常由大量STL公式组成，导致一致性检查和需求分析成为工程瓶颈。虽基于表格的可满足性过程是解决此问题的自然方案，但现有有界离散时间STL的树形表格法不能对所有STL公式给出可靠的可满足性/不可满足性判定。本文指出该过程的缺陷，提出新的树形表格法并证明其对有界离散时间STL是可靠且完备的。在此基础上，引入开源Rust工具STLSat，它能判定STL公式的可满足性、合成具体见证信号、检查规范间的逻辑蕴含和等价性、提取不可满足核，还实现了增强的一阶逻辑和可满足性模理论编码，可作为组合求解器。通过公开的扩展基准套件评估，该组合求解器在保持正确性的同时匹配或优于现有工具。
英文摘要
Signal Temporal Logic (STL) is a formalism used to describe temporal properties of real-valued signals in cyber-physical systems. In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck. Tableau-based satisfiability procedures are a natural way to address this problem. Two of the authors of this paper contributed to the only existing tree-shaped tableau for bounded discrete-time STL, but we have recently found out that the procedure can return incorrect verdicts for some STL formulas. In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau that we prove to be sound and complete for bounded discrete-time STL. On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, and extracts unsatisfiable cores with its tableau engine, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced first-order logic and satisfiability modulo theories encodings for STL, which allow it to act as a portfolio solver. We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving correctness.
Comments29 pages, 7 figures
