Record Details

Approximate Verification of the Symbolic Dynamics of Markov Chains

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Approximate Verification of the Symbolic Dynamics of Markov Chains
 
Creator AGRAWAL, M
AKSHAY, S
GENEST, B
THIAGARAJAN, PS
 
Subject MODEL-CHECKING
PROBABILITY
INEQUALITY
Theory
Verification
Algorithms
Markov chains
discretization
LTL logic
approximate model checking
 
Description A finite-state Markov chain M can be regarded as a linear transform operating on the set of probability distributions over its node set. The iterative applications of M to an initial probability distribution mu(0) will generate a trajectory of probability distributions. Thus, a set of initial distributions will induce a set of trajectories. It is an interesting and useful task to analyze the dynamics of M as defined by this set of trajectories. The novel idea here is to carry out this task in a symbolic framework. Specifically, we discretize the probability value space [0, 1] into a finite set of intervals I = {I-1, I-2,..., I-m}. A concrete probability distribution mu over the node set {1, 2,..., n} of M is then symbolically represented as D, a tuple of intervals drawn from I where the ith component of D will be the interval in which mu(i) falls. The set of discretized distributions D is a finite alphabet. Hence, the trajectory, generated by repeated applications of M to an initial distribution, will induce an infinite string over this alphabet. Given a set of initial distributions, the symbolic dynamics of M will then consist of a language of infinite strings L over the alphabet D. Our main goal is to verify whether L meets a specification given as a linear-time temporal logic formula.. In our logic, an atomic proposition will assert that the current probability of a node falls in the interval I from I. If L is an omega-regular language, one can hope to solve our model-checking problem (whether L satisfies phi?) using standard techniques. However, we show that, in general, this is not the case. Consequently, we develop the notion of an is an element of -approximation, based on the transient and long-term behaviors of the Markov chain M. Briefly, the symbolic trajectory. zeta' is an is an element of-approximation of the symbolic trajectory zeta iff (1) zeta' agrees with. during its transient phase; and (2) both zeta and zeta' are within an is an element of-neighborhood at all times after the transient phase. Our main results are that one can effectively check whether (i) for each infinite word in L, at least one of its is an element of -approximations satisfies the given specification; (ii) for each infinite word in L, all its is an element of -approximations satisfy the specification. These verification results are strong in that they apply to all finite state Markov chains.
 
Publisher ASSOC COMPUTING MACHINERY
 
Date 2016-01-15T09:55:13Z
2016-01-15T09:55:13Z
2015
 
Type Article
 
Identifier JOURNAL OF THE ACM, 62(1)
0004-5411
1557-735X
http://dx.doi.org/10.1145/2629417
http://dspace.library.iitb.ac.in/jspui/handle/100/18305
 
Language en