[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Compositional Reasoning for Probabilistic Finite-State Behaviors

  • Chapter
Processes, Terms and Cycles: Steps on the Road to Infinity

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3838))

  • 529 Accesses

Abstract

We study a process algebra which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch’s simple probabilistic automata. We consider strong bisimulation and observational equivalence, and provide complete axiomatizations for a language that includes parallel composition and (guarded) recursion. The presence of the parallel composition introduces various technical difficulties and some restrictions are necessary in order to achieve complete axiomatizations.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Aceto, L., Ésik, Z., Ingólfsdóttir, A.: Equational axioms for probabilistic bisimilarity (preliminary report). Technical Report RS-02-6, BRICS (2002)

    Google Scholar 

  2. Aceto, L., Fokkink, W.J.: The quest for equational axiomatizations of parallel composition: Status and open problems. In: Proceedings of the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond. BRICS Notes Series (2005) (to appear)

    Google Scholar 

  3. Andova, S.: Probabilistic Process Algebra. PhD thesis, Eindhoven University of Technology (2002)

    Google Scholar 

  4. Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Information and Computation 121(2), 234–255 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)

    Book  Google Scholar 

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

    Chapter  Google Scholar 

  8. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communications. Information and Control 60, 109–137 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  9. Bergstra, J.A., Klop, J.W.: Verification of an alternating bit protocol by means of process algebra. In: Bibel, W., Jantke, K.P. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems 1985. LNCS, vol. 215, pp. 9–23. Springer, Heidelberg (1986)

    Google Scholar 

  10. Bergstra, J.A., Klop, J.W.: A complete inference system for regular processes with silent moves. In: Proceedings of Logic Colloquium 1986, pp. 21–81. North Holland, Amsterdam (1988)

    Google Scholar 

  11. Bravetti, M., Gorrieri, R.: Deciding and axiomatizing weak ST bisimulation for a process algebra with recursion and action refinement. ACM Transactions on Computational Logic 3(4), 465–520 (2002)

    Article  MathSciNet  Google Scholar 

  12. Christensen, S.: Decidability and Decomposition in Process Algebras. PhD thesis, University of Edinburgh (1993)

    Google Scholar 

  13. Christensen, S., Hirshfeld, Y., Moller, F.: Decidable subsets of ccs. Computer Journal 37(4), 233–242 (1994)

    Article  Google Scholar 

  14. D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: On generative parallel composition. Electronic Notes in Theoretical Computer Science 22 (1999)

    Google Scholar 

  15. Deng, Y.: Axiomatisations and types for probabilistic and mobile processes. PhD thesis, Ecole des Mines de Paris (2005)

    Google Scholar 

  16. Deng, Y., Palamidessi, C.: Axiomatizations for probabilistic finite-state behaviors. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 110–124. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Fokkink, W.J., Groote, J.F., Pang, J., Badban, B., van de Pol, J.C.: Verifying a sliding window protocol in μCRL. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 148–163. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP WG 2.2/2.3 Working Conference on Programming Concepts and Methods, pp. 453–459 (1990)

    Google Scholar 

  19. Groote, J.F., Ponse, A., Usenko, Y.S.: Linearization in parallel pCRL. Journal of Logic and Algebraic Programming 48(1-2), 39–72 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  20. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of ACM 32, 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  21. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  22. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  23. Larsen, K.G., Skou, A.: Compositional verification of probabilistic processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 456–471. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  24. Lynch, N.A., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proceedings of the 13th Annual ACM Symposium on the Principles of Distributed Computing, pp. 314–323 (1994)

    Google Scholar 

  25. Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science 25, 267–310 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  26. Milner, R.: A complete inference system for a class of regular behaviours. Journal of Computer and System Science 28, 439–466 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  27. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  28. Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation 81, 227–247 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  29. Pogosyants, A., Segala, R., Lynch, N.A.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing 13(3), 155–186 (2000)

    Article  Google Scholar 

  30. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  31. 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)

    Chapter  Google Scholar 

  32. Stark, E.W., Smolka, S.A.: A complete axiom system for finite-state probabilistic processes. In: Proof, language, and interaction: essays in honour of Robin Milner, pp. 571–595. MIT Press, Cambridge (2000)

    Google Scholar 

  33. Stoelinga, M., Vaandrager, F.: Root contention in IEEE 1394. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 53–74. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  34. Usenko, Y.S.: Linearization in μCRL. PhD thesis, Edindhoven University of Technology (2002)

    Google Scholar 

  35. van Glabbeek, R.J.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 473–484. Springer, Heidelberg (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis and Université Paris 7, France

    Yuxin Deng

  2. INRIA Futurs and LIX, École Polytechnique, France

    Catuscia Palamidessi & Jun Pang

Authors
  1. Yuxin Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Catuscia Palamidessi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jun Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Aart Middeldorp

  2. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    Vincent van Oostrom

  3. Department of Theoretical Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081 HV, Amsterdam, The Netherlands

    Femke van Raamsdonk

  4. VU Vrije Universiteit Amsterdam,  

    Roel de Vrijer

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Deng, Y., Palamidessi, C., Pang, J. (2005). 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. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_17

Download citation

  • DOI: https://doi.org/10.1007/11601548_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30911-6

  • Online ISBN: 978-3-540-32425-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation