Abstract
We present a formal proof system for compositional verification of probabilistic concurrent processes. Processes are specified using an SOS-style process algebra with probabilistic operators. Properties are expressed using a probabilistic modal μ-calculus. And the proof system is formulated as a sequent calculus in which sequents are given a quantitative interpretation. A key feature is that the probabilistic scenario is handled by introducing the notion of Markov proof, according to which proof trees contain probabilistic branches and are required to satisfy a condition formulated by interpreting them as Markov Decision Processes. We present simple but illustrative examples demonstrating the applicability of the approach to the compositional verification of infinite state processes. Our main result is the soundness of the proof system, which is proved by applying the coupling method from probability theory to the game semantics of the probabilistic modal μ-calculus.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)
Bartels, F.: GSOS for probabilistic transition systems. Electronic Notes in Theoretical Computer Science 65(1) (2002)
Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. Journal of Logic and Computation 21(6), 1177–1216 (2011)
Cardelli, L., Larsen, K.G., Mardare, R.: Modular Markovian Logic. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 380–391. Springer, Heidelberg (2011)
Chatterjee, K.: Stochastic ω-Regular Games. PhD thesis, University of California, Berkeley (2007)
Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract Probabilistic Automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative Multi-objective Verification for Probabilistic Systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112–127. Springer, Heidelberg (2011)
Hájek, P.: Metamathematics of Fuzzy Logic. Trends in Logic. Springer (2001)
Henzinger, T.A., Sifakis, J.: The Embedded Systems Design Challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1–15. Springer, Heidelberg (2006)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. of 12th LICS (1997)
Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-Guarantee Verification for Probabilistic Systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23–37. Springer, Heidelberg (2010)
McIver, A., Morgan, C.: Results on the quantitative μ-calculus qMμ. ACM Transactions on Computational Logic 8(1) (2007)
Mio, M.: Game Semantics for Probabilistic μ-Calculi. PhD thesis, School of Informatics, University of Edinburgh (2012)
Mio, M.: On the equivalence of denotational and game semantics for the probabilistic μ-calculus. Logical Methods in Computer Science 8(2) (2012)
Niwinski, D., Walukiewicz, I.: Games for the μ-calculus. Theoretical Computer Science 163, 99–116 (1997)
Panangaden, P.: Labelled Markov processes. Imperial College Press (2009)
Pnueli, A.: The temporal logic of programs. In: Proc. of 19th FOCS (1977)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Laboratory for Computer Science, M.I.T (1995)
Simpson, A.: Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS. Journal of Logic and Algebraic Programming 60-61, 287 (2004)
Stirling, C.: Modal and temporal logics for processes. Springer (2001)
Studer, T.: On the proof theory of the modal mu-calculus. Studia Logica 89(3) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mio, M., Simpson, A. (2013). A Proof System for Compositional Verification of Probabilistic Concurrent Processes. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)