iLTL: An LTL Model Checker for Discrete Time Markov Chains
iLTL is a Linear Temporal Logic for specifying properties of Discrete Time Markov Chains (DTMCs).
It has all logical and temporal operators of LTL along with atomic propositions of
inequalities or equalities about expected rewards. Because iLTL specifies transitions of
probability mass function (pmf) it can express overall expected properties of large scale systems.
Example: A queuing system of capacity 5
In this example, we model a queing system of capacity 5 as a DTMC (which has 6 states with
q* represents the state of '*' elements in the queue) and check its properties.
model:
#
# A DTMC is a tuple of a set of states
# and a Markov transition matrix
#
Markov chain q
#
# q has 6 states q0 ... q5 with
# qi represents the state with i elements in the queue
#
has states :
{ q0, q1, q2, q3, q4, q5},
#
# Markov transition matrix
# Mij = P[ X(t+1)=qi | X(t)=qj ]
#
transits by :
[ .94, .07, .00, .00, .00, .00;
.06, .87, .07, .00, .00, .00;
.00, .06, .87, .07, .00, .00;
.00, .00, .06, .87, .07, .00;
.00, .00, .00, .06, .87, .07;
.00, .00, .00, .00, .06, .93 ]
specification:
#
# Define atomic propositions first
#
#
# properties about pmf shape
#
a : P[q=q4] + 0.7 < P[q=q5],
b : P[q=q3] + 0.1 < P[q=q4],
c : P[q=q2] + 0.1 < P[q=q3],
#
# properties about expected queue length
#
d : 1*P[q=q1] + 2*P[q=q2] + 3*P[q=q3] + 4*P[q=q4] + 5*P[q=q5] < 2.057,
e : 1*P[q=q1] + 2*P[q=q2] + 3*P[q=q3] + 4*P[q=q4] + 5*P[q=q5] > 2.056
#
# Using the atomic propositions defined above
# specify an iLTL formula
# Operators of iLTL are:
# logical operators: /\, \/, ~, ->
# temporal operators: U, R, X, [], <>
#
a -> <> b
#a -> <> c
#<> [] (d /\ e) #The steady state expected queue length is in
#the interval (2.057, 2.056)
You can easily start using iLTL by copy-and-pasting the example above
to the text input box below: