Skip to main content
SpringerLink
Log in

Characterising Probabilistic Processes Logically

(Extended Abstract)

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010)

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

Abstract

In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

  2. Christoff, I.: Testing equivalences and fully abstract models for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 126–140. Springer, Heidelberg (1990)

    Google Scholar 

  3. Cleaveland, R., Purushothaman Iyer, S., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science 342(2-3), 316–350 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  4. D’Argenio, P.R., Wolovick, N., Terraf, P.S., Celayes, P.: Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization. In: Proc. QEST 2009, pp. 11–20. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  5. Deng, Y., Du, W.: A Local Algorithm for Checking Probabilistic Bisimilarity. In: Proc. FCST 2009, pp. 401–407. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  6. Deng, Y., van Glabbeek, R.J.: Characterising Probabilistic Processes Logically, http://arxiv.org/abs/1007.5188 , Full version of this paper

  7. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C.: Characterising Testing Preorders for Finite Probabilistic Processes. Logical Methods in Computer Science 4(4), 4 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  8. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C.: Testing Finitary Probabilistic Processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.C., Zhang, C.: Remarks on Testing Probabilistic Processes. ENTCS 172, 359–397 (2007)

    MathSciNet  MATH  Google Scholar 

  10. Deng, Y., Palamidessi, C.: Axiomatizations for probabilistic finite-state behaviors. Theoretical Computer Science 373(1-2), 92–114 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  11. Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labelled Markov processes. In: Proc. LICS 1998, pp. 478–489. IEEE Computer Society, Los Alamitos (1998)

    Google Scholar 

  12. Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proc. IFIP TC 2 Working Conference on Programming Concepts and Methods, pp. 443–458 (1990)

    Google Scholar 

  13. Hansson, H., Jonsson, B.: A Calculus for Communicating Systems with Time and Probabilities. In: Proc. RTSS 1990, pp. 278–287. IEEE Computer Society, Los Alamitos (1990)

    Google Scholar 

  14. Hansson, H., Jonsson, B.: A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  16. Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. LICS 1997, pp. 111–122. IEEE Computer Society, Los Alamitos (1997)

    Google Scholar 

  17. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. LICS 1991, pp. 266–277. Computer Society Press (1991)

    Google Scholar 

  18. Jonsson, B., Wang, Y.: Testing preorders for probabilistic processes can be characterized by simulations. Theoretical Computer Science 282(1), 33–51 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  19. Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  21. Lowe, G.: Probabilistic and Prioritized Models of Timed CSP. Theoretical Computer Science 138, 315–352 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  22. McIver, A.K., Morgan, C.C.: An expectation-based model for probabilistic temporal logic. Technical Report PRG-TR-13-97, Oxford University Computing Laboratory (1997)

    Google Scholar 

  23. McIver, A.K., Morgan, C.C.: Results on the Quantitative Mu-Calculus. ACM Transactions on Computational Logic 8(1) (2007)

    Google Scholar 

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

    MATH  Google Scholar 

  25. Mislove, M.W., Ouaknine, J., Worrell, J.: Axioms for Probability and Non-determinism. ENTCS 96, 7–28 (2004)

    MATH  Google Scholar 

  26. Müller-Olm, M.: Derivation of Characteristic Formulae. ENTCS 18, 159–170 (1998)

    MathSciNet  Google Scholar 

  27. Parma, A., Segala, R.: Logical Characterizations of Bisimulations for Discrete Probabilistic Systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 287–301. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)

    Book  MATH  Google Scholar 

  29. Ramakrishna, Y.S., Smolka, S.A.: Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) LFCS 1997. LNCS, vol. 1234, pp. 5–24. Springer, Heidelberg (1997)

    Google Scholar 

  30. Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Technical Report MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS (1995)

    Google Scholar 

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

  32. Steffen, B., Ingólfsdóttir, A.: Characteristic Formulae for Processes with Divergence. Information and Computation 110, 149–163 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  33. Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics 5(2), 285–309 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  34. Tix, R., Keimel, K., Plotkin, G.D.: Semantic Domains for Combining Probability and Non-Determinism. ENTCS 129, 1–104 (2005)

    MathSciNet  MATH  Google Scholar 

  35. Wang, Y., Larsen, K.G.: Testing Probabilistic and Nondeterministic Processes. In: Proc. IFIP TC6/WG6.1 PSTV’92, C-8, North-Holland, pp. 47–61 (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Comp. Sci. & Eng. and MOE-Microsoft Key Lab for Intell. Comp. & Syst., Shanghai Jiao Tong University, China

    Yuxin Deng

  2. State Key Lab of Comp. Sci., Inst. of Software, Chinese Academy of Sciences, China

    Yuxin Deng

  3. NICTA, Australia

    Rob van Glabbeek

  4. University of New South Wales, Australia

    Rob van Glabbeek

Authors
  1. Yuxin Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rob van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Computersprachen 185.2, Theory and Logic Group, TU Wien, Favoritenstraße 9-11, A-1040, Vienna, Austria

    Christian G. Fermüller

  2. School of Computer Science, University of Manchester, Oxford Road, Kilburn Building, M13 9PL, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Deng, Y., van Glabbeek, R. (2010). Characterising Probabilistic Processes Logically. In: Fermüller, C.G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science, vol 6397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16242-8_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16242-8_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16241-1

  • Online ISBN: 978-3-642-16242-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation