Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum
Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum
复制标题
线性时间-分支时间谱的分级单子和分级逻辑
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Lutz Schröder
中科院分区：
文献类型：
--
作者：
Ulrich Dorsch;Stefan Milius;Lutz Schröder
基于状态的并发系统模型传统上是在各种进程等价的概念下考虑的。在标记跃迁系统的特殊情况下，这些等效范围从迹等效到（强）双相似，并组织在所谓的线性时间分支时间谱中。通用协代数和分级单子的组合提供了一个通用框架，在这个框架中，并发的语义可以根据底层转换系统的分支类型和进程等价的粒度进行参数化。在本文中，我们证明了这个分级语义框架确实包含了线性时间分支时间谱中最重要的等价。分级语义的一个重要特征是它允许有原则地提取特征模态逻辑。在以前的工作中，我们已经在给定的分级语义下建立了这些分级逻辑的不变性；在本文中，我们用显式命题层扩展了逻辑框架，并提供了一个一般表达准则，将经典Hennessy-Milner定理推广到更粗糙的过程等价概念。我们在标记转移系统和概率系统上提取了一系列分级语义的分级逻辑，并基于我们的一般准则给出了它们的可表达性的示例证明。
State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the particular case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time -- branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time -- branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplaric proofs of their expressiveness based on our generic criterion.