AI 中文总结
研究实时系统形式分析中无穷性的两个维度，提出基于归约的验证方法，整合重写、归约及约束存储等技术，引入折叠机制确保终止，通过验证协议评估，能统一支持多种实时模型分析，为实时重写理论符号验证提供基础。
AI 中文摘要
实时系统的形式分析必须处理无穷性的两个维度：代理和消息数量无界，以及密集时间导致的潜在无限状态空间。我们提出了一种新颖的基于归约的验证方法来处理这两个维度。该方法整合了：基于SMT重写以符号表示定时约束；使用逻辑变量归约以推理代理数量未知的系统；以及类似约束逻辑编程的部分实例化项的约束存储。还引入了折叠机制确保符号分析终止。此方法已作为Maude重写引擎的扩展实现。通过验证定时互斥协议的正确性进行评估，且该框架能统一支持其他实时模型分析。结果表明所提框架为实时重写理论的符号验证提供了合理且有表现力的基础。
英文摘要
The formal analysis of real-time systems must address two dimensions of infiniteness: an unbounded number of agents and messages, and a potentially infinite state space induced by dense time. We present a novel narrowing-based verification method that deals with both dimensions. Our approach integrates (i) rewriting modulo SMT for symbolic representation of timing constraints, (ii) narrowing with logical variables to reason about systems with an unknown number of agents, and (iii) a constraint store over partially instantiated terms, in the style of constraint logic programming. We further introduce a folding mechanism that, under certain conditions, ensures termination of the symbolic analysis. The method has been implemented as an extension of the Maude rewriting engine. We evaluate the approach by verifying the correctness of a timed mutual exclusion protocol without imposing bounds on the number of participating processes. Moreover, we show that the framework uniformly supports the analysis of other real-time models, including parametric timed automata with unspecified components that our method can synthesize. Our results suggest that the proposed framework provides a sound and expressive basis for the symbolic verification of real-time rewrite theories.
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 430-443
