Report

Symbolic dynamics of Markov chains P S Thiagarajan School of Computing National University of Singapore Joint work with: Manindra Agrawal, S Akshay, Blaise Genest Acknowledgements • Samarjit and Javier • IAS • TÜV SÜD Foundation Agenda • Study complex dynamical systems – verification of temporal logic specification • High dimensional • Continuous time; continuous value domains. – Differential equations – Hybrid automata • Networks of such dynamical systems Strategy • Approximate the dynamics. – Discretize the time and value domains • Today’s first talk will have this flavor. – Sample the dynamics and do a statistical analysis. • Today’s second talk • To handle large networks: Deterministic synchronizations • Tomorrow’s talk Probabilistic dynamics • Illustrate these ideas in the setting of probabilistic dynamical systems. – Yield useful approximations in the presence intractability and lack of knowledge. – Scalability can be achieved through sampling (simulations) based statistical analysis techniques. • Statistical model checking • Key application: (Networks) of biochemical networks. Study I: Symbolic dynamics of Markov chains • • • • Well-known probabilistic dynamical systems. Rich theory Widely applied. Our focus (finite state, discrete time): – Symbolic dynamics • Discretize the probability value space [0, 1]. Symbolic dynamics of Markov chains • Analyze the symbolic dynamics via: – classical (linear) temporal logic specifications. • Probabilities are sneaked in through the atomic propositions. – Model checking methods • Details in: – LICS’2012 – Journal paper under review. Two views of Markov chains • View I – a finite state probabilistic transition system. • View II – a linear transform of probability distributions over the states. The transition system view 1 3 1 2 1 1 2/5 3/5 4 The transition system view 0 1 1 3 1 2 3/5 1 1 0 2/5 4 0 The transition system view 3 1 3 1 1 1 2 1 4 3/5 2/5 1 2/5 4 2/5 3/5 1 2 3 3 4 4 2/5 3/5 The transition system view • Outcomes: Infinite paths • Basic cylinder: The set of infinite paths that have a common finite prefix. • Path space: -algebra generated by the basic cylinders. • Probabilities are assigned to basic cylinders in a natural way. • Extends canonically to a probability measure over the path space. The transition system view 3 1 3 1 1 1 2 4 3/5 2/5 1 2/5 1 4 1 Pr(B) = 1 2/5 1 1 = 2/5 2 1 1 B – The set of all paths that have the prefix 3 4 1 3 4 3/5 3 3 1 1 4 B 4 Measurable properties • The state 3 will be visited infinitely often. PCTL, CTL, …. Baier, C. and Katoen, J.-P. Principles of Model Checking VIEW II • The Markov chain transforms (linearly) a given distribution over its nodes to a new one. • The graph of the chain is represented as a stochastic matrix – (all row sums are 1) • The Perron-Frobinius theory (for non-negative matrices) applies. VIEW II • Leads to natural sub-classes: – Irreducible and aperiodic, – periodic, … • transient states, recurrent states…. • Stationary distributions…. VIEW II 1 3 1 2 1 1 2/5 3/5 4 The second view 0 1 3 1 2 1 1 1 0 2/5 3/5 4 0 Trajectory of distributions • Markov chain as (linear)transformer of probability distributions 3 1 1 1 2 0 3/5 1 1 0 2/5 4 0 Transition matrix M Trajectory of distributions 0 0 3 1 1 1 1 2 3/5 1 2/5 0 4 Transition matrix M • Each initial distribution generates a trajectory of distributions: Trajectory of distributions 0 0 3 1 1 1 1 2 3/5 1 2/5 0 4 Transition matrix M • Each initial distribution generates a trajectory of distributions: Trajectory of distributions • Dynamics: – The set of trajectories generated from an initial set of distributions – This set can be infinite • We can ask whether all (none) of the trajectories satisfy some desired dynamical property • What we can ask in this setting is incomparable with View I specifiable properties Trajectory of distributions • Eventually the probability of being in 1 is always greater than being in 3. • There is a future time at which 90% of the probability mass lies on {1, 4}. Symbolic dynamics • A trajectory: – an infinite sequence of probability distributions (over a finite set of nodes). – The alphabet of probability distributions -over a finite set of nodes- is (uncountably) infinite. • Hence a trajectory is an infinite sequence over an infinite alphabet, • But exactly tracking probability distributions may be neither necessary nor possible. – Bio-chemical networks – Sensor networks… Symbolic dynamics • We propose to reason about sequences of distributions in a symbolic way. – Using a finite alphabet of discretized distributions. Symbolic dynamics • A classical tradition dynamical systems theory. – Jacques Hadamard(1898), Morse and Hedlund (1921), …. – Shannon, Smale… – Significant applications in data storage and transmission (via coding theory), linear algebra. Symbolic dynamics • We know how to do this for: – Timed automata – In some restricted settings for hybrid automata. • For finite state Markov chains this has been done under very restricted setting and unnatural restrictions (Chada et.al 2011, Korthikanti et.all 2010.) • We shall instead give up on bisimulation-based equivalence classes: • Instead, fix a discretization of [0, 1] – With no restrictions handle all finite state Markov chains . Symbolic dynamics c d F2(x) F(x) F3(x) e a b x Finite alphabet! Symbolic dynamics • Each block is a letter. • Each trajectory is now recorded as a sequence of letters taken from a finite alphabet. • If each block bisimualtion equivalence class it is called a Markov partition! • Study the system dynamics in terms of these sequences. – Sophic shift sequences – Shift sequences of finite type. Symbolic dynamics • We know how to get “Markov partitions”) do this for: – Timed automata – For hybrid automata, in a few settings. • For finite state Markov chains this has been done under very restricted setting and unnatural restrictions (Chada et.al 2011, Korthikanti et.all 2010.) • We do not look for bisimulations of finite index.: • Instead, we fix a discretization of [0, 1] – Handle all finite state Markov chains ; no restrictions. Symbolic dynamics of Markov chains • Discretization – We partition [0,1] into a finite set of intervals, a b c Symbolic dynamics of Markov chains a b c • Each (probability) value is mapped to (identified with) the interval it falls in. Symbolic dynamics of Markov chains Symbolic dynamics of Markov chains • Each distribution maps to D, a unique n-tuple of intervals. • ∈D means Γ() = D = D Symbolic dynamics of Markov chains • Each distribution maps to D, a unique n-tuple of intervals. • Several distributions can map to the same D, • in fact Γ-1(D) can be infinite = D Symbolic dynamics of Markov chains • Discretization – We partition [0,1] into a finite set of intervals, • Γ-1(D) can be empty ? = D Symbolic dynamics of Markov chains • Discretized distribution – A tuple of intervals D is discretized distribution ( - distribution for short ) if Γ-1(D) ≠ ø ø = D = D × Symbolic dynamics of Markov chains • The set of discretized distributions is finite Symbolic dynamics of Markov chains • A Trajectory of M starting from a distribution : • Induces a symbolic trajectory – a word over ω • ξ = (Γ() Γ(1) Γ(2) ….) Symbolic dynamics of Markov chains 3 0.45 1 2 0.12 1 1 1 0.35 2/5 3/5 4 0.08 . . Symbolic dynamics of Markov chains • Fix a set of initial distributions IN. • We use a -distribution Din to specify IN. That is IN = Din This can be an infinite set . – IN = = , ……….. • We can fix the set of initial distributions in many other ways. Symbolic dynamics of Markov chains • The symbolic dynamics of (M , Din ) is: • We wish to reason about this -language. Symbolic dynamics of Markov chains • The discretization need not be uniform • Can be different for each dimension (node). • {[0, 1]} can be used to mask out “don’t care” nodes. – Dimension-reduction. A temporal logic to reason about the symbolic dynamics • I, a discretization of [0, 1] : – < i , d > is an atomic proposition – node i interval d – “In the current distribution , (i) falls in the interval d ”. – In the current discretized distribution D, D(i) = d • Probabilistic linear-time temporal logic LTL I The verification problem • Given, – – – – a Markov chain M, a discretization I, an initial set of distributions represented as Din , and a specification φ as an LTL I formula, • Determine if M, Din ⊨ φ. In other words, – (0) ⊨ for every in LM – Does every symbolic trajectory of M satisfy φ, i.e., – is it the case LM ⊆ L φ? Example formulas • Whenever probability of node i is “high”, the probability of node j is “low” : • The -distribution (d1, d2, . . . , dn) appears infinitely often: Example formulas • Extending with FO theory of reals, we can express much more: – e.g., Infinitely often, the probability of node i is at least twice the sum of probabilities of all other nodes. • Logics based on path spaces (PCTL etc.) and logics based sequences of probability distributions are incomparable Examples • We have modeled a simple version of the Google pageranking algorithms. • We have also modeled a small pharmacokinetics system for drug delivery. The verification problem • Given, M, I, Din , φ, determine if M, Din ⊨ φ , i.e., LM ⊆ L φ – If LM is ω-regular and effectively computable then we can use standard model checking techniques. – But LM is not always ω-regular ! The verification problem LM is not always ω-regular. -approximations • Fix a small > 0 (fraction of length of an interval of I ) . . ’ -approximations • Fix a small >0 (fraction of length of an interval of I ) . D . . ’ -approximations • Fix a small >0(fraction of length of an interval of I ) . D . . ’ • The -nbhd of a concrete distribution is the set of all distributions which are atmost -away from it. -approximations • The -nbhd of a concrete distribution is the set of all distributions which are atmost -away from it. – Nbr() • is an -neighborhood iff there exists such that Nbr() = -approximations Suppose D, D’ belong to a final class. Then there exist in D and ’ in D’ such that (, ’) 2 • Suppose D, D’ belong to a final class. Then for every in D and ’ in D’ , (, ’) 2 + where depends only on the discretization. • D DD 2 ’ D’ DD A basic property of the symbolic dynamics • There exists a computable constant K and a computable ordered collection of -nbhds { 0, 1, . . . , } called final classes such that: – After K steps, ξ will forever cycle through the ordered final classes. In other words, ξ (k) ∈ k mod for k > K A basic property of the symbolic dynamics • There exists a computable constant K and an ordered collection of -nbhds { 0, 1, . . . , } called final classes such that: – After K steps, ξ will forever cycle through the ordered final classes. In other words, ξ (k) ∈ k mod for k > K M 1 M 2 K steps 0 . 1 M -1 M M 2 A basic property of the symbolic dynamics • There exists a computable constant K and an ordered collection of -nbhds { 0, 1, . . . , } called final classes such that: – After K steps, ξ will forever cycle through the ordered final classes. In other words, ξ (k) ∈ k mod for k > K M 1 M 2 K steps 0 . M 1 M -1 M M 2 -approximations of trajectories • A symbolic trajectory ξ’ is an - approximation of ξ (the symbolic trajectory gen. by ) iff: – ξ (k)= ξ’ (k) for all 0≤ k ≤ K , – For all k> K , ξ’ (k) and ξ (k) belong to the same final class. Two approximate verification problems • Determine if – M, Din ⊨ φ , i.e., for every ∈ Din , there exists an -approximation of ξ in L φ. – M, Din ⊨ φ , i.e., for every ∈ Din , every -approximation of ξ is in L φ. Two approximate verification problems • Proposition – M, Din ⊨ φ implies LM ⊆ L φ – M, Din ⊭ φ implies LM ⊈ L φ Two approximate verification problems • If M, Din ⊨ φ and M, Din ⊭ φ then M - approximately meets φ. • If we want to do better we can set ’ = /2 and iterate (incremental overhead). The main result • Theorem: Checking M, Din ⊨ φ and M, Din ⊨ φ are both effectively solvable problems. The main result • The proof first assumes a single initial distributions and proceeds to establish the theorem for: – Irreducible aperiodic chains – Irreducible periodic chains. – General chains • This is then extended to a set of initial distributions Din. • The main step is the transient + steady state characterization of the symbolic dynamics. The main result The main result Additional results • Convex hull of a finite set of distributions can also be handled. • The atomic propositions can be constraints expressed in the first order theory of reals. • Restrictions on the eigenvalues can yield -regular behaviors (egs.: distinct and real) Summary • Discretizing the values space [0, 1] leads to an interesting and useful symbolic dynamics of finite state Markov chains. • Extensions: – – – – Optimizations Implementations Case studies Interval Markov chains