Skip to main content
SpringerLink
Log in

Partial Order Reduction for Markov Decision Processes: A Survey

  • Conference paper
Formal Methods for Components and Objects (FMCO 2005)

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

Included in the following conference series:

Abstract

In the past, several model checking algorithms have been proposed to verify probabilistic reactive systems. In contrast to the non-probabilistic setting where various techniques have been suggested and successfully applied to combat the state space-explosion problem in the context of model checking the techniques used for probabilistic systems have mainly concentrated on symbolic methods with variants of decision diagrams or abstraction methods. Only recently results have been published that give criteria on applying partial order reduction for verifying quantitative linear time properties as well as branching time properties for probabilistic systems. This paper summarizes the results that have been established so far about partial order reduction for Markov decision processes. We present the different reduction conditions and provide a comparison of the corresponding results.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Baier, C., Ciesinski, F., Groesser, M.: Quantitative analysis of distributed randomized protocols. In: Proc. of the tenth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2005) (2005)

    Google Scholar 

  2. Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (1997)

    Google Scholar 

  3. Baier, C., D’Argenio, P., Größer, M.: Partial order reduction for probabilistic branching time. In: Proc. QAPL (2005)

    Google Scholar 

  4. Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimularity and similarity for probabilistic processes. Jounal of Computer and System Sciences 60, 187–231 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Baier, C., Größer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: QEST 2004 [37], pp. 230–239 (2004)

    Google Scholar 

  6. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P., Siegle, M.: Validation of Stochastic Systems. LNCS, vol. 2925. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  7. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)

    Google Scholar 

  8. Bozga, M., Maler, O.: On the Representation of Probabilities over Structured Domains. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 261–273. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  10. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  11. Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events (extended abstract). In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 336–349. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  12. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  13. d’ Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: [17], pp. 57–76 (2001)

    Google Scholar 

  14. D’Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: QEST 2004 [37], pp. 240–249 (2004)

    Google Scholar 

  15. de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science (1997)

    Google Scholar 

  16. de Alfaro, L.: Stochastic transition systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 423–438. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. de Alfaro, L., Gilmore, S. (eds.): PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399. Springer, Heidelberg (2001)

    Google Scholar 

  18. Fecher, H., Leuker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model checking. In: Proc. 3rd Israel Symposium on the Theory of Computing Systems (ISTCS 1995), pp. 130–139. IEEE Press, Los Alamitos (1995)

    Chapter  Google Scholar 

  20. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)

    Google Scholar 

  21. Godefroid, P., Peled, D., Staskauskas, M.: Using partial-order methods in the formal validation of industrial concurrent programs. In: Proc. International Symposium on Software Testing and Analysis, pp. 261–269. ACM Press, New York (1996)

    Google Scholar 

  22. Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Probabilistic Analysis of Large Finite State Machines. In: 31st ACM/IEEE Design Automation Conference (DAC). San Diego Convention Center (1994)

    Google Scholar 

  23. Hermanns, H., Kwiatkowska, M., Norman, G., Parker, D., Siegle, M.: On the use of MTBDDs for performability analysis and verification of stochastic systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems 56, 23–67 (2003)

    MATH  MathSciNet  Google Scholar 

  24. Hermanns, H., Segala, R. (eds.): PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  25. Holzmann, G., Peled, D.: An improvement in formal verification. In: Proc. Formal Description Techniques, FORTE 1994, Berne, Switzerland, pp. 197–211. Chapman & Hall, Boca Raton (1994)

    Google Scholar 

  26. Huth, M.: Possibilistic and probabilistic abstraction-based model checking. In: [24], pp. 115–134 (2002)

    Google Scholar 

  27. Huth, M.: Abstraction and probabilities for hybrid logics. In: Proc. 2nd workshop on Quantitative Aspects of Programming Languages (2004)

    Google Scholar 

  28. Jonsson, B., Larsen, K.: Specification and refinement of probabilistic processes. In: Proc. LICS, pp. 266–277. IEEE CS Press, Los Alamitos (1991)

    Google Scholar 

  29. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT) (2004)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  31. Miner, A., Parker, D.: Symbolic representations and analysis of large probabilistic systems.In: [6] (2003)

    Google Scholar 

  32. Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)

    Google Scholar 

  33. Peled, D.: Partial order reduction: Linear and branching time logics and process algebras. In: [34], pp. 79–88 (1996)

    Google Scholar 

  34. Peled, D., Pratt, V., Holzmann, G. (eds.): Partial Order Methods in Verification. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29(10). American Mathematical Society (1997)

    Google Scholar 

  35. Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation 103(1), 1–29 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  36. Puterman, M.L.: Markov Decision Processes—Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)

    MATH  Google Scholar 

  37. Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST 2004), Enschede, The Netherlands. IEEE Computer Society Press, Los Alamitos (2004)

    Google Scholar 

  38. Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)

    Google Scholar 

  39. Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1, 297–322 (1992)

    Article  MATH  Google Scholar 

  40. Valmari, A.: State of the art report: Stubborn sets. Petri-Net Newsletters 46, 6–14 (1994)

    Google Scholar 

  41. Valmari, A.: Stubborn set methods for process algebras. In: [34], pp. 79–88 (1996)

    Google Scholar 

  42. van Glabbeek, R., Smolka, S., Steffen, B., Tofts, C.: Reactive, generative, and stratified models of probabilistic processes. In: Proc. 5th Annual Symposium on Logic in Computer Science (LICS), pp. 130–141. IEEE Computer Society Press, Los Alamitos (1990)

    Chapter  Google Scholar 

  43. Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 327–338 (1985)

    Google Scholar 

  44. Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proc. 1st Annual Symposium on Logic in Computer Science (LICS), pp. 332–344. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik I, Römerstrasse 164, 53117, Bonn

    Marcus Groesser & Christel Baier

Authors
  1. Marcus Groesser
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christel Baier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI, Kruislaan 413, 1098, Amsterdam, SJ, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300, Leiden, RA, The Netherlands

    Marcello M. Bonsangue

  3. Centre Equitation, VERIMAG, 2 Avenue de Vignate, 38610, Grenoble-Gières, France

    Susanne Graf

  4. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel,Hermann-Rodewald-Straße 3, 24118, Kiel, Germany

    Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groesser, M., Baier, C. (2006). Partial Order Reduction for Markov Decision Processes: A Survey. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2005. Lecture Notes in Computer Science, vol 4111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11804192_19

Download citation

  • DOI: https://doi.org/10.1007/11804192_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36749-9

  • Online ISBN: 978-3-540-36750-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation