License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-83928
URL:

;

### Complexity of Model Checking MDPs against LTL Specifications

 pdf-format:

### Abstract

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.

### BibTeX - Entry

@InProceedings{kini_et_al:LIPIcs:2018:8392,
author =	{Dileep Kini and Mahesh Viswanathan},
title =	{{Complexity of Model Checking MDPs against LTL Specifications}},
booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
pages =	{35:1--35:13},
series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =	{978-3-95977-055-2},
ISSN =	{1868-8969},
year =	{2018},
volume =	{93},
editor =	{Satya Lokam and R. Ramanujam},
publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address =	{Dagstuhl, Germany},
URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8392},
URN =		{urn:nbn:de:0030-drops-83928},
doi =		{10.4230/LIPIcs.FSTTCS.2017.35},
annote =	{Keywords: Markov Decision Processes, Linear Temporal Logic, model checking, complexity}
}


 Keywords: Markov Decision Processes, Linear Temporal Logic, model checking, complexity Seminar: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) Issue date: 2018 Date of publication: 12.02.2018

DROPS-Home | Fulltext Search | Imprint | Privacy