Abstract
This chapter is about the verification of Markov decision processes (MDPs) which incorporate one of the fundamental models for reasoning about probabilistic and nondeterministic phenomena in reactive systems. MDPs have their roots in the field of operations research and are nowadays used in a wide variety of areas including verification, robotics, planning, controlling, reinforcement learning, economics and semantics of randomized systems. Furthermore, MDPs served as the basis for the introduction of probabilistic automata which are related to weighted automata. We describe the use of MDPs as an operational model for randomized systems, e.g., systems that employ randomized algorithms, multi-agent systems or systems with unreliable components or surroundings. In this context we outline the theory of verifying ω-regular properties of such operational models. As an integral part of this theory we use ω-automata, i.e., finite-state automata over finite alphabets that accept languages of infinite words. Additionally, basic concepts of important reduction techniques are sketched, namely partial order reduction of MDPs and quotient system reduction of the numerical problem that arises in the verification of MDPs. Furthermore we present several undecidability and decidability results for the controller synthesis problem for partially observable MDPs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
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
H. Aljazzar, H. Hermanns, and S. Leue. Counterexamples for timed probabilistic reachability. In Proceedings of the 3rd International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS’05), volume 3829 of Lecture Notes in Computer Science, pages 177–195. Springer, Berlin, 2005.
C. Baier, N. Bertrand, and M. Grösser. On decision problems for probabilistic Büchi automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’08), volume 4962 of Lecture Notes in Computer Science, pages 287–301. Springer, Berlin, 2008.
C. Baier and F. Ciesinski. Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of SysTems (QEST’06), pages 131–132. IEEE Computer Society Press, Los Alamitos, 2006.
C. Baier, F. Ciesinski, and M. Grösser. ProbMeLa: A modeling language for communicating probabilistic systems. In Proceedings of the 2nd ACM–IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE’04), pages 57–66. IEEE Computer Society Press, Los Alamitos, 2006.
C. Baier, F. Ciesinski, M. Grösser, and J. Klein. Reduction techniques for model checking Markov decision processes. In Proceedings of the 5th International Conference on Quantitative Evaluation of SysTems (QEST’08), pages 45–54. IEEE Computer Society Press, Los Alamitos, 2008.
C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP’97), volume 1256 of Lecture Notes in Computer Science, pages 430–440. Springer, Berlin, 1997.
C. Baier, P. d’Argenio, and M. Größer. Partial order reduction for probabilistic branching time. In Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL’05), volume 153(2) of Electronic Notes in Theoretical Computer Science, pages 97–116. Springer, Berlin, 2006.
C. Baier, B. Engelen, and M. Majster-Cederbaum. Deciding bisimularity and similarity for probabilistic processes. Journal of Computer and System Sciences, 60:187–231, 2000.
C. Baier, M. Größer, and F. Ciesinski. Partial order reduction for probabilistic systems. In Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST’04), pages 230–239. IEEE Computer Society Press, Los Alamitos, 2004.
C. Baier, B. Haverkort, H. Hermanns, and J.P. Katoen. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science, 345(1):2–26, 2005.
C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, Cambridge, 2008.
C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3):125–155, 1998.
H. Bauer. Wahrscheinlichkeitstheorie und Grundzüge der Maßtheorie. de Gruyter, Berlin, 1978.
R. Bellmann. A Markovian decision process. Journal of Mathematics and Mechanics, 6(4):679–684, 1957.
A. Bianco and L. De Alfaro. Model checking of probabilistic and nondeterministic systems. In Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’95), volume 1026 of Lecture Notes in Computer Science, pages 499–513. Springer, Berlin, 1995.
M. Bozga and O. Maler. On the representation of probabilities over structured domains. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 261–273. Springer, Berlin, 1999.
J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.
S. Cattani and R. Segala. Decision algorithms for probabilistic bisimulation. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR’02), volume 2421 of Lecture Notes in Computer Science, pages 371–385. Springer, Berlin, 2002.
K. Chatterjee. Stochastic ω-regular games. PhD thesis, University of California at Berkeley, 2007
K. Chatterjee, L. de Alfaro, and T. Henzinger. The complexity of stochastic Streett and Rabin games. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP’05), volume 3580 of Lecture Notes in Computer Science, pages 878–890. Springer, Berlin, 2005.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, 1999.
C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events (extended abstract). In Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of Lecture Notes in Computer Science, pages 336–349. Springer, Berlin, 1990.
C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, 1995.
P.R. d’Argenio, B. Jeannet, H.E. Jensen, and K.G. Larsen. Reduction and refinement strategies for probabilistic analysis. In Proceedings of the Joint International Workshop on Process Algebra and Performance Modeling and Probabilistic Methods in Verification (PAPM–PROBMIV’02), volume 2399 of Lecture Notes in Computer Science, pages 57–76. Springer, Berlin, 2002.
P.R. d’Argenio, B. Jeannet, H. Jensen, and K. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Proceedings of the 1st Joint International Workshop on Process Algebra and Performance Modeling and Probabilistic Methods in Verification (PAPM–PROBMIV’01), volume 2165 of Lecture Notes in Computer Science, pages 57–76. Springer, Berlin, 2001.
P.R. d’Argenio and P. Niebert. Partial order reduction on concurrent probabilistic programs. In Proceedings of the 1st International Conference on Quantitative Evaluation of SysTems (QEST’04), pages 240–249. IEEE Computer Society Press, Los Alamitos, 2004.
L. de Alfaro. Formal verification of probabilistic systems. PhD thesis, Stanford University, 1997
L. de Alfaro. Stochastic transition systems. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR’98), volume 1466 of Lecture Notes in Computer Science, pages 423–438. Springer, Berlin, 1998.
L. de Alfaro. The verification of probabilistic systems under memoryless partial-information policies is hard. In Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification (ProbMiV’99), pages 19–32. Birmingham University, Research Report CSR-99-9, 1999.
L. de Alfaro and R. Majumdar. Quantitative solution of omega-regular games. Journal of Computer and System Sciences, 68:374–397, 2004.
M. Droste and P. Gastin. Weighted automata and weighted logics. In this Handbook. Chapter 5. Springer, Berlin, 2009.
M. Droste and D. Kuske. Skew and infinitary formal power series. Theoretical Computer Science, 366:199–227, 2006.
M. Droste and G. Rahonis. Weighted automata and weighted logics with discounting. In Proceedings of the 12th International Conference on Implementation and Applications of Automata (CIAA’07), volume 4783 of Lecture Notes in Computer Science, pages 73–84. Springer, Berlin, 2007.
M. Droste, J. Sakarovitch, and H. Vogler. Weighted automata with discounting. Information Processing Letters, 108(1):23–28, 2008.
Z. Esik and W. Kuich. Finite automata. In this Handbook. Chapter 3. Springer, Berlin, 2009.
I. Fichtner, D. Kuske, and I. Meinecke. Traces, series-parallel posets, and pictures: a weighted study. In this Handbook. Chapter 10. Springer, Berlin, 2009.
S. Giro and P.R. d’Argenio. Quantitative model checking revisited: neither decidable nor approximable. In Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’07), volume 4763 of Lecture Notes in Computer Science, pages 179–194. Springer, Berlin, 2007.
P. Godefroid. Partial Order Methods for the Verification of Concurrent Systems: an Approach to the State Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, Berlin, 1996.
P. Godefroid, D. Peled, and M. Staskauskas. Using partial-order methods in the formal validation of industrial concurrent programs. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA’96), pages 261–269. ACM, New York, 1996.
E. Grädel, W. Thomas, and T. Wilke, editors. Outcome of the 2001 Dagstuhl Seminar on Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, Berlin, 2002.
M. Größer and C. Baier. Partial order reduction for Markov decision processes: A survey. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO’05), volume 4111 of Lecture Notes in Computer Science, pages 408–427. Springer, Berlin, 2006.
M. Größer, G. Norman, C. Baier, F. Ciesinski, M. Kwiatkowska, and D. Parker. On reduction criteria for probabilistic reward models. In Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’06), volume 4337 of Lecture Notes in Computer Science, pages 309–320. Springer, Berlin, 2006.
M. Größer. Reduction methods for probabilistic model checking. PhD thesis, Technische Universität, Dresden, 2008
R. Gupta, S. Smolka, and S. Bhaskar. On randomization in sequential and distributed algorithms. ACM Computing Surveys, 26(1):7–86, 1994.
G. Hachtel, E. Macii, A. Pardo, and F. Somenzi, Probabilistic analysis of large finite state machines. In Proceedings of the 31st Design Automation Conference (DAC’94), pages 270–275. ACM, New York, 1994.
T. Han and J.-P. Katoen. Counterexamples in probabilistic model checking. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’07), volume 4424 of Lecture Notes in Computer Science, pages 60–75. Springer, Berlin, 2007.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
V. Hartonas-Garmhausen, S. Campos, and E. Clarke. Probverus: Probabilistic symbolic model checking. In Proceedings of the 5th International Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS’99), volume 1601 of Lecture Notes in Computer Science, pages 96–110. Springer, Berlin, 1999.
H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker, and M. Siegle. On the use of MTBDDs for performability analysis and verification of stochastic systems. The Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56:23–67, 2003.
H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08), volume 5123 of Lecture Notes in Computer Science, pages 162–175. Springer, Berlin, 2008.
G. Holzmann. The SPIN Model Checker, Primer and Reference Manual. Addison–Wesley, Reading, 2003.
G.J. Holzmann and D. Peled. An improvement in formal verification. In Proceedings of the 7th International Conference on Formal Description Techniques (IFIP’94), pages 197–211. Chapman & Hall, London, 1995.
F. Horn. Random games. PhD thesis, RWTH Aachen and Université Paris 7, 2008
R. Howard. Dynamic Programming and Markov Processes. MIT Press, Cambridge, 1960.
T. Huynh and L. Tian. On some equivalence relations for probabilistic processes. Fundamenta Informaticae, 17:211–234, 1992.
B. Jeannet, P.R. d’Argenio, and K.G. Larsen. RAPTURE: A tool for verifying Markov decision processes. In Proceedings of the International Conference on Concurrency Theory (CONCUR’02): Tools Day, Technical Report, Faculty of Informatics, Masaryk University Brno, 2002.
M. Jurdzinski, F. Laroussinie, and J. Sproston. Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science, 4(3-1):4–20, 2008.
J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. Three-valued abstraction for continuous-time Markov chains. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07), volume 4590 of Lecture Notes in Computer Science, pages 316–329. Springer, Berlin, 2007.
J. Kemeny and J. Snell. Denumerable Markov Chains. Van Nostrand, Princeton, 1976.
M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In Proceedings of the 12th International Conference on Modelling Tools and Techniques for Computer and Communication System Performance Evaluation (TOOLS’02), volume 2324 of Lecture Notes in Computer Science, pages 113–140. Springer, Berlin, 2002.
M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2):128–142, 2004.
M. Kwiatkowska, G. Norman, and D. Parker. Symmetry reduction for probabilistic model checking. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06), volume 4144 of Lecture Notes in Computer Science, pages 238–248. Springer, Berlin, 2008.
M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Verification of real-time probabilistic systems. In Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249–288. Wiley, New York, 2008
M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282:101–150, 2002.
K. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, 1991.
D. Lehmann and M.O. Rabin. On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In Proceedings of the 8th Annual ACM Symposium on Principles of Programming Languages (POPL’81), pages 133–138. ACM, New York, 1981.
W. Lovejoy. A survey of algorithmic methods for partially observable Markov decision processes. Annals of Operations Research, 28(1):47–65, 1991.
N. Lynch. Distributed Algorithms. Morgan Kaufmann, San Francisco, 1996.
A. Miner and D. Parker. Symbolic representations and analysis of large probabilistic systems. In Proceedings of the GI/Dagstuhl Research Seminar on Validation of Stochastic Systems, volume 2925 of Lecture Notes in Computer Science. Springer, Berlin, 2003.
G. Monahan. A survey of partially observable Markov decision processes: Theory, models, and algorithms. Management Science, 28(1):1–16, 1982.
C. Papadimitriou and J. Tsitsiklis. The complexity of Markov decision processes. Mathematics of Operations Research, 12(3):441–450, 1987.
D. Parker. Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham, 2002.
A. Paz. Introduction to Probabilistic Automata. Academic Press, San Diego, 1971.
D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference on Computer-Aided Verification (CAV’93), volume 697 of Lecture Notes in Computer Science, pages 409–423. Springer, Berlin, 1993.
D. Peled. Partial order reduction: Linear and branching time logics and process algebras. In Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, volume 29(10) of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 233–257. American Mathematical Society, Providence, 1997
D. Peled, V. Pratt, and G. Holzmann, editors. Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, volume 29(10) of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, Providence, 1997.
A. Philippou, I. Lee, and O. Sokolsky. Weak bisimulation for probabilistic systems. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00), volume 1877 of Lecture Notes in Computer Science, pages 334–349. Springer, Berlin, 2000.
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Symposium on the Foundations of Computer Science (FOCS’77), pages 46–57. IEEE Computer Society Press, Los Alamitos, 1977.
A. Pnueli and L. Zuck. Probabilistic verification by tableaux. In Proceedings of the Symposium on Logic in Computer Science (LICS’86), pages 322–331. IEEE Computer Society Press, Los Alamitos, 1986.
M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York, 1994.
M.O. Rabin. Probabilistic automata. Information and Control, 6(3):230–245, 1963.
J.J.M.M. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, volume 23 of CRM Monograph Series. American Mathematical Society, Providence, 2004.
A. Schrijver. Combinatorial Optimization: Polyhedra and Efficiency. Springer, Berlin, 2003.
E.J. Sondik. The optimal control of partially observable Markov processes. PhD thesis, Stanford University, 1971.
W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B, Chapter 4, pages 133–191. Elsevier, Amsterdam, 1990.
A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1:297–322, 1992.
A. Valmari. State of the art report: Stubborn sets. Petri-Net Newsletters, 46:6–14, 1994.
A. Valmari. Stubborn set methods for process algebras. In Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, volume 29(10) of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 213–231. American Mathematical Society, Providence, 1997.
R. van Glabbeek, S. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science (LICS’90), pages 130–141. IEEE Computer Society Press, Los Alamitos, 1990.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th Symposium on Foundations of Computer Science (FOCS’85), pages 327–338. IEEE Computer Society Press, Los Alamitos, 1985.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the Symposium on Logic in Computer Science (LICS’86), pages 332–344. IEEE Computer Society Press, Los Alamitos, 1986.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Baier, C., Größer, M., Ciesinski, F. (2009). Model Checking Linear-Time Properties of Probabilistic Systems. In: Droste, M., Kuich, W., Vogler, H. (eds) Handbook of Weighted Automata. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-01492-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-01492-5_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-01491-8
Online ISBN: 978-3-642-01492-5
eBook Packages: Computer ScienceComputer Science (R0)