bibtex

@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},
}


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

info visites 4187411