Abstract : 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 \emph{symbolic} framework. Specifically, we discretize the probability value space $[0,1]$ into a finite set of intervals $\cI = \{I_1, I_2, \ldots, I_m\}$. A concrete probability distribution $\mu$ over the node set $\{1, 2, \ldots, n\}$ of $M$ is then symbolically represented as $D$, a tuple of intervals drawn from $\mathcal{I}$ where the $i^{th}$ component of $D$ will be the interval in which $\mu(i)$ falls. The set of discretized distributions $\mathcal{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 an infinite language $L$ over $\mathcal{D}$. Our main goal is to verify whether $L$ meets a specification given as a linear time temporal logic formula $\varphi$. In our logic an atomic proposition will assert that the current probability of a node falls in the interval in $I$. Assuming $L$ can be computed effectively, one can hope to solve our model checking problem ( $L\models \varphi$?) using standard techniques in case $L$ is an $\omega$-regular language. However we show that in general this is not the case. Consequently, we develop the notion of an $\epsilon$-approximation, based on the transient and long term behaviors of M. Briefly, the symbolic trajectory $\xi'$ is an $\epsilon$-approximation of the symbolic trajectory $\xi$ iff (1) $\xi'$ agrees with $\xi$ during its transient phase; and (2) both $\xi$ and $\xi'$ are within an $\epsilon$-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 $\epsilon$-approximations satisfies the given specification; (ii) for each infinite word in $L$, all its $\epsilon$-approximations satisfy the specification. These verification results are strong in that they apply to \emph{all} finite state Markov chains.
