Linear inequality LTL (iLTL): A model checker for discrete time Markov chains

Young Min Kwon, Gul Agha

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

We develop a way of analyzing the behavior of systems modeled using Discrete Time Markov Chains (DTMC). Specifically, we define iLTL, an LTL with linear inequalities on the pmf vectors as atomic propositions. iLTL allows us to express not only properties such as the expected number of jobs or the expected energy consumption of a protocol during a time interval, but also inequalities over such values. We present an algorithm for model checking properties of DTMCs expressed in iLTL. Our model checker differs from existing probabilistic ones in that the latter do not check properties of the transitions on the probability mass function (pmf) itself. Thus, iLTLChecker can check, given an interval estimate of current pmf, whether future pmfs will always satisfy a specification. We believe such properties often arise in distributed systems and networks and may, in particular, be useful in specifying requirements for routing or load balancing protocols. Our algorithm has been implemented in a tool called iLTLChecker and we illustrate the use of the tool by means of some examples.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsJim Davies, Wolfram Schulte, Mike Barnett
PublisherSpringer
Pages194-208
Number of pages15
ISBN (Electronic)3540238417, 9783540238416
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3308
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Linear inequality LTL (iLTL): A model checker for discrete time Markov chains'. Together they form a unique fingerprint.

Cite this