Abstract
We study which standard operators of probabilistic process calculi allow for compositional reasoning with respect to bisimulation metric semantics. We argue that uniform continuity (generalizing the earlier proposed property of non-expansiveness) captures the essential nature of compositional reasoning and allows now also to reason compositionally about recursive processes. We characterize the distance between probabilistic processes composed by standard process algebra operators. Combining these results, we demonstrate how compositional reasoning about systems specified by continuous process algebra operators allows for metric assume-guarantee like performance validation.
Chapter PDF
Similar content being viewed by others
Keywords
- Operational Semantic
- Parallel Composition
- Compositionality Property
- Process Algebra
- Probabilistic Process
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
Bacci, G., Bacci, G., Larsen, K.G., Mardare, R.: Computing Behavioral Distances, Compositionally. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 74–85. Springer, Heidelberg (2013)
Bartels, F.: On Generalised Coinduction and Probabilistic Specification Formats. Ph.D. thesis, VU University Amsterdam (2004)
van Breugel, F., Worrell, J.: A Behavioural Pseudometric for Probabilistic Transition Systems. TCS 331(1), 115–142 (2005)
D’Argenio, P.R., Lee, M.D.: Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol. 7213, pp. 452–466. Springer, Heidelberg (2012)
De Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: Proc. LICS 2007, pp. 99–108. IEEE (2007)
De Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the Future in Systems Theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)
Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for Action-labelled Quantitative Transition Systems. ENTCS 153(2), 79–96 (2006)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for Labelled Markov Processes. TCS 318(3), 323–354 (2004)
Fahrenberg, U., Legay, A.: The quantitative linear-time-branching-time spectrum. TCS 538, 54–69 (2014)
Fokkink, W.: Modelling Distributed Systems. Springer (2007)
Gebler, D., Tini, S.: Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators. In: Proc. EXPRESS/SOS 2014. EPTCS, vol. 160, pp. 63–78 (2014)
Lee, M.D., Gebler, D., D’Argenio, P.R.: Tree Rules in Probabilistic Transition System Specifications with Negative and Quantitative Premises. In: Proc. EXPRESS/SOS 2012. EPTCS, vol. 89, pp. 115–130 (2012)
Mio, M.: Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 335–350. Springer, Heidelberg (2014)
Mio, M., Simpson, A.: A Proof System for Compositional Verification of Probabilistic Concurrent Processes. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 161–176. Springer, Heidelberg (2013)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis. MIT (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gebler, D., Larsen, K.G., Tini, S. (2015). Compositional Metric Reasoning with Probabilistic Process Calculi. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)