Advertisement

Weak bisimulation for fully probabilistic processes

  • Christel Baier
  • Holger Hermanns
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

Bisimulations that abstract from internal computation have proven to be useful for verification of compositionally defined transition system. In the literature of probabilistic extensions of such transition systems, similar bisimulations are rare. In this paper, we introduce weak bisimulation and branching bisimulation for transition systems where nondeterministic branching is replaced by probabilistic branching. In contrast to the nondeterministic case, both relations coincide. We give an algorithm to decide weak bisimulation with a time complexity cubic in the number of states of the transition system. This meets the worst case complexity for deciding branching bisimulation in the nondeterministic case.

Keywords

Transition System Composition Operator Probabilistic Case Probabilistic Process Internal Computation 
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

  1. 1.
    G. Adel'son-Velshii, Y. Landis: An Algorithm for the Organization of Information. Soviet. Math. Dokl. 3, pp 1259–1262, 1962.Google Scholar
  2. 2.
    A. Aziz, V. Singhal, F. Balarin, R. Brayton, A. Sangiovanni-Vincentelli: It usually works: The Temporal Logic of Stochastic Systems. Proc. CAV'95, LNCS 939, pp 155–165, 1995.Google Scholar
  3. 3.
    C. Baier: Polynomial Time Algorithms for Testing probabilistic Bisimulation and Simulation. Proc. CAV'96, LNCS 1102, pp 38–49, 1996.Google Scholar
  4. 4.
    C. Baier, H. Hermanns: Weak Bisimulation for Fully Probabilistic Processes. Techn. Bericht IMMD-VII/1-97, Universität Erlangen.Google Scholar
  5. 5.
    A. Bianco, L. de Alfaro: Model Checking of Probabilistic and Nondeterministic Systems. Proc. Foundations of Software Technology and Theoretical Computer Science, LNCS 1026, pp 499–513, 1995.Google Scholar
  6. 6.
    G. Chehaivbar, H. Garavel, N. Tawbi, F. Zulian: Specification and Verification of the Powerscale Bus Arbitration Protocol: An Industrial Experiment with LOTOS. Formal Description Techniques IX, Chapmann Hall, 1996.Google Scholar
  7. 7.
    I. Christoff: Testing Equivalences and Fully Abstract Models for Probabilistic Processes, Proc. CONCUR'90, LNCS 458, pp 126–140, 1990.Google Scholar
  8. 8.
    L. Christoff, I. Christoff: Efficient Algorithms for Verification of Equivalences for Probabilistic Processes. Proc. CAV'91, LNCS 575, pp 310–321, 1991.Google Scholar
  9. 9.
    R. Cleaveland, S. Smolka, A. Zwarico: Testing Preorders for Probabilistic Processes. Proc. ICALP'92, LNCS 623, pp 708–719, 1992.Google Scholar
  10. 10.
    D. Coppersmith, S. Winograd: Matrix Multiplication via Arithmetic Progressions. Proc. 19th ACM Symposium on Theory of Computing, pp 1–6, 1987.Google Scholar
  11. 11.
    C. Courcoubetis, M. Yannakakis: Verifying Temporal Properties of Finite-State Probabilistic Programs. Proc. FOCS'88, pp 338–345, 1988.Google Scholar
  12. 12.
    A. Giacalone, C. Jou, S. Smolka: Algebraic Reasoning for Probabilistic Concurrent Systems. Proc. IFIP TC2 Working Conf. on Programming Concepts and Methods, 1990.Google Scholar
  13. 13.
    R. van Glabbeek, S.A. Smolka, and B. Steffen: Reactive, generative, and stratified models of probabilistic processes. Information and Computation, Vol 121, pp 59–80, 1995.Google Scholar
  14. 14.
    R. van Glabbeek, W. Weijland: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), pp. 555–600, 1996.Google Scholar
  15. 15.
    J. Groote, F. Vaandrager: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. Proc. ICALP'90, LNCS 443, 1990.Google Scholar
  16. 16.
    P. Halmos: Measure Theory. Springer-Verlag, 1950.Google Scholar
  17. 17.
    H. Hansson: Time and Probability in Formal Design of Distributed Systems. Ph.D.Thesis, Uppsala University, 1994.Google Scholar
  18. 18.
    H. Hansson, B. Jonsson: A Calculus for Communicating Systems with Time and Probabilities. Proc. IEEE Real-Time Systems Symposium, 1990.Google Scholar
  19. 19.
    H. Hansson, B. Jonsson: A Logic for Reasoning about Time and Probability. Formal Aspects of Computing, Vol. 6, pp 512–535, 1994.Google Scholar
  20. 20.
    S. Hart, M. Sharir: Probabilistic Temporal Logic for Finite and Bounded Models. Proc. 16th ACM Symposium on Theory of Computing, 1984.Google Scholar
  21. 21.
    T. Huynh, L. Tian: On some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae, Vol. 17, pp 211–234, 1992.Google Scholar
  22. 22.
    B. Jonsson, K.G. Larsen: Specification and Refinement of Probabilistic Processes. Proc. LICS'91, pp 266–277,1991.Google Scholar
  23. 23.
    B. Jonsson, W. Yi: Compositional Testing Preorders for Probabilistic Processes. Proc, LICS'95, pp 431–443, 1995.Google Scholar
  24. 24.
    C.C. Jou, S. Smolka: Equivalences, Congruences and Complete Axiomatizations for Probabilistic Processes. Proc. CONCUR'90, LNCS 458, pp 367–383, 1990.Google Scholar
  25. 25.
    P. Kanellakis, S. Smolka: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation, Vol. 86, pp 43–68, 1990.Google Scholar
  26. 26.
    K. Larsen, A. Skou: Bisimulation through Probabilistic Testing. Information and Computation, Vol. 94, pp 1–28, 1991.Google Scholar
  27. 27.
    K. Larsen, A. Skou: Compositional Verification of Probabilistic Processes. Proc. CONCUR'92, LNCS 630, pp 456–471, 1992.Google Scholar
  28. 28.
    R. Milner: Calculi for Synchrony and Asynchrony. Theoretical Computer Science, Vol. 25, pp 269–310, 1983.Google Scholar
  29. 29.
    R. Milner: Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  30. 30.
    R. Paige, R. Tarjan: Three Partition Refinement Algorithms. SIAM Journal of Computing, Vol. 16, No. 6, pp 973–989, 1987.Google Scholar
  31. 31.
    A. Pnueli, L. Zuck: Verification of Multiprocess Probabilistic Protocols. Distributed Computing, Vol. 1, No. 1, pp 53–72, 1986.Google Scholar
  32. 32.
    A. Pnueli, L. Zuck: Probabilistic Verification. Information and Computation, Vol. 103, pp 1–29, 1993.Google Scholar
  33. 33.
    R. Segala, N. Lynch: Probabilistic Simulations for Probabilistic Processes. Proc. CONCUR 94, LNCS 836, pp 481–496, 1994.Google Scholar
  34. 34.
    M. Vardi: Automatic Verification of Probabilistic Concurrent Finite-State Programs. Proc. FOCS'85, pp 327–338, 1985.Google Scholar
  35. 35.
    M. Vardi, P. Wolper: An Automata-Theoretic Approach to Automatic Program Verification. Proc. LICS'86, pp 332–344, 1986.Google Scholar
  36. 36.
    S. Yuen, R. Cleaveland, Z. Dayar, S. Smolka: Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes. Proc. CONCUR'94, LNCS 836, pp 497–512, 1994.Google Scholar
  37. 37.
    W. Yi, K. Larsen: Testing Probabilistic and Nondeterminsitic Processes. Protocol Specification, Testing and Verification XII, Elsevier Science Publishers, IFIP, pp 47–61, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Christel Baier
    • 1
  • Holger Hermanns
    • 2
  1. 1.Fakultät für Mathematik & InformatikUniversität MannheimGermany
  2. 2.Informatik VIIUniversität ErlangenGermany

Personalised recommendations