Eilenberg-Moore 煤代数的分级语义和分级逻辑
摘要：关于具有状态的系统的抽象研究，也就是co-algebra，自然地具有一个将表现相同的状态识别为行为等价的概念。然而，在许多情况下，这种等价关系比预期的语义更加精细。特别是在自动机理论中，非确定性自动机的行为等价本质上是相似性等价，因此与语言等价并不一致。语言等价可以通过确定化时的行为等价来捕捉，确定化是通过标准的幂集构造获得的。假设在确定可接受结构类型（例如，词语语言）和捕捉分支类型（例如，非确定性、加权、概率性）的单子谱（monad）之间存在所谓的Eilenberg-Moore分配法（distributive law），则可以将此构造推广到co-algebraic广义。 Eilenberg-Moore样式的co-algebraic语义在本意义上已被更一般的分级语义框架基本包含，该框架主要基于分级单子谱（graded monad）。分级语义具有一系列通用结果，尤其是关于不变性和在适当条件下给定语义的专门模态逻辑的表达性；值得注意的是，这些逻辑是在原始状态空间上评估的。我们表明，将这些分级逻辑实例化为Eilenberg-Moore样式语义的情况非常顺利，并且在基本上所有感兴趣的情况下提供了表达性的模态逻辑。我们另外将该框架参数化为一个真值的量子群，因此特别包括了两值等价和量化等价（即，行为距离）。
作者：Jonas Forster, Lutz Schr"oder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara K"onig, Karla Messing
论文ID：2307.14826
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-28