Formalisation of Probabilistic Testing Semantics in Coq
Yuxin Deng and Jean-Francois Monin
Van Breugel et al. [F. van Breugel et al, Theor. Comput. Sci. 333(1-2):171-197, 2005]
have given an elegant testing framework that can characterise probabilistic bisimulation,
but its completeness proof is highly involved. Deng and Feng [Y. Deng and Y. Feng,
Inf. Comput. 257:58-64, 2017] have simplified that result for finite-state processes.
The crucial part in the latter work is an algorithm that can construct enhanced tests.
We formalise the algorithm and prove its correctness by maintaining a number of subtle
invariants in Coq. To support the formalisation, we develop a reusable library for
manipulating finite sets. This sets an early example of formalising probabilistic
concurrency theory or quantitative aspects of concurrency theory at large, which is
a rich field to be pursued.