Parametric LTL on Markov Chains

TL;DR

This paper studies the verification of finite Markov chains against parametrized LTL formulas with variable bounds, focusing on the decidability of parameter valuation sets for probabilistic satisfaction thresholds.

Contribution

It introduces several logic fragments of parametric LTL and analyzes their decidability properties for model checking in Markov chains.

Findings

Decidability results for specific pLTL fragments.

Identification of a maximal subclass with decidable parameter valuation emptiness.

Analysis of the undecidability of the full pLTL logic.

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., $\Diamond_{\le x}\ \varphi$ asserts that $\varphi$ 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} (\varphi)$ for which the probability to satisfy pLTL-formula $\varphi$ 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}(\varphi)$ is undecidable, we consider several logic fragments. We consider parametric reachability properties, a sub-logic of pLTL restricted to next and $\Diamond_{\le x}$, parametric B\"uchi properties and finally, a maximal subclass of pLTL for which emptiness of $V_{> 0}(\varphi)$ is decidable.