Back to Search
Start Over
Complexity of Model Checking MDPs against LTL Specifications
- Publication Year :
- 2018
- Publisher :
- Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2018.
-
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.
- Subjects :
- 060201 languages & linguistics
000 Computer science, knowledge, general works
Computer Science::Logic in Computer Science
0602 languages and literature
Computer Science
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
06 humanities and the arts
02 engineering and technology
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Accession number :
- edsair.doi...........33d2cec626414b38559d1053868faa7a
- Full Text :
- https://doi.org/10.4230/lipics.fsttcs.2017.35