用于保持历史互模拟的带逆向模态词的逻辑
计算机科学中的逻辑
2011-08-24 v1
摘要
我们引入了事件标识符逻辑（EIL），它通过增加(1)逆向和正向模态词，以及(2)用于跟踪事件的标识符，扩展了Hennessy-Milner逻辑。我们证明了在特定的真并发模型（即稳定配置结构）中，该逻辑对应于遗传性保持历史（HH）互模拟等价。我们进一步展示了EIL的自然子逻辑如何对应于更粗的等价关系。特别地，我们提供了弱保持历史（WH）和保持历史（H）互模拟的逻辑刻画。据我们所知，对应于HH和H互模拟的逻辑此前已有研究，但尚无针对WH互模拟（当允许自动并发时）的逻辑。我们还提出了特征公式，用于刻画关于保持历史等价的各个独立结构。
引用
@article{arxiv.1108.4470,
title = {A Logic with Reverse Modalities for History-preserving Bisimulations},
author = {Iain Phillips and Irek Ulidowski},
journal= {arXiv preprint arXiv:1108.4470},
year = {2011}
}
备注
In Proceedings EXPRESS 2011, arXiv:1108.4077