一句话：通过引入对全局历史中原子的新鲜性测试，扩展 nominal μ-演算，并证明其模型检测可判定。
带有原子的 μ-演算（nominal μ-演算）是一种时序逻辑，用于推理在无限数据域上运行、原子仅可按相等性比较的迁移系统。然而，它不足以定义系统验证中一些感兴趣的性质。为此，作者将演算扩展为带有相对于迁移全局历史的原子新鲜性测试。由于全局历史可能任意增长，扩展后演算的模型检测是否可判定并不显然。论文证明它是可判定的，方法是指出只需关注历史中局部相关的部分，从而将无限历史问题约化为局部信息。
The μ -calculus with atoms, or nominal μ -calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.
DOI 原文 ·
@inproceedings{paperbot4972,
title = {History-Dependent Nominal μ-Calculus},
author = {Clovis Eberhart and Bartek Klin},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785736}
}