TY - GEN
T1 - Complexity of model checking MDPs against LTL specifications
AU - Kini, Dileep
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© Dileep Kini and Mahesh Viswanathan.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - Given a Markov Decision Process (MDP) M, an LTL formula ?, and a threshold ? ? [0, 1], the verification question is to determine if there is a scheduler with respect to which the executions of M satisfying ? have probability greater than (or =) ?. When ? = 0, we call it the qualitative verification problem, and when ? ? (0, 1], we call it the quantitative verification problem. In this paper we study the precise complexity of these problems when the specification is constrained to be in di erent fragments of LTL.
AB - Given a Markov Decision Process (MDP) M, an LTL formula ?, and a threshold ? ? [0, 1], the verification question is to determine if there is a scheduler with respect to which the executions of M satisfying ? have probability greater than (or =) ?. When ? = 0, we call it the qualitative verification problem, and when ? ? (0, 1], we call it the quantitative verification problem. In this paper we study the precise complexity of these problems when the specification is constrained to be in di erent fragments of LTL.
KW - Complexity
KW - Linear Temporal Logic
KW - Markov Decision Processes
KW - Model checking
UR - http://www.scopus.com/inward/record.url?scp=85043989729&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85043989729&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSTTCS.2017.35
DO - 10.4230/LIPIcs.FSTTCS.2017.35
M3 - Conference contribution
AN - SCOPUS:85043989729
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017
A2 - Lokam, Satya
A2 - Ramanujam, R.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017
Y2 - 12 December 2017 through 14 December 2017
ER -