名义转换系统的模态逻辑
摘要：一般转换系统中的状态和动作标签可以来自任意的名称集合，动作可以绑定名称，而来自任意逻辑的状态谓词定义了状态的属性。我们介绍了这些系统的Hennessy-Milner逻辑，并证明了它对于仿真等价是充分且表达完备的。一个主要的技术创新是使用有限支持的无穷连词。我们展示了如何以系统性方式处理不同的仿真变体，如早期、晚期、开放和弱仿真等，并探讨传统的定理中状态谓词可以被动作取代的问题，并与相关工作进行了实质性的比较。主要的定义和定理已在Nominal Isabelle中进行了形式化。
作者：Joachim Parrow, Johannes Borgstr"om, Lars-Henrik Eriksson, Ram=unas Forsberg Gutkovas, Tjark Weber
论文ID：1904.02564
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22