Formalisation of Probabilistic Testing Semantics in Coq

Yuxin Deng; Jean Francois Monin

doi:10.1007/978-3-030-31175-9_16

Formalisation of Probabilistic Testing Semantics in Coq

Yuxin Deng^*
, Jean Francois Monin

^*Corresponding author for this work

Software Engineering Institute

Verimag

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Abstract

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 [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.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer Verlag
Pages	276-292
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-030-31175-9_16
State	Published - 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11760 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-030-31175-9_16

Cite this

Deng, Y., & Monin, J. F. (2019). Formalisation of Probabilistic Testing Semantics in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 276-292). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11760 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-31175-9_16

Deng, Yuxin ; Monin, Jean Francois. / Formalisation of Probabilistic Testing Semantics in Coq. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, 2019. pp. 276-292 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{a0d41b08a25e4b45bc81f4ecbd6798ef,

title = "Formalisation of Probabilistic Testing Semantics in Coq",

abstract = "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 [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.",

author = "Yuxin Deng and Monin, \{Jean Francois\}",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.",

year = "2019",

doi = "10.1007/978-3-030-31175-9\_16",

language = "英语",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "276--292",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "德国",

}

Deng, Y & Monin, JF 2019, Formalisation of Probabilistic Testing Semantics in Coq. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11760 LNCS, Springer Verlag, pp. 276-292. https://doi.org/10.1007/978-3-030-31175-9_16

Formalisation of Probabilistic Testing Semantics in Coq. / Deng, Yuxin; Monin, Jean Francois.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag, 2019. p. 276-292 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11760 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Formalisation of Probabilistic Testing Semantics in Coq

AU - Deng, Yuxin

AU - Monin, Jean Francois

PY - 2019

Y1 - 2019

N2 - 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 [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.

AB - 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 [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.

UR - https://www.scopus.com/pages/publications/85075054457

U2 - 10.1007/978-3-030-31175-9_16

DO - 10.1007/978-3-030-31175-9_16

M3 - 章节

AN - SCOPUS:85075054457

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 276

EP - 292

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -

Deng Y, Monin JF. Formalisation of Probabilistic Testing Semantics in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. 2019. p. 276-292. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-31175-9_16

Formalisation of Probabilistic Testing Semantics in Coq

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this