Advertisement

Formalisation of Probabilistic Testing Semantics in Coq

  • Yuxin DengEmail author
  • Jean-Francois Monin
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)

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.

Notes

Acknowledgment

We would like to thank Yves Bertot for helpful discussion.

References

  1. 1.
  2. 2.
  3. 3.
    Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568–589 (2009)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Barthe, G., Crespo, J.M., Grégoire, B., Kunz, C., Zanella Béguelin, S.: Computer-aided cryptographic proofs. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 11–27. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32347-8_2CrossRefGoogle Scholar
  5. 5.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-662-07964-5CrossRefzbMATHGoogle Scholar
  6. 6.
    Deng, Y.: Semantics of Probabilistic Processes: An Operational Approach. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-45198-4CrossRefGoogle Scholar
  7. 7.
    Deng, Y., Feng, Y.: Probabilistic bisimilarity as testing equivalence. Inf. Comput. 257, 58–64 (2017)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Deng, Y., van Glabbeek, R.: Characterising probabilistic processes logically. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 278–293. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16242-8_20CrossRefGoogle Scholar
  9. 9.
    Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04081-8_19CrossRefGoogle Scholar
  10. 10.
    Deng, Y., Wu, H.: Modal characterisations of probabilistic and fuzzy bisimulations. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 123–138. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11737-9_9CrossRefGoogle Scholar
  11. 11.
    Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating labelled Markov processes. Inf. Comput. 184(1), 160–200 (2003)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Gonthier, G.: Formal proof – the four-color theorem. Not. Am. Math. Soc. 55(11), 1382–1393 (2008)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163–179. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39634-2_14CrossRefGoogle Scholar
  15. 15.
    Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sjöberg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Proceedings of OSDI 2016, pp. 653–669. USENIX Association (2016)Google Scholar
  16. 16.
    Hennessy, M.: Exploring probabilistic bisimulations, Part I. Formal Aspects Comput. 24(4–6), 749–768 (2012)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209(2), 154–172 (2011)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Jones, C.: Probabilistic nondeterminism. Ph.d. thesis, University of Edinburgh (1990)Google Scholar
  20. 20.
    Kennedy, A., Benton, N., Jensen, J.B., Dagand, P.: Coq: the world’s best macro assembler? In: Proceedings of PPDP 2013, pp. 13–24. ACM (2013)Google Scholar
  21. 21.
    Krebbers, R.: The C standard formalized in Coq. Ph.d. thesis, Radboud University Nijmegen (2015)Google Scholar
  22. 22.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: Proceedings of the 8th European Congress on Embedded Real Time Software and Systems. SEE (2016). https://hal.inria.fr/hal-01238879
  24. 24.
    Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  25. 25.
    Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981).  https://doi.org/10.1007/BFb0017309CrossRefGoogle Scholar
  26. 26.
    Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 287–301. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71389-0_21CrossRefzbMATHGoogle Scholar
  27. 27.
    van Breugel, F., Mislove, M.W., Ouaknine, J., Worrell, J.: Domain theory, testing and simulation for labelled Markov processes. Theoret. Comput. Sci. 333(1–2), 171–197 (2005)MathSciNetCrossRefGoogle Scholar
  28. 28.
    van Glabbeek, R.J., Smolka, S.A., Steffen, B., Tofts, C.M.N.: Reactive, generative, and stratified models of probabilistic processes. In: Proceedings of LICS 1990, pp. 130–141. IEEE Computer Society (1990)Google Scholar
  29. 29.
    Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: Proceedings of POPL 2012, pp. 427–440. ACM (2012)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Shanghai Key Laboratory of Trustworthy ComputingMOE International Joint Lab of Trustworthy Software, East China Normal UniversityShanghaiChina
  2. 2.Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAGGrenobleFrance

Personalised recommendations