tock-CSP 中的优先级机制

$tock$-CSP 编码在 CSP 中嵌入了一种丰富且灵活的建模离散时间行为的方法，其中事件 $tock$ 被解释为标记时间的流逝。模型检测器 FDR 为 $tock$-CSP 提供了专门支持，包括一个优先级算子，该算子通常用于确保最大进展，即仅在内部活动稳定后时间才推进。优先级本身也可作为一种建模构造独立使用。然而，其操作语义仅在 CSP 最具判别力的语义模型——有限线性模型上才是同余的。为了在 $tock$-CSP 设定中实现可靠且组合的推理，我们计算了优先级的指称定义。为此，我们在有限线性模型的一个特化（将 $tock$ 和表示终止的 $\checkmark$ 作为特殊事件）与 $\checkmark$-$tock$-CSP（一种捕获终止、截止时间且适于推理时间精化的 $tock$-CSP 模型）之间建立了一个 Galois 连接。我们的结果使用 Isabelle/HOL 进行了机械化。