Skip to Main content Skip to Navigation
Conference papers

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., $\Diamond _{\leqslant x}\ \varphi$ asserts that ϕ 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 ≺ p (ϕ) for which the probability to satisfy pLTL-formula ϕ in a Markov chain meets a given threshold ≺ p, where ≺ is a comparison on reals and p a probability. As for pLTL determining the emptiness of V> 0(ϕ) is undecidable, we consider several logic fragments. We consider parametric reachability properties, a sub-logic of pLTL restricted to next and $\Diamond _{\leqslant x}$, parametric Büchi properties and finally, a maximal subclass of pLTL for which emptiness of V> 0(ϕ) is decidable.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, November 24, 2016 - 10:51:27 AM
Last modification on : Thursday, February 8, 2018 - 4:20:02 PM
Long-term archiving on: : Monday, March 20, 2017 - 8:13:22 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Souymodip Chakraborty, Joost-Pieter Katoen. Parametric LTL on Markov Chains. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.207-221, ⟨10.1007/978-3-662-44602-7_17⟩. ⟨hal-01402042⟩



Record views


Files downloads