IA169 System Verification and Assurance Verification of Systems with Probabilities Vojtěch Řehák Motivation example Fail-repair system What are the properties of the model? • G(working =^> F done) NO • G(working =^> F error) NO • FG(working V error V repair) NO IA169 System Verification and Assurance — 12 2/31 The example with probability Fail-repair system • What is the probability of reaching "done" from "working" with no visit ot error r • What is the probability of reaching "done" from "working" with at most one visit of "error"? • What is the probability of reaching "done" from "working"? IA169 System Verification and Assurance — 12 3/31 Discrete-time Markov Chains (DTMC) IA169 System Verification and Assurance — 12 4/31 Discrete-time Markov Chains (DTMC) • Standard model for probabilistic systems. • State based model with probabilities on branching. • Based on the current state, the succeeding state is given by a discrete probability distribution. • Markov property ("memorylessness") — only the current state determines the successors (the past states are irrelevant). • Probabilities on outgoing edges sums to 1 for each state. • Hence, each state has at least one outgoing edge ("no deadlock"). IA169 System Verification and Assurance — 12 5/31 DTMC examples Model of a queue 2/3 1/3 Queue for at most 4 items. In every time tick, a new item comes with probability 1/3 and an item is consumed with probability 2/3. What if a new items comes with probability p = 1/2 and an item is consumed with probability q = 2/3? IA169 System Verification and Assurance — 12 6/31 DTMC examples Model of the new queue l-p (1-pXl-g) (l-pXl-g) (l-pXl-g) l_g /-\ /-n r-\ /-\ t-\ P(l - q) P(l - q) P(l - q) IA169 System Verification and Assurance — 12 7/31 DTMC - formal definition Deterministic Time Markov Chain is given by • a set of states S, o an initial state So of S, o a probability matrix P : S x S —>► [0,1], and • an interpretation of atomic propositions / : S —>► >4P. IA169 System Verification and Assurance — 12 8/31 Back to our questions Fail-Repair System • What is the probability of reaching "done" from "working" with no visit of "error"? • What is the probability of reaching "done" from "working" with at most one visit of "error"? • What is the probability of reaching "done" from "working"? IA169 System Verification and Assurance — 12 9/31 Markov chain analysis Transient analysis a distribution after /c-steps • reaching/hitting probability • hitting time Long run analysis • probability of infinite hitting • stationary (invariant) distribution 9 mean inter visit time • long run limit distribution IA169 System Verification and Assurance — 12 10/31 Property Specification IA169 System Verification and Assurance — 12 11/31 Property specification languages Recall some non-probabilistic specification languages: LTL formulae (f ::= p I -i<£? \ cpV cp \ X cp \ cp U cp CTL formulae (f ::= p I -i<£? I V I EX | E[(p U if] \ EG cp Syntax of CTL state formula path formula = P := (p i(p\(p\/(p\Ei{j t0 ip\/ip X ip ip U ip IA169 System Verification and Assurance — 12 12/31 Property specification languages We need to quantify probability that a certain behaviour will occur. Probabilistic Computation Tree Logic (PCTL) Syntax of PCTL where • b G [0,1] is a probability bound, • DXG {<, <, >, >}, and • k G N is a bound on the number of steps. A PCTL formula is always a state formula. a U-k P is a bounded until saying that a holds until f3 within k steps. For k = 3 it is equivalent to j3 V (a A X j3) V (a A X (/3 V a A X Some tools also supports P=?^ asking for the probability that the specified behaviour will occur. state formula ifj \\= X cp \ cp U cp \ cp U~k (p path formula IA169 System Verification and Assurance — 12 13/31 PCTL examples We can also use derived operators like G, F, A, etc. Probabilistic reachability P>i(Fdone) • probability of reaching the state done is equal to 1 Probabilistic bounded reachability P>o.99( F-6 done) • probability of reaching the state done in at most 6 steps is > 0.99 Probabilistic until Po(X(^) is equivalent to EX cp • there is a next state satisfying ip • P>i(X(p) is equivalent to AXcp 9 the next states satisfy p • P>o( F cp) is equivalent to EF cp • there exists a finite path to a state satisfying ip but • P>i(Fcp)\s not equivalent to AFcp There is no CTL formula equivalent to P>i(F(p), and no PCTL formula equivalent to AF cp. IA169 System Verification and Assurance — 12 15/31 How the transient probabilities are computed? p= 0 0 0 0 0 1 0 0 1 0 0 0.05 0 0 0 0 0 1 0 0 0 0.95 0 0 1 Probability in the k-th state when starting in 1 1000 0]xP=[0 1000 1 0 0 0 0] x P2 = [0 0 0.05 0 0.95 1 0 0 0 0] x P3 = [0 0 0 0.05 0.95 1 0 0 0 0] x P4 = [0 0.05 0 0 0.95 1 0 0 0 Ol x P5 = [0 0 0.0025 0 0.9975 IA169 System Verification and Assurance — 12 16/31 How the transient probabilities are computed? p= 0 0 0 0 0 1 0 0 1 0 0 0.05 0 0 0 Probability of being in 5 or 2 in the k-th state P x \0 1 0 0 1 P2 x [0 1 0 0 1 P3 x 0 1 0 0 1 P4 x 0 1 0 0 1 i T i T 1 0.95 Oil 0.95 0.95 1 0.95 1 0 0 1 0 0 1 T 0.95 1 0.95 0.95 1 i T i T p5 X 0 10 0 1 0 0.95 0 0 1 1 0.9975 0.95 1 1 0.9975 0.9975 1 0.9975 1 IA169 System Verification and Assurance — 12 17/31 Unbounded reachability Let p(s, A) be the probability of reaching a state in A from s. It holds that: • p(s,A) = 1 for s e A • p(s, 4) = Es'es,cc(s) * A) for s 0 ^ where succ(s) is a set of successors of s and P(s,s/) is the probability on the edge from s to sf. Theorem • The minimal non-negative solution of the above equations equals to the probability of unbounded reachability. IA169 System Verification and Assurance — 12 Long Run Analysis IA169 System Verification and Assurance — 12 19/31 Long run analysis What are the states visited infinitely often with probability 1? IA169 System Verification and Assurance — 12 20/31 Definitions • A state of DMTC is called transient iff there is a positive probability that the system will not return back to this state. • A state s of DMTC is called recurrent iff, starting from s, the system eventually returns back to the s with probability 1. Theorem • Every transient state is visited finitely many times with probability 1. • Each recurrent state is with probability 1 either not visited or visited infinitely many times.1 1This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance — 12 Which states are transient? Which states are recurrent? sec ...........................0,5............................. Decompose the graph representation onto strongly connected components. BSCC BSCC Theorem 1 9 A state is recurrent if and only if it is in a bottom strongly connected component. All other states are transient. 1This holds only in DTMC models with finitely many states. IA169 System Verification and Assurance — 12 Irreducible Markov Chain For the sake of infinite behaviour, we will concentrate on bottom strongly connected components only. Definition • A Markov chain is said to be irreducible if every state can be reached from every other state in a finite number of steps. Theorem • A Markov chain is irreducible if and only if its graph representation is a single strongly connected component. Corollary • All states of a finite irreducible Markov chain are recurrent. IA169 System Verification and Assurance — 12 23/31 Stationary (Invariant) Distribution Definition • Let P be the transition matrix of a DTMC and A be a probability distribution on its states. If AP = A, then A is a stationary (or steady-state or invariant or equilibrium) distribution of the DTMC. Question: How many stationary distributions can a Markov chain have? Can it be more than one? Can it be none? IA169 System Verification and Assurance — 12 24/31 Stationary Distributions Answer: It can be more that one. For example, in the Drunkard's walk 1 1 both (1,0,0,0) and (0,0,0,1) are stationary distributions. But, this is not an irreducible Markov chain. IA169 System Verification and Assurance — 12 25/31 Stationary Distributions Theorem • In every finite irreducible DTMC there is a unique invariant distribution. Q: Can it be none? Theorem 9 For each finite DTMC, there is an invariant distribution. Q: How can we compute the invariant distribution of a finite irreducible Markov chain? IA169 System Verification and Assurance — 12 26/31 Stationary Distribution & Cut-sets Again, we can construct a set of equations that express the result. Theorem • Let P be a transition matrix of a finite irreducible DTMC and 7r = (7Ti,7T2,... ,7rn) be a stationary distribution corresponding to P. For any state / of the DTMC, we have IA169 System Verification and Assurance — 12 27/31 Mean Portion of Visited States and Inter Visit Time Theorem Let us have a finite irreducible DTMC and the unique stationary distribution jr. It holds that 7T/ = limn^OQE{ # of visits of state / during the first n steps)//?, Let us have a finite irreducible DTMC and the unique stationary distribution jr. It holds that 7T; = 1 / 777/ where m; is the mean inter visit time of state /. IA169 System Verification and Assurance — 12 28/31 Aperiodic Markov Chains For example: aperiodic periodic Definition • A state s is periodic if there exists an integer A > 1 such that length of every path from s to s is divisible by A. • A Markov chain is periodic if any state in the chain is periodic. • A state or chain that is not periodic is aperiodic. IA169 System Verification and Assurance — 12 29/31 Aperiodic Markov Chains Theorem Let us have a finite aperiodic irreducible DTMC and the unique stationary distribution jr. It holds that 7T = lim n^oo XPn where A is an arbitrary distribution on states. Q: What this is good for? IA169 System Verification and Assurance — 12 30/31 DTMC Extensions - Communication and Nondeterminism Last remark on some DTMC extensions. Modules and synchronisation • modules • actions • rewards Decision extension • Markov Decision Processes (MDP) • Pmin and Pmax properties IA169 System Verification and Assurance - 12 31/31