loading...
Checking LTL Properties of Recursive Markov Chains
Torino, Italy September 19-September 22
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2005.8Second International Conference on th ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Mihalis Yannakakis, Columbia University
Kousha Etessami, University of Edinburgh
We present algorithms for the qualitative and quantitative model checking of Linear Temporal Logic (LTL) properties for Recursive Markov Chains (RMCs). Recursive Markov Chains are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. For the qualitative problem ("Given a RMC A and an LTL formula \wp, do the computations of A satisfy \wp almost surely?") we present an algorithm that runs in polynomial space in A and exponential time in \wp. For several classes of RMCs, including RMCs with one exit (a special case that corresponds to well-studied probabilistic systems, e.g., multi-type branching processes and stochastic context-free grammars) the algorithm runs in polynomial time in A and exponential time in \wp. On the other hand, we also prove that the problem is EXPTIMEhard, and hence it is EXPTIME-complete. For the quantitative problem ("does the probability that a computation of A satisfies \wp exceed a given threshold p?", or approximate the probability within a desired precision) we present an algorithm that runs in polynomial space in A and exponential space in \wp. For linearly-recursive RMCs, we can compute the exact probability in time polynomial in A and exponential in \wp. These results improve by one exponential, in both the qualitative and quantitative case, the complexity that one would obtain if one first translated the LTL formula to a Buchi automaton and then applied the model checking algorithm for Buchi automata from [11]. Our results combine techniques developed in [10, 11] for analysis of RMCs, and in [6] for LTL model checking of flat Markov Chains
Citation:
Mihalis Yannakakis, Kousha Etessami, "Checking LTL Properties of Recursive Markov Chains," qest, pp.155-165, Second International Conference on the Quantitative Evaluation of Systems (QEST'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.