# Linear inequality ltl (iltl): a model checker for discrete time markov chains

By

- Full Text:
- Download PDF
- Publisher Link:
- http://dx.doi.org/10.1007/978-3-540-30482-1_21

## 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.

This research has been supported by the DARPA IXO NEST Award F33615-01-C-1907 and the DARPA/AFOSR MURI Award F49620-02-1-0325.

## BibTeX

@inproceedings{conf/icfem/KwonA04, author = "Kwon, YoungMin and Agha, Gul", editor = "Davies, Jim and Schulte, Wolfram and Barnett, Michael", title = "Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains", booktitle = "ICFEM", crossref = "conf/icfem/2004", ee = "http://dx.doi.org/10.1007/978-3-540-30482-1_21", keywords = "formal methods, sensor networks, real-time systems", pages = "194-208", year = "2004", } @proceedings{conf/icfem/2004, editor = "Davies, Jim and Schulte, Wolfram and Barnett, Michael", title = "Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings", isbn = "3-540-23841-7", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "3308", year = "2004", }