Parametric LTL on Markov Chains

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., ${\mathrm{◊}}_{\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$isacomparisononrealsand$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 ${\mathrm{◊}}_{\le x}$, parametric B"uchi properties and finally, a maximal subclass of pLTL for which emptiness of $V_{> 0}(\varphi)$ is decidable.