{'fraction_non_alphanumeric': 0.03541315345699832, 'fraction_numerical': 0.0037942664418212477, 'mean_word_length': 4.455172413793103, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
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 [0,1] into a finite set of intervals I = {I1, I2,..., Im}. 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 μ(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 ω-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 (i) for each infinite word in L, at least one of its ε-approximations satisfies the given specification; (ii) 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.