马尔可夫链上的等价距离的完整量化推导系统
摘要：有限标记马尔可夫链的等价关系距离的完全公理化 摘要：我们在本文中提出了对有限标记马尔可夫链的Desharnais等人所提出的等价关系距离的完全公理化。我们的公理化是以Mardare、Panangaden和Plotkin（LICS 2016）最近提出的数量扩展的等式逻辑风格为基础的，该逻辑使用以有理数为索引的等式关系t equiv_ε s，表示“t和s在误差ε内近似相等”。值得注意的是，我们的数量推理系统以自然方式扩展了Stark和Smolka对于概率等价关系的等式系统，通过引入用于处理概率分布之间的Kantorovich距离的公理。然后，我们利用这个公理化提出了对有限标记马尔可夫链的Kleene风格表示定理的度量扩展，该定理由Silva等人（Inf. Comput. 2011）以更一般的协代数形式提出。
作者：Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Radu Mardare
论文ID：1702.02528
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22