ILTLChecker: A probabilistic model checker for multiple DTMCs

Young Min Kwon, Gul A Agha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationQEST 2005 - Proceedings Second International Conference on the Quantitative Evaluation of SysTems
Pages245-246
Number of pages2
DOIs
StatePublished - Dec 1 2005
EventQEST 2005 - Second International Conference on the Quantitative Evaluation of SysTems - Torino, Italy
Duration: Sep 19 2005Sep 22 2005

Publication series

NameQEST 2005 - Proceedings Second International Conference on the Quantitative Evaluation of SysTems
Volume2005

Other

OtherQEST 2005 - Second International Conference on the Quantitative Evaluation of SysTems
CountryItaly
CityTorino
Period9/19/059/22/05

    Fingerprint

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Kwon, Y. M., & Agha, G. A. (2005). ILTLChecker: A probabilistic model checker for multiple DTMCs. In QEST 2005 - Proceedings Second International Conference on the Quantitative Evaluation of SysTems (pp. 245-246). [1595802] (QEST 2005 - Proceedings Second International Conference on the Quantitative Evaluation of SysTems; Vol. 2005). https://doi.org/10.1109/QEST.2005.14