@inproceedings{DM9,
title = {Formalisation of Probabilistic Testing Semantics in Coq },
author = {Deng, Yuxin and Monin, Jean-Fran\c{c}ois},
year = {2019},
booktitle = {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},
pages = {276--292},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {11760},
team = {PACSS},
pdf = {https://www-verimag.imag.fr/~monin/Publis/Docs/fc19-probatesting_long.pdf},
timestamp = {Thu, 07 Nov 2019 17:02:36 +0100},
biburl = {https://dblp.org/rec/bib/conf/birthday/DengM19},
bibsource = {dblp computer science bibliography, https://dblp.org},
abstract = {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},
}
