行为度量：庞加莱提升的可组成性及其在 Up-To 技术中的应用
计算机科学中的逻辑
2024-07-24 v2
摘要
通过 coalgebra 为端函子建模的转换系统的行为距离将传统行为等价概念推广到定性环境，在该环境中，状态被赋予衡量其 (不)相似程度的度量。为转换系统赋予此类距离的做法本质上依赖于能够将描述转换系统一步行为的函子提升到伪度量空间的范畴。我们考虑了从运输论中抽象的庞加莱提升范畴论推广，适用于将函子提升到 quantale 值关系的情形，这涵盖了等价、序关系和（有向）度量。我们利用纤维范畴论的工具，使人们能够将庞加莱提升视为从适当的纤维伴随中产生。我们的主要贡献是庞加莱提升的可组成性结果，表明构成函子的提升等同于提升的组成。在此基础上，我们描述了在其中一个函子为多项式（具有有限余并）的情况下，如何提升分配律。这些结果是适用于 quantale 值行为距离的 Up-To 技术的关键要素。Up-To 技术是一种众所周知的共辩证技术，用于高效地给出行为距离的下界。我们在两个案例研究中展示了本文结果。
引用
@article{arxiv.2404.19632,
title = {Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques},
author = {Keri D'Angelo and Sebastian Gurke and Johanna Maria Kirss and Barbara König and Matina Najafi and Wojciech Różowski and Paul Wild},
journal= {arXiv preprint arXiv:2404.19632},
year = {2024}
}