Abstract
A branching bisimulation for probabilistic systems that is preserved under parallel composition has been defined recently for the alternating model. We show that besides being compositional, it is decidable in polynomial time and it preserves the properties expressible in probabilistic Computation Tree Logic (pCTL). In the ground-complete axiomatization, only a single axiom is added to the axioms for strong bisimulation. We show that the Concurrent Alternating Bit protocol can be verified using the process algebra and a set of recursive rules.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aceto, L., Ésik, Z., Ingólfsdóttir, A.: Equational axioms for probabilistic bisimilarity. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 239–253. Springer, Heidelberg (2002)
Andova, S., Baeten, J.C.M., D’Argenio, P.R., Willemse, T.A.C.: A compositional merge of probabilistic processes in the alternating model. In: NWPT 2006 (2006)
Andova, S., Baeten, J.C.M., Willemse, T.A.C.: A complete axiomatisation of branching bisimulation for probabilistic systems with an application in protocol verification. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 327–342. Springer, Heidelberg (2006)
Andova, S., Georgievska, S., Trčka, N.: On compositionality, efficiency, and applicability of abstraction in probabilistic systems (2008), http://www.win.tue.nl/~sgeorgie/processalgebra.pdf
Andova, S., Willemse, T.A.C.: Branching bisimulation for probabilistic systems: characteristics and decidability. Theor. Comput. Sci. 356(3), 325–355 (2006)
Baeten, J.C.M., Bravetti, M.: A ground-complete axiomatization of finite state processes in process algebra. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 248–262. Springer, Heidelberg (2005)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)
Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149–214 (2005)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11(3), 125–155 (1998)
Bandini, E., Segala, R.: Axiomatizations for probabilistic bisimulation. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 370–381. Springer, Heidelberg (2001)
Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. JACM 42(2), 458–487 (1995)
Deng, Y., Palamidessi, C., Pang, J.: Compositional reasoning for probabilistic finite-state behaviors. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 309–337. Springer, Heidelberg (2005)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for PCTL*. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 355–370. Springer, Heidelberg (2002)
van Glabbeek, R.J., Weijland, P.: Branching time and abstraction in bisimulation semantics. JACM 43(3), 555–600 (1996)
Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)
Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)
Mislove, M.W., Ouaknine, J., Worrell, J.: Axioms for probability and nondeterminism. ENTCS 96, 7–28 (2004)
Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)
Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic J. of Computing 2(2), 250–273 (1995)
Segala, R., Turrini, A.: Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: QEST 2005, pp. 44–53. IEEE Computer Society Press, Los Alamitos (2005)
Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1–43. Springer, Heidelberg (2004)
Trčka, N., Georgievska, S.: Branching bisimulation congruence for probabilistic systems. In: QAPL 2008, ENTCS (to appear, 2008), http://www.win.tue.nl/~sgeorgie/TG08report.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andova, S., Georgievska, S. (2009). On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)