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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
Baier, C., D’Argenio, P., Größer, M.: Partial order reduction for probabilistic branching time. In: Proc. QAPL (2005)
Baier, C., Engelen, B., Majster-Cederbaum, M.: Deciding bisimularity and similarity for probabilistic processes. Jounal of Computer and System Sciences 60, 187–231 (2000)
Baier, C., Größer, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: QEST 2004 [37], pp. 230–239 (2004)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P., Siegle, M.: Validation of Stochastic Systems. LNCS, vol. 2925. Springer, Heidelberg (2004)
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)
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)
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)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
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)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
d’ Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: [17], pp. 57–76 (2001)
D’Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: QEST 2004 [37], pp. 240–249 (2004)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Department of Computer Science (1997)
de Alfaro, L.: Stochastic transition systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 423–438. Springer, Heidelberg (1998)
de Alfaro, L., Gilmore, S. (eds.): PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399. Springer, Heidelberg (2001)
Fecher, H., Leuker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925. Springer, Heidelberg (2006)
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)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
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)
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)
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)
Hermanns, H., Segala, R. (eds.): PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399. Springer, Heidelberg (2002)
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)
Huth, M.: Possibilistic and probabilistic abstraction-based model checking. In: [24], pp. 115–134 (2002)
Huth, M.: Abstraction and probabilities for hybrid logics. In: Proc. 2nd workshop on Quantitative Aspects of Programming Languages (2004)
Jonsson, B., Larsen, K.: Specification and refinement of probabilistic processes. In: Proc. LICS, pp. 266–277. IEEE CS Press, Los Alamitos (1991)
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)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)
Miner, A., Parker, D.: Symbolic representations and analysis of large probabilistic systems.In: [6] (2003)
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)
Peled, D.: Partial order reduction: Linear and branching time logics and process algebras. In: [34], pp. 79–88 (1996)
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)
Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation 103(1), 1–29 (1993)
Puterman, M.L.: Markov Decision Processes—Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc., New York (1994)
Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST 2004), Enschede, The Netherlands. IEEE Computer Society Press, Los Alamitos (2004)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1, 297–322 (1992)
Valmari, A.: State of the art report: Stubborn sets. Petri-Net Newsletters 46, 6–14 (1994)
Valmari, A.: Stubborn set methods for process algebras. In: [34], pp. 79–88 (1996)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)