非确定性概率选择下分支双态等价的完备公理化
计算机科学中的逻辑
2025-02-11 v1
摘要
本文提出了一种非确定性概率过程的分支双态等价概念。为了表征相应的根分支概率双态等价，提出了一种用于基本、无递归过程语言的等式理论，该语言包含非确定性选择和概率选择。该公理化的完备性证明一方面依赖于强概率双态等价的完备性，另一方面依赖于具体过程的概念，即不显示（部分）惰性 τ-move 的过程。该方法首先针对该计算的非确定性片段进行展示，然后推广到包含概率选择。
引用
@article{arxiv.2502.05631,
title = {A Complete Axiomatization of Branching Bisimilarity for a Simple Process Language with Probabilistic Choice},
author = {Rob van Glabbeek and Jan Friso Groote and Erik de Vink},
journal= {arXiv preprint arXiv:2502.05631},
year = {2025}
}
备注
Written in 2019. Dedicated to Catuscia Palamidessi, on the occasion of her 60th birthday. Extended abstract in The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, LNCS 11760, Springer, 2019, pp. 139-162, doi:10.1007/978-3-030-31175-9_9