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.
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.207-221, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_17〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01402042
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 10:51:27
Dernière modification le : jeudi 8 février 2018 - 16:20:02
Document(s) archivé(s) le : lundi 20 mars 2017 - 20:13:22

Fichier

978-3-662-44602-7_17_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Souymodip Chakraborty, Joost-Pieter Katoen. Parametric LTL on Markov Chains. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.207-221, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_17〉. 〈hal-01402042〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

10