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 μ_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 into a finite set of intervals I = {I_1, I_2,..., I_m}- A concrete probability distribution μ 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 μ(ⅰ) 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 ω-regular language, one can hope to solve our model-checking problem (whether L |= φ?) using standard techniques. However, we show that, in general, this is not the case. Consequently, we develop the notion of an ∈-approximation, based on the transient and long-term behaviors of the Markov chain M. Briefly, the symbolic trajectory ξ' is an ∈-approximation of the symbolic trajectory ξ iff (1) ξ' agrees with ξ during its transient phase; and (2) both ξ and ξ' are within an ∈-neighborhood at all times after the transient phase. Our main results are that one can effectively check whether (ⅰ) for each infinite word in L, at least one of its ∈-approximations satisfies the given specification; (ⅱ) for each infinite word in L, all its ∈-approximations satisfy the specification. These verification results are strong in that they apply to all finite state Markov chains.