Please use this identifier to cite or link to this item:
Title: Approximate verification of the symbolic dynamics of markov chains
Authors: Agrawal, M.
Akshay, S.
Genest, B.
Thiagarajan, P.S. 
Keywords: Approximation
Markov Processes
Model Checking
Probabilistic Computation
Issue Date: 2012
Citation: Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S. (2012). Approximate verification of the symbolic dynamics of markov chains. Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 : 55-64. ScholarBank@NUS Repository.
Abstract: A finite state Markov chain M is often viewed as a probabilistic transition system. An alternative view - which we follow here - is to regard M as a linear transform operating on the space of probability distributions over its set of nodes. The novel idea here is to discretize the probability value space [0,1] into a finite set of intervals. A concrete probability distribution over the nodes is then symbolically represented as a tuple D of such intervals. The i-th component of the discretized distribution D will be the interval in which the probability of node i falls. The set of discretized distributions is a finite set and each trajectory, generated by repeated applications of M to an initial distribution, will induce a unique infinite string over this finite set of letters. Hence, given a set of initial distributions, the symbolic dynamics of M will consist of an infinite language L over the finite alphabet of discretized distributions. We investigate whether L meets a specification given as a linear time temporal logic formula whose atomic propositions will assert that the current probability of a node falls in an interval. Unfortunately, even for restricted Markov chains (for instance, irreducible and aperiodic chains), we do not know at present if and when L is an (omega)-regular language. To get around this we develop the notion of an epsilon-approximation, based on the transient and long term behaviors of M. 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 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 all finite state Markov chains. Further, the study of the symbolic dynamics of Markov chains initiated here is of independent interest and can lead to other applications. © 2012 IEEE.
Source Title: Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012
ISBN: 9780769547695
DOI: 10.1109/LICS.2012.17
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Aug 10, 2020


checked on Aug 10, 2020

Page view(s)

checked on Aug 4, 2020

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.