行为度量的定量分级语义和谱
摘要：行为度量提供了对具有定量数据的系统上经典的二值行为等价关系的定量细化，例如度量或概率转移系统。类似于传统的线性时间/分支时间谱上的二值行为等价关系在转移系统上的情况，行为度量具有各种粒度级别，这取决于观察者与系统进行交互的能力。已经证明分级单子代表行为等价谱的统一框架。在这里，我们将该原则转化为行为度量的谱，以一个更一般的共代数级别中进行工作，也就是在系统类型参数化的层面上。在定量分级语义的发展中，我们讨论了关于基于度量空间范畴中分级单子的表示以及分级定量等式理论的内容。此外，我们获得了不变的实值模态逻辑的规范泛型概念，并为此类逻辑提供了表现力准则，即逻辑距离与相应的行为距离一致。因此，我们恢复了最近对共代数分支时间度量和度量转移系统中跟踪距离的表现力结果，并获得了关于模糊转移系统跟踪语义的新表现力结果。我们还提供了一些重要的负面结果。特别地，我们证明了概率度量转移系统上的跟踪距离根本不适用于特征实值模态逻辑。
作者：Jonas Forster, Lutz Schr"oder, Paul Wild
论文ID：2306.01487
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-12