Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Polynomial time algorithms for testing probabilistic bisimulation and simulation

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 1102))

Included in the following conference series:

  • 476Accesses

Abstract

Various models and equivalence relations or preorders for probabilistic processes are proposed in the literature. This paper deals with a model based on labelled transition systems extended to the probabalistic setting and gives anO(n2·m) algorithm for testing probabilistic bisimulation and anO (n5·m2) algorithm for testing probabilistic simulation wheren is the number of states andm the number of transitions in the underlying probabilistic transition systems.

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

  1. R. Alur, C. Courcoubetis, D. Dill: Verifying Automata Specifications of Probabilistic Real-Time Systems, Proc. REX Workshop, Mook, The Netherlands, Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, C. Rozenberg (eds.), Lecture Notes in Computer Science 600, pp 27–44, 1991.

    Google Scholar 

  2. C. Baier, M. Kwiatkowska: Domain Equations for Probabilistic Processes, submitted for publication.

    Google Scholar 

  3. T. Bolognesi, S. Smolka: Fundamental Results for the Verification of Observational Equivalence: a Survey, Protocol Specification, Testing and Verification, Elsevier Science Publishers, IFIP, pp 165–179, 1987.

    Google Scholar 

  4. R. Cleaveland, J. Parrow, B. Steffen: A Semantics-Based Verification Tool for Finite State Systems, Protocol Specification, Testing and Verification IX, Elsevier Science Publishers, IFIP, pp 287–302, 1990.

    Google Scholar 

  5. R. Cleaveland, S. Smolka, A. Zwarico: Testing Preorders for Probabilistic Processes, Proc. ICALP 1992, Lecture Notes in Computer Science 623, Springer-Verlag, pp 708–719, 1992.

    Google Scholar 

  6. C. Courcoubetis, M. Yannakakis: Verifying Temporal Properties of Finite-State Probabilistic Programs, Proc. 29th Annual Symp. on Foundations of Computer Science, pp 338–345, 1988.

    Google Scholar 

  7. E. Dinic: Algorithm for Solution of a Problem of Maximal Flow in a Network with Power Estimation, Soviet. Math. Dokl., Vol. 11, pp 1277–1280, 1970.

    Google Scholar 

  8. R. Enders, T. Filkorn, D. Taubner: Generating BDDs fir Symbolic Model checking in CCS, Distributed Computing, Vol. 6, pp 155–164, 1993.

    Google Scholar 

  9. S. Even: Graph Algorithms, Computer Science Press, 1979.

    Google Scholar 

  10. L. Ford, D. Fulkerson: Flows in Networks, Princeton University Press, 1962.

    Google Scholar 

  11. J. Groote, F. Vaandrager: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence, Proc. 17th International Colloqium Warwick, Automata, Languages and Programming, Lecture Notes in Computer Science 443, pp 626–638, 1990.

    Google Scholar 

  12. H. Hansson: Time and Probability in Formal Design of Distributed Systems, Ph.D.Thesis, Uppsala University, 1994.

    Google Scholar 

  13. H. Hansson, B. Jonsson: A Logic for Reasoning about Time and Probability, Formal Aspects of Computing, Vol. 6, pp 512–535, 1994.

    Article  Google Scholar 

  14. S. Hart, M. Sharir: Probabilistic temporal logic for finite and bounded models, Proc. 16th ACM Symposium on Theory of Computing, pp 1–13, 1984.

    Google Scholar 

  15. B. Jonsson, K.G. Larsen: Specification and Refinement of Probabilistic Processes, Proc. 6th IEEE Symp. on Logic in Computer Science, 1991.

    Google Scholar 

  16. B. Jonsson, W. Yi: Compositional Testing Preorders for Probabilistic Processes, Proc. 10th IEEE Symp. on Logic in Computer Science, pp 431–443, 1995.

    Google Scholar 

  17. P. Kannelakis, S. Smolka: CCS Expressions, Finite State Processes and Three Problems of Equivalence, Proc. 2nd ACM Symposium on the Pronciples of Distributed Computing, pp 228–240, 1983.

    Google Scholar 

  18. K. Larsen, A. Skou: Bisimulation through Probabilistic Testing, Information and Computation, Vol. 94, pp 1–28, 1991.

    Article  Google Scholar 

  19. D. Lehmann, S. Shelah: Reasoning with Time and Chance, Information and Control, Vol. 53, pp 165–198, 1982.

    Article  Google Scholar 

  20. V. Malhotra, M. Pramodh Kumar, S. Maheshwari: AnO(¦V3¦) Algorithm for Finding Maximum Flows in Networks, Computer Science Program, Indian Institute of Technology, Kanpur 208016, 1978.

    Google Scholar 

  21. R. Milner: Communication and Concurrency, Prentice Hall, 1989.

    Google Scholar 

  22. R. Paige, R. Tarjan: Three Partition Refinement Algorithms, SIAM Journal of Computing, Vol. 16, No. 6, pp 973–989, 1987.

    Article  Google Scholar 

  23. A. Pnueli, L. Zuck: Verification of Multiprocess Probabilistic Protocols, Distributed Computing, Vol. 1, No. 1, pp 53–72, 1986.

    Article  Google Scholar 

  24. A. Pnueli, L. Zuck: Probabilistic Verification, Information and Computation, Vol. 103, pp 1–29, 1993.

    Article  Google Scholar 

  25. R. Segala, N. Lynch: Probabilistic Simulations for Probabilistic Processes, Proc. CONCUR 94, Theories of Concurrency: Unification and Extension, Lecture Notes in Computer Science 836, Springer-Verlag, pp 492–493, 1994.

    Google Scholar 

  26. R. van Glabbeek, S. Smolka, B. Steffen, C. Tofts: Reactive, Generative, and Stratified Models for Probabilistic Processes, Proc. 5th IEEE Symposium on Logic in Computer Science, pp 130–141, 1990.

    Google Scholar 

  27. M. Vardi: Automatic Verification of Probabilistic Concurrent Finite-State Programs, Proc. 26th Symp. on Foundations of Computer Science, pp 327–338, 1985.

    Google Scholar 

  28. S. Yuen, R. Cleaveland, Z. Dayar, S. Smolka: Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes, Probabilistic Simulations for Probabilistic Processes, Proc. CONCUR 94, Theories of Concurrency: Unification and Extension, Lecture Notes in Computer Science 836, Springer-Verlag, pp 497–512, 1994.

    Google Scholar 

  29. W. Yi: Algebraic Reasoning for Real-Time Probabilistic Processes with Uncertain Information, Formal Techniques in Real Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, Springer-Verlag, pp 680–693, 1994.

    Google Scholar 

  30. 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 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Mathematik & Informatik, Universität Mannheim, 68131, Mannheim, Germany

    Christel Baier

Authors
  1. Christel Baier

    You can also search for this author inPubMed Google Scholar

Editor information

Rajeev Alur Thomas A. Henzinger

Rights and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baier, C. (1996). Polynomial time algorithms for testing probabilistic bisimulation and simulation. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_57

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp