%0 Conference Proceedings
%T Parametric LTL on Markov Chains
%+ Rheinisch-Westfälische Technische Hochschule Aachen University (RWTH)
%A Chakraborty, Souymodip
%A Katoen, Joost-Pieter
%Z Part 2: Track B: Logic, Semantics, Specification and Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th IFIP International Conference on Theoretical Computer Science (TCS)
%C Rome, Italy
%Y Josep Diaz
%Y Ivan Lanese
%Y Davide Sangiorgi
%I Springer
%3 Theoretical Computer Science
%V LNCS-8705
%P 207-221
%8 2014-09-01
%D 2014
%R 10.1007/978-3-662-44602-7_17
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01402042/document
%2 https://inria.hal.science/hal-01402042/file/978-3-662-44602-7_17_Chapter.pdf
%L hal-01402042
%U https://inria.hal.science/hal-01402042
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-LNCS-8705
%~ IFIP-TCS
%~ IFIP-WG2-2