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

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'ILTLChecker: A probabilistic model checker for multiple DTMCs'. Together they form a unique fingerprint.

Cite this