线性时间—分支时间谱的 graded 单子与 graded 逻辑
计算机科学中的逻辑
2020-10-21 v3 范畴论
摘要
基于状态的并发系统模型传统上在各种进程等价性概念下被考量。在标号迁移系统的特定情形下，这些等价性从迹等价性到（强）互模拟不等，并被组织为所谓的线性时间—分支时间谱。泛化余代数与 graded 单子的结合提供了一个通用框架，其中并发的语义可同时在底层迁移系统的分支类型和进程等价性的粒度上进行参数化。我们在本文中表明，这一 graded 语义框架确实包含了线性时间—分支时间谱中最重要的等价性。graded 语义的一个重要特征是它允许原则性地提取特征模态逻辑。我们已在早期工作中确立了这些 graded 逻辑在给定的 graded 语义下的不变性；在本文中，我们通过显式命题层扩展了该逻辑框架，并提供了一个泛化经典 Hennessy-Milner 定理至更粗进程等价性概念的通用表达力准则。我们为标号迁移系统和概率系统上的一系列 graded 语义提取了 graded 逻辑，并基于我们的通用准则给出了其表达力的示例性证明。
引用
@article{arxiv.1812.01317,
title = {Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum},
author = {Ulrich Dorsch and Stefan Milius and Lutz Schröder},
journal= {arXiv preprint arXiv:1812.01317},
year = {2020}
}