基于模糊Lax扩展的行为半度量的特征逻辑
摘要：行为距离比行为等价或行为包含的两值概念提供了更精细的状态比较，在涉及概率、模糊或度量系统的系统中。与两值情况类似，系统类型的广泛变化需要适用于许多系统类型的通用方法。这种方法正在通用合代数范式中出现，基于沿着集合函子提升伪度量或通过模糊松弛延拓提升一般实值（模糊）关系的模糊松弛延拓。后者的一个直接好处是，它们允许通过模糊（双）仿真来限制行为距离，这些仿真本身不需要是半度量或伪度量。这类似于经典的仿真和双仿真，它们分别不需要是预序或等价关系。已知的通用伪度量提升，特别是通用的坎托罗维奇和Wasserstein提升，都可以通过选择定量模态来扩展为模糊松弛延拓。然后，我们的核心结果表明，事实上所有的模糊松弛延拓都是适当的一组定量模态（即所谓的Moss模态）的坎托罗维奇延拓。对于非扩张的模糊松弛延拓，这允许提取表征行为距离的定量模态逻辑，即满足Hennessy-Milner定理的定量版本；同样，我们获得了定量版本的Moss合代数逻辑的表达性。我们所有的结果明确适用于非对称距离（半度量），即定量模拟的概念。
作者：Paul Wild and Lutz Schr"oder
论文ID：2007.01033
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22