Approximate Verification of the Symbolic Dynamics of Markov Chains

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