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

Jakob PiribauerJakob Piribauer, Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Ocan SankurOcan Sankur

DOI Link

Jakob Piribauer, Christel Baier, Nathalie Bertrand, Ocan Sankur
Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking
In Haddad, Serge and Varacca, Daniele, eds., 32nd International Conference on Concurrency Theory (CONCUR 2021), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), 7:1--7:18, 2021. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{PBBS2021,
  author    = {Jakob Piribauer and Christel Baier and Nathalie Bertrand and Ocan
               Sankur},
  title     = {Quantified Linear Temporal Logic over Probabilistic Systems with
               an Application to Vacuity Checking},
  editor    = {Haddad and Serge and Varacca and Daniele},
  booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)},
  series    = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume    = {203},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2021},
  pages     = {7:1--7:18},
  doi       = {10.4230/LIPIcs.CONCUR.2021.7}
}