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 = {}, timestamp = {Thu, 07 Nov 2019 17:02:36 +0100}, biburl = {}, bibsource = {dblp computer science bibliography,},
    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},

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3982359