Quantitative Verification - Chapter 7: Continuous-time Markov Chains - TUM

Quantitative VerificationChapter 7: Continuous-time Markov chainsJan Křetı́nskýTechnical University of MunichWinter 2017/181 / 27

Continuous-time Markov chainsCTMC2 / 27

CTMC - MotivationDicrete-time abstraction is fitting for situations whereI flow of time irrelevant: execution steps, steps of a game, . . .I flow of time important but timing within the steps irrelevant:discretized time (e.g. one day per step) without loss of precision.3 / 27

CTMC - MotivationDicrete-time abstraction is fitting for situations whereI flow of time irrelevant: execution steps, steps of a game, . . .I flow of time important but timing within the steps irrelevant:discretized time (e.g. one day per step) without loss of precision.For some problems, the discrete-time abstraction is not appropriate.How long do I need towait (in 1910’) onaverage for atelephone connection?How many pumpmachines a gas stationneeds to satisfy thepeak demand?How often do safetyfunctions in a nuclearpower plant fail (atthe same time)?3 / 27

CTMC - MotivationDicrete-time abstraction is fitting for situations whereI flow of time irrelevant: execution steps, steps of a game, . . .I flow of time important but timing within the steps irrelevant:discretized time (e.g. one day per step) without loss of precision.For some problems, the discrete-time abstraction is not appropriate.How long do I need towait (in 1910’) onaverage for atelephone connection?IIIHow often do safetyHow many pumpmachines a gas station functions in a nuclearpower plant fail (atneeds to satisfy thethe same time)?peak demand?One could address these questions by discretizing time.However, continuous-time models are more suitable.Continuous-time models are actually also easy to solve!3 / 27

CTMC – Stochastic ProcessDefinition4 / 27

CTMC - Math / Statistics Definition (1)RecallA discrete-time stochastic process {Xn n N} over state space S is:IMarkov if for all n 1 and s0 , . . . , sn with P(Xn 1 sn 1 ) 0:P(Xn sn Xn 1 sn 1 , . . . , X0 s0 ) P(Xn sn Xn 1 sn 1 ).Ihomogeneous if for all n 1 and s, s 0 S with P(X0 s) 0:P(Xn 1 s 0 Xn s) P(X1 s 0 X0 s)5 / 27

CTMC - Math / Statistics Definition (1)RecallA discrete-time stochastic process {Xn n N} over state space S is:IMarkov if for all n 1 and s0 , . . . , sn with P(Xn 1 sn 1 ) 0:P(Xn sn Xn 1 sn 1 , . . . , X0 s0 ) P(Xn sn Xn 1 sn 1 ).Ihomogeneous if for all n 1 and s, s 0 S with P(X0 s) 0:P(Xn 1 s 0 Xn s) P(X1 s 0 X0 s)Definition:A continuous-time stochastic process {Xt t R 0 } over states S isIMarkov if for all n 1, 0 t0 t1 · · · tn and s0 , . . . , sn withP(Xtn 1 sn 1 ) 0:P(Xtn sn Xtn 1 sn 1 , . . . , Xt0 s0 ) P(Xtn sn Xtn 1 sn 1 ).Ihomogeneous if for all t, t 0 R and s, s 0 S with P(X0 s) 0:P(Xt t 0 s 0 Xt s) P(Xt 0 s 0 X0 s).We consider only discrete-space homogeneous Markov processes,that we call continuous-time Markov chains (CTMC).5 / 27

CTMC - Math / Statistics definition (2)Sojourn time:Let {Xt t R 0 } be a continuous-time Markov chain. We define foreach state s and i NIIrandom variables As,i , Bs,i denoting time of entering and leavings for the i-th time, respectively i.e. As,1 inf{t 0 Xt s}, andBs,i inf{t As,i Xt 6 s} and As,i 1 inf{t Bs,i Xt s};random variable Ts,i denoting the sojourn time upon the i-thvisit to s, i.e. Ts,i Bs,i As,i .6 / 27

CTMC - Math / Statistics definition (2)Sojourn time:Let {Xt t R 0 } be a continuous-time Markov chain. We define foreach state s and i NIIrandom variables As,i , Bs,i denoting time of entering and leavings for the i-th time, respectively i.e. As,1 inf{t 0 Xt s}, andBs,i inf{t As,i Xt 6 s} and As,i 1 inf{t Bs,i Xt s};random variable Ts,i denoting the sojourn time upon the i-thvisit to s, i.e. Ts,i Bs,i As,i .Observation:For any i and t, t 0 we have from the two propertiesP(Ts,i t t 0 Ts,i t) P(Ts,i t 0 ).6 / 27

CTMC - Math / Statistics definition (2)Sojourn time:Let {Xt t R 0 } be a continuous-time Markov chain. We define foreach state s and i NIIrandom variables As,i , Bs,i denoting time of entering and leavings for the i-th time, respectively i.e. As,1 inf{t 0 Xt s}, andBs,i inf{t As,i Xt 6 s} and As,i 1 inf{t Bs,i Xt s};random variable Ts,i denoting the sojourn time upon the i-thvisit to s, i.e. Ts,i Bs,i As,i .Observation:For any i and t, t 0 we have from the two propertiesP(Ts,i t t 0 Ts,i t) P(Ts,i t 0 ).Proposition:Each Ts,i is exponentially distributed with some rate λs , i.e.FTs,i (x) 1 e λs xfTs,i (x) λs e λs xwith the expected value given by E [Ts,i ] 1.6 / 27

CTMC – Graph Based Definition7 / 27

CTMC [Graph] - Definition (1)Definition: CTMCA continuous-time Markov chain is a tuple (S, R, π0 ) whereI S is the set of states,IIR : S S R 0 is the transition rate matrix, andπ0 is the initial distribution.8 / 27

CTMC [Graph] - Definition (1)Definition: CTMCA continuous-time Markov chain is a tuple (S, R, π0 ) whereI S is the set of states,IIR : S S R 0 is the transition rate matrix, andπ0 is the initial distribution.Definition: Embedded DTMCWe define the exit rate of a state s S asXE (s) R(s, s 0 ) including the self-loop!s 0 SThe embedded DTMC coincides on S and π0 but has the transitionprobability matrix E defined by R(s,s 0 ) E (s) if E (s) 0,0E(s, s ) 0 if E (s) 0 s 6 s 0 , and 1 if E (s) 0 s s 0 .8 / 27

CTMC [Graph] - Definition (2)Definition:The probability measure for a CTMC (S, R, π0 ) is induced by themeasure for cylinder sets P(C (s0 I0 . . . sn )) defined as Yπ0 (s)E(si , si 1 ) e E (si ) inf Ii e E (si ) sup Ii .0 i n9 / 27

CTMC - Solution Techniques10 / 27

CTMC - Transient Analysis (1)Symbolic Solution:For a CTMC C (S, Q, π0 ), the transient probability distribution πtat time t satisfiesdπt πt Q.dtWe can symbolically solve this system of differential equations byπt π0 e Qtwheree Qt X(Qt)ii 0i!.But unfortunately (Qt)i is unstable to compute and the infinite sumis not easy to truncate.11 / 27

CTMC - Transient Analysis (2)Another approach?12 / 27

CTMC - Transient Analysis (2)Another approach?Separate the discrete and continuous randomness!12 / 27

CTMC - Uniformization (1)Definition: Uniformization RateFor a CTMC C (S, R, π0 ) the uniformization rate q is defined asq max E (s).s SDefinition: Uniformized DTMCFor a CTMC C (S, R, π0 ), the uniformized DTMC (withuniformization rate q), denoted by uni(C) is defined as the DTMC(S, P, π0 ) with(R(i, j)for i 6 jR0 (i, j) .Pq k R(i, k) for i j13 / 27

(λt)k k 0, 1, . . .k!Equivalently: the customer interarrival times are exponentiallydistributed with parameter λ (or mean λ1 ) the service times are independent exponentially distributed withparameter µ Example:the semantics is a CTMCf (k; λt) (2)e λtCTMC - UniformizationCTMC:λ0λ1µZhang (Saarland University, Germany)λ2µλ.3µUniformized DTMC with q Quantitative λ µ:Model CheckingµSeptember 02nd , 200911 / 114 / 27

(λt)k k 0, 1, . . .k!Equivalently: the customer interarrival times are exponentiallydistributed with parameter λ (or mean λ1 ) the service times are independent exponentially distributed withparameter µ Example:the semantics is a CTMCf (k; λt) (2)e λtCTMC - UniformizationCTMC:λ0λ1µZhang (Saarland University, Germany)λ2µλ.3µµndCheckingSeptember 02 , 2009Uniformized DTMC with q Quantitative λ µ:Modeladda self-loop withrate µ on 011 / 114 / 27

CTMC - Transient Analysis - By UniformizationLemma:Let C (S, R, π0 ) be a CTMC and uni(C) (S, P, π0 ) its uniformizedDTMC with uniformization rate q and t 0.Let ψ(i, qt) denote the Poisson probability at i (with parameter qt)and πi0 the transient probability distribution of the uniformized DTMCat time step i. Then Xπt ψ(i, qt)πi0 .i 015 / 27

CTMC - Transient Analysis - AlgorithmComputation:How to compute the infinite sumP i 0πi0 ψ(i, qt):16 / 27

CTMC - Transient Analysis - AlgorithmComputation:How to compute the infinite sumIP i 0πi0 ψ(i, qt):The Poisson probabilities decrease very fast, i.e.,limi ψ(i 1, qt)qt lim 0.i i 1ψ(i, qt)16 / 27

CTMC - Transient Analysis - AlgorithmComputation:How to compute the infinite sumIi 0πi0 ψ(i, qt):The Poisson probabilities decrease very fast, i.e.,limi IP ψ(i 1, qt)qt lim 0.i i 1ψ(i, qt)For each 0, the Fox-Glynn algorithm provides bounds L, Rsuch thatRXψ(i, qt) 1 .i LMoreover, ψ(i, qt) for L i R can be computed efficiently.16 / 27

CTMC - Transient Analysis - AlgorithmComputation:How to compute the infinite sumIi 0πi0 ψ(i, qt):The Poisson probabilities decrease very fast, i.e.,limi IP ψ(i 1, qt)qt lim 0.i i 1ψ(i, qt)For each 0, the Fox-Glynn algorithm provides bounds L, Rsuch thatRXψ(i, qt) 1 .i LIMoreover, ψ(i, qt) for L i R can be computed efficiently.Computation of πi0 via the known algorithms for DTMCs.16 / 27

CTMC - Steady-StateTheorem:Steady state of a CTMC exists iff steady state of its uniformizedDTMC exists. In this case, they equal.17 / 27

CTMC - Steady-StateTheorem:Steady state of a CTMC exists iff steady state of its uniformizedDTMC exists. In this case, they equal.By taking higher uniformization rate than maxs E (s), we haveself-loops in every state; hence the uniformized DTMC is aperiodic(other conditions on existence of steady-state were equivalent).17 / 27

Continuous Stochastic Logic(CSL)18 / 27

CSL - Labelled CTMC and SyntaxDefinition: Labelled CTMCA labelled CTMC is a tuple C (S, R, π0 , L) with labelling functionL : S 2AP where AP is a set of atomic propositions.Definition: Syntax of CSLState formulas:Φ true a Φ1 Φ2 Φ PJ (φ) SJ (Φ)where a AP, J [0, 1] is an interval with rational bounds.Path formulas:φ X I Φ Φ 1 U I Φ2where I R 0 denotes an interval.19 / 27

CSL - ExampleExample:Specifying properties using CSLconsidera m:WeWeconsidera tripleup3s3,1up2s2,13λµνδνdown s0,0νs0,1up0µ2λνµλs1,1up120 / 27

CSL - ExampleSpecifications:Let up down, then we can specify the following performanceproperties:IIIISJ (up): steady state availabilityPJ (F[t,t]PJ (G[t,t 0 ]PJ (Φ Uup): instantaneous availability at time t[t,t]up): conditional instantaneous availability at time tup): interval availabilityWe can even nest P and S:IP[0,0.01] (up2 up3 U [0,10] down): The probability of going downwithin 10 time units after having continuously operated with atleast two processors is at most 0.01.IS[0.9,1.0] (P[0.8,1.0] (G [0,10] down)): In the long-run, at least 90% oftime is spent in states where the probability that the systemwill not go down within 10 time units is at least 0.8.21 / 27

CSL - ReachabilityLet us fix a labelled CTMC C (S, R, π0 , L), goal states B S, andinterval of time I R 0 . We write ReachI (B) : Paths(F I B).ReachabilityWhat is the probability P(ReachI (B))?22 / 27

CSL - ReachabilityLet us fix a labelled CTMC C (S, R, π0 , L), goal states B S, andinterval of time I R 0 . We write ReachI (B) : Paths(F I B).ReachabilityWhat is the probability P(ReachI (B))?How to compute it?22 / 27

CSL - ReachabilityLet us fix a labelled CTMC C (S, R, π0 , L), goal states B S, andinterval of time I R 0 . We write ReachI (B) : Paths(F I B).ReachabilityWhat is the probability P(ReachI (B))?How to compute it? First, we address I [0, t]22 / 27

CSL - ReachabilityLet us fix a labelled CTMC C (S, R, π0 , L), goal states B S, andinterval of time I R 0 . We write ReachI (B) : Paths(F I B).ReachabilityWhat is the probability P(ReachI (B))?How to compute it? First, we address I [0, t]Lemma:For any labelled CTMC C (S, R, π0 , L), let C[B] be obtained bymaking states in B absorbing. Then, the reachability probabilityP(ReachI (B)) does not change.22 / 27

CSL - Reachability - Time-boundedTheorem:For C (S, R, π0 , L) with an absorbing set of states B and I [0, t]:12P(Reach[0,t] (B)) P(Reach[t,t] (B)) Xπt (s 0 ).s 0 BProof Sketch:23 / 27

CSL - Reachability - Time-boundedTheorem:For C (S, R, π0 , L) with an absorbing set of states B and I [0, t]:12P(Reach[0,t] (B)) P(Reach[t,t] (B)) Xπt (s 0 ).s 0 BProof Sketch:1. Show that σ Reach[0,t] (B) iff σ Reach[t,t] (B).2. Trivial.23 / 27

CSL - Reachability - Interval Bounded (1)How to solve the case I [a, b]?24 / 27