Parametric LTL on Markov chains

DOI10.1007/978-3-662-44602-7_17MaRDI QIDQ3190162zbMATH OpenOpenAlexWikidataFDO

Authors Souymodip Chakraborty, Joost-Pieter Katoen

Publication date 15 September 2014

Published in Advanced Information Systems Engineering (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1406.6683

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

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., $Diamon{d}_{lex}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_{precp}(varphi)$ for which the probability to satisfy pLTL-formula $varphi$ in a Markov chain meets a given threshold $precp$, 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 $Diamon{d}_{lex}$, parametric B"uchi properties and finally, a maximal subclass of pLTL for which emptiness of $V_{>0}(varphi)$ is decidable.

Recommendations

• scientific article; zbMATH DE number 1405643
• Parametric temporal logic for “model measuring”
• An efficient synthesis algorithm for parametric Markov chains against linear time properties
• Theoretical Aspects of Computing - ICTAC 2004
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination

Cited in

(5)

• An efficient synthesis algorithm for parametric Markov chains against linear time properties
• Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
• Complexity of model checking MDPs against LTL specifications
• On frequency LTL in probabilistic systems
• Markov chains and unambiguous automata

This page was built for publication: Parametric LTL on Markov chains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3190162)