Parametric LTL on Markov Chains

Abstract

This paper is concerned with the verification of finite Markov chains against parametrized LTL (pLTL) formulas. In pLTL, the until-modality is equipped with a bound that contains variables; e.g., ${◊}_{\le x}\phi$ asserts that $\phi$ holds within $x$ time steps, where $x$ is a variable on natural numbers. The central problem studied in this paper is to determine the set of parameter valuations $V_{\prec p}(\phi )$ for which the probability to satisfy pLTL-formula $\phi$ in a Markov chain meets a given threshold $\prec p$, where $\prec$ is a comparison on reals and $p$ a probability. As for pLTL determining the emptiness of $V_{>0}(\phi )$ is undecidable, we consider several logic fragments. We consider parametric reachability properties, a sub-logic of pLTL restricted to next and ${◊}_{\le x}$, parametric Büchi properties and finally, a maximal subclass of pLTL for which emptiness of $V_{>0}(\phi )$ is decidable.

TCS Track B 2014