Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

Abstract

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.

Details

OriginalspracheEnglisch
Titel32nd International Conference on Concurrency Theory, CONCUR 2021
Redakteure/-innenSerge Haddad, Daniele Varacca
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Seiten7:1–7:18
ISBN (Print)978-3-95977-203-7
PublikationsstatusVeröffentlicht - 1 Aug. 2021
Peer-Review-StatusJa

Publikationsreihe

Reihe32nd International Conference on Concurrency Theory (CONCUR 2021) ; Vol. 203
Band203
ISSN1868-8969

Konferenz

Titel32nd International Conference on Concurrency Theory
KurztitelCONCUR 2021
Dauer23 - 27 August 2021
Webseite
BekanntheitsgradInternationale Veranstaltung
Ortonline
StadtParis
LandFrankreich

Externe IDs

ORCID /0000-0002-5321-9343/work/142236688
Scopus 85115305824
ORCID /0000-0003-4829-0476/work/165453929

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • Markov chain, Markov decision process, Quantified linear temporal logic, vacuity, Vacuity