Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

技术摘要：用于实时系统逻辑分析中的延迟约束（Delayed Constraints）

问题陈述
实时系统的形式化分析在处理“无限性”方面面临两个主要挑战：代理（agents）和消息数量可能无界，以及由于稠密时间（dense time）导致的态空间无限。传统的重写逻辑（Rewriting Logic, RL）验证方法（特别是在 Maude 重写引擎中实现的实现方式）在历史上受到了限制。虽然 Maude 支持具有完整指定组件（基项/ground terms）和 SMT 约束的系统的不变量验证，但它难以处理包含未知数量代理或任意参数的系统。此外，现有的符号技术通常依赖于时间采样，这在稠密时间设置下缺乏可靠性（soundness）和完备性（completeness）。使用逻辑变量处理无界代理的现有方法往往会导致半判定程序（semi-decision procedures），其搜索空间是无限的，且缺乏保证终止的机制。

方法论
作者提出了一个创新的验证框架，该框架集成了三种核心技术来解决上述局限性：

1. 基于 SMT 的重写（Rewriting Modulo SMT）： 利用 SMT 理论对时间约束进行符号表示。
2. 带有逻辑变量的窄化（Narrowing with Logical Variables）： 使用逻辑变量对具有未知或任意数量代理的系统进行推理。
3. 延迟约束与折叠（Delayed Constraints and Folding）： 受约束逻辑编程（CLP）启发，引入了一个针对部分实例化项的约束存储器。

其核心创新是延迟折叠窄化（Delayed Folding Narrowing）。与标准窄化不同，该方法允许规则条件中的 SMT 表达式包含“延迟”部分——即那些在项被进一步实例化之前无法求值的子表达式。这是通过 SMT 扩展实现的，其中非有效的 SMT 表达式（例如，代表最大经过时间的 mte(t, T')）被抽象为新鲜变量。这些约束被累积起来，并仅在项被充分实例化后才进行求解或传播。

该框架定义了逻辑实时重写理论（Logical Real-Time Rewrite Theories），它扩展了标准的实时重写理论，使其允许：

• 重写规则的条件中包含带有延迟部分的 SMT 表达式。
• 右侧（RHS）可以包含不在左侧（LHS）中出现的变量。
• 查询可以在初始状态和目标状态中包含共享变量。

为了确保终止，该方法采用了折叠机制（folding mechanism）。构建一个状态图，如果一个符号状态 $v'$ 是另一个已探索状态在等式理论下的实例，则将其移除。作者证明，在特定条件下（特别是精心设计的类型层级/sort hierarchy），这种折叠偏序关系能确保有限的搜索空间，从而将半判定程序转化为不变量验证的判定程序。

主要贡献

1. 延迟折叠窄化： 定义并实现了一种能够处理带有延迟约束的扩展 SMT 表达式的窄化关系。这使得验证具有任意逻辑变量和 SMT 变量的系统（无论是在初始配置还是不变量中）成为可能。
2. 定时 Fischer 协议的验证： 本文展示了对定时 Fischer 互斥协议在最一般设置下的首次自动验证。这包括任意数量的进程以及任意的定时参数（$\gamma$ 和 $\delta$）。这是通过设计特定的类型层级以保证折叠程序的终止，并利用逻辑变量来表示未指定的进程数量来实现的。
3. 进餐哲学家问题的控制器合成： 该框架被应用于定时进餐哲学家问题以合成一个控制器（“仆人/lackey”）。通过将控制器的转换保持未指定状态（由逻辑变量表示），窄化程序合成了满足可达性属性（例如，特定哲学家在截止日期前进入餐厅）所需的缺失转换。

结果
该方法已作为 Maude 重写引擎的一个扩展通过元级特性实现。

• Fischer 协议： 作者成功验证了任意数量进程下的互斥性。当初始状态受到 $\gamma > \delta$ 的约束时，由于折叠机制，搜索空间是有限的（仅包含 3 个状态），工具确认没有任何可达状态违反不变量。相反，当 $\delta \ge \gamma$ 时，找到了反例。
• 进餐哲学家： 系统成功合成了一个允许特定哲学家进入餐厅的“仆人”自动机。输出提供了一组具体的转换和控制器的位置，展示了该框架处理合成任务的能力。
• 效率： 折叠机制显著减少了搜索空间，使得能够分析那些在其他情况下因无限状态空间而难以处理的系统。

意义与主张
本文声称为实时重写理论的符号验证提供了一个可靠且具有表达力的基础。其重要性在于弥合了逻辑编程的表达力（通过逻辑变量处理无界代理）与实时分析的精确性（通过 SMT 和延迟约束处理稠密时间）之间的鸿沟。

作者强调，他们的方法超越了“标准”Maude 和现有的参数化定时自动机（PTA）工具，后者通常需要固定的进程数量或固定的时间界限。通过在单一框架内支持任意参数和无界数量的代理，该方法为分析复杂的实时模型（包括缺失系统组件的合成）提供了一种统一的方法。这项工作表明，延迟约束是实现无限状态实时系统符号分析中终止的关键机制。