TY - CHAP
T1 - Linear inequality LTL (iLTL)
T2 - A model checker for discrete time Markov chains
AU - Kwon, Young Min
AU - Agha, Gul
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35048875810&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35048875810&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-30482-1_21
DO - 10.1007/978-3-540-30482-1_21
M3 - Chapter
AN - SCOPUS:35048875810
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 194
EP - 208
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Davies, Jim
A2 - Schulte, Wolfram
A2 - Barnett, Mike
PB - Springer
ER -