Approximate Verification of the Symbolic Dynamics of Markov Chains

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.
Type de document :
Article dans une revue
Journal of the ACM (JACM), Association for Computing Machinery, 2015, 62 (1), pp.34-65
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00920793
Contributeur : Blaise Genest <>
Soumis le : dimanche 18 octobre 2015 - 17:28:23
Dernière modification le : mardi 16 janvier 2018 - 15:54:22
Document(s) archivé(s) le : jeudi 27 avril 2017 - 06:36:40

Fichier

AAGT15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00920793, version 1

Citation

Manindra Agrawal, Sundararaman Akshay, Blaise Genest, P.S. Thiagarajan. Approximate Verification of the Symbolic Dynamics of Markov Chains. Journal of the ACM (JACM), Association for Computing Machinery, 2015, 62 (1), pp.34-65. 〈hal-00920793〉

Partager

Métriques

Consultations de la notice

363

Téléchargements de fichiers

114