Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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

Résumé

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. 2012 ACM Subject Classification Theory of computation → Verification by model checking Keywords and phrases Quantified linear temporal logic, Markov chain, Markov decision process, vacuity.
Fichier principal
Vignette du fichier
LIPIcs-CONCUR-2021-7.pdf (791.44 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03408379 , version 1 (29-10-2021)

Licence

Paternité

Identifiants

Citer

Jakob Piribauer, Christel Baier, Nathalie Bertrand, Ocan Sankur. Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking. CONCUR 2021 - 32nd International Conference on Concurrency Theory, Aug 2021, Paris, France. pp.1-18, ⟨10.4230/LIPIcs.CONCUR.2021.7⟩. ⟨hal-03408379⟩
45 Consultations
47 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More