2026-08-11T00:06:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:8392 2024-03-06T10:41:59Z ddc:004 open_access

Complexity of Model Checking MDPs against LTL Specifications Kini, Dileep Viswanathan, Mahesh Markov Decision Processes Linear Temporal Logic model checking complexity Given a Markov Decision Process (MDP) M, an LTL formula \varphi, and a threshold \theta \in [0,1], the verification question is to determine if there is a scheduler with respect to which the executions of M satisfying \varphi have probability greater than (or greater than or equal to) \theta. When \theta = 0, we call it the qualitative verification problem, and when \theta \in (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 different fragments of LTL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dileep Kini and Mahesh Viswanathan 2018 Is Part Of LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2017.35 urn:nbn:de:0030-drops-83928 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.35 eng https://creativecommons.org/licenses/by/3.0/legalcode