2026-07-22T06:50:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14384 2024-03-06T10:54:16Z ddc:004 open_access

Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking Piribauer, Jakob Baier, Christel Bertrand, Nathalie Sankur, Ocan Quantified linear temporal logic Markov chain Markov decision process vacuity Quantified linear temporal logic (QLTL) is an ω-regular extension of LTL allowing quantification over propositional variables. We study the model checking problem of QLTL-formulas over Markov chains and Markov decision processes (MDPs) with respect to the number of quantifier alternations of formulas in prenex normal form. For formulas with k{-}1 quantifier alternations, we prove that all qualitative and quantitative model checking problems are k-EXPSPACE-complete over Markov chains and k{+}1-EXPTIME-complete over MDPs. As an application of these results, we generalize vacuity checking for LTL specifications from the non-probabilistic to the probabilistic setting. We show how to check whether an LTL-formula is affected by a subformula, and also study inherent vacuity for probabilistic systems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jakob Piribauer and Christel Baier and Nathalie Bertrand and Ocan Sankur 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.7 urn:nbn:de:0030-drops-143842 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.7 eng https://creativecommons.org/licenses/by/4.0/legalcode