Title :
iLTLchecker: a probabilistic model checker for multiple DTMCs
Author :
Kwon, Youngmin ; Agha, Gul
Author_Institution :
Dept. of Comput. Sci., Illinois Univ., Urbana, IL, USA
Abstract :
iLTL is a probabilistic temporal logic that can specify properties of multiple discrete time Markov chains (DTMCs). In this paper, we describe two related tools: MarkovEstimator a tool to estimate a Markov transition matrix, and iLTLChecker, a tool to model check iLTL properties of DTMCs. These tools work together to verify iLTL properties of DTMCs.
Keywords :
Markov processes; probabilistic logic; program verification; temporal logic; DTMC; Markov transition matrix; MarkovEstimator; iLTLchecker; multiple DTMCs; multiple discrete time Markov chain; probabilistic model checker; probabilistic temporal logic; Computer science; Discrete Fourier transforms; Equations; Frequency estimation; Large-scale systems; Markov processes; Probabilistic logic; Quadratic programming; State estimation; Stochastic systems;
Conference_Titel :
Quantitative Evaluation of Systems, 2005. Second International Conference on the
Print_ISBN :
0-7695-2427-3
DOI :
10.1109/QEST.2005.14
