Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
by
Tomáš Brázdil,
Vojtěch Forejt,
Antonín Kučera,
A full version of the paper presented at ICALP 2008. December 2008, 48 pages.
FIMU-RS-2008-05.
Available as Postscript,
PDF.
Abstract:
We show that controller synthesis and verification problems for
Markov decision processes with qualitative PECTL* objectives
are 2-EXPTIME complete. More precisely, the algorithms are
polynomial in the size of a given Markov decision process
and doubly exponential in the size of a given qualitative PECTL*
formula. Moreover, we show that if a given qualitative PECTL*
objective is achievable by some strategy, then it is also
achievable by an effectively constructible one-counter
strategy, where the associated complexity bounds are essentially
the same as above. For the fragment of qualitative PCTL objectives,
we obtain EXPTIME completeness and the algorithms are only singly
exponential in the size of the formula.