一句话：为名义迁移系统建立 Hennessy-Milner 逻辑，证明对双模拟表达完全并机器化。
论文研究状态与动作标签取自任意名义集合、动作可绑定名字、状态谓词由任意逻辑给出的迁移系统。作者定义此类名义迁移系统，并引入相应的 Hennessy-Milner 模态逻辑，其关键技术是有限支撑的无穷合取。该逻辑被证明对双模拟等价既可靠又表达完全，并能系统处理 early、late、open、weak 等双模拟变体；还探讨状态谓词可由动作替代的民间定理并与相关工作比较。主要定义和定理已在 Nominal Isabelle 中形式化。
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.
@article{paperbot1345,
title = {Modal Logics for Nominal Transition Systems},
author = {Joachim Parrow and Johannes Borgström and Lars-Henrik Eriksson and Ramūnas Forsberg Gutkovas and Tjark Weber},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:6)2021}
}