Complexity of model checking MDPs against LTL specifications

Dileep Kini, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017
EditorsSatya Lokam, R. Ramanujam
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770552
DOIs
StatePublished - Jan 1 2018
Event37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017 - Kanpur, India
Duration: Dec 12 2017Dec 14 2017

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume93
ISSN (Print)1868-8969

Other

Other37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017
CountryIndia
CityKanpur
Period12/12/1712/14/17

Keywords

  • Complexity
  • Linear Temporal Logic
  • Markov Decision Processes
  • Model checking

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Complexity of model checking MDPs against LTL specifications'. Together they form a unique fingerprint.

Cite this