|
Published Articles >> Table of Contents >> Abstract
Second International Conference on the Quantitative Evaluation of Systems (QEST'05)
pp. 155-165
Checking LTL Properties of Recursive Markov Chains
Mihalis Yannakakis, Columbia University
Kousha Etessami, University of Edinburgh
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/QEST.2005.8
Send link to a friend
| Abstract |
|
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
|
 Additional Information
|
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
|
|
