i i † iす565–0871 1–5 E-mail: †{a-ito,t-nagaok,okano,kusumoto}@ist.osaka-u.ac.jp

CEGAR
Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique Akihiko ITO†, Takeshi NAGAOKA†, Kozo OKANO†, and Shinji KUSUMOTO† † Graduate School of Information Science and Technology, Osaka University Yamada-oka 1–5, Suita City, Osaka, 565–0871 Japan E-mail: †{a-ito,t-nagaok,okano,kusumoto}@ist.osaka-u.ac.jp Abstract  This paper gives a reachability analysis technique for Probabilistic Timed Automaton (PTA), based on CEGAR loop. The proposed method uses a transformation technique in order to avoid influence caused by dynamic change of behaviour with elapsing time. Key words   Timed Probabilistic System, Model Checking, CEGAR, Simulation 1. [1] [2] 2.
R R* 0 3. 4. 5.
2. CEGAR CEGAR
120
t 0 ν [ X := 0]レ2レ+ t Zones(X) ζ ::= x ～ c | x − y ～ c | ζ ∧ ζ | true a) time transitions t ≤ 0 μ = μ(l,v+t) ν + t' ▷ inv(l) 0 ≥ t ′ ≥ t b)   discrete transitions (X, l') ∈ support(p) t = 0レやg ν [ X  := 0] ▷ inv ( l ′ ) (l, g, p) E prob (l',v) E S p(X, l') x ∑ x &ﾉ≡レ[ X : = 0] L'((l,v)) = L(l) for all (l,v) E S 2.1.5 well-formed well- formed [3] PTA = (L, lo, Act, X, inv, prob, L) well-formed ∀(l, g, p) ∈ prob. ∀ν ∈ R ξ 0. (ν ≥ g) → (∀(X',l') ∈ support(p). ν[X := 0] ▷ inv(l')). well- formed 2.1.6 PTA = (L, l 0 , Act, X, inv, prob, L) (l, g, p)  E  prob p( X , l') > 0 (l, g, p, X, l') 5 edges(l, g, p) (l, g, p) edges = {edges(l,p,g) | (l,g,p) E prob} 2.4 ( ). PTA = (L, l 0 , Act, X, inv, prob, L) TPSpta = (S, so, TSteps, L' ) S ⊆ L × R ×  (l,v) ∈ S . ν ▷ inv(l) so = (lo, vo) . ((l,v),t,μ) ∈ TSteps X ζ ζ V x ς 2.1.3 2.1 ( PTA TPSpta = (S, so, TSteps, L) • S •  ●   TSteps ⊆ S × R ≥ 0 × Dist( S ) (s,t,μ) ∈ TSteps        t > 0 duration (s, t, μ)      t μ •   L : S → 2AP 2.1.4 2.2 ( ). PTA PTA = (L, lo, Act, X, inv, prob, L) 7 . L l o . . Act . X inv : L → Zones(X) . prob ⊆ L × Zones(X) × Dist(2 × × L) . ●  DBM(Difference Bound Matrix) [4] 2.1.7 νやζ
). TPSpta 4 x,y E X ～ E {<,>,<,>} ν(x) 1 = 0 a . d zz : == 0 ∧ y == 1 a 1 2.1 (2 PTA ). 1 (lo , vo ll (L w ωβ isCompatible(ω * true false E N such that ω (i + 1)̸= ω β (i + 1) if ( ^Vj ≤ i ∈ N. ω α ( j ) otherwise true i + 1 i + 1 3 2.3 2.2 (2 PTA Ω ). 2. 3. 1 Ω isCompatible(Ω) true
2.3.2 ValueIteration [6] ValueIteration 4 V(AV, E 2,2 such that Ω′ ≠ Ω V |Ω′| ≥ 2). isCompatible(Ω′) false otherwise ValueIteration 2.1
Ω 2.2
b
[1] = 0 ∧ y 1.0,0 0 ∧ y d 0 ∧ y = 0.5,1 1.0,0 1) 0》 : 0 ∧ y = : 1) 2.2 Clarke [1] Guided  Abstraction  Refinement [5] Counter-example CEGAR 2 3. d PTA [ true U err] PCTL P<p err p 3.1 [1] err PCTL over approximation 3.2 ValueIteration p true 3.3 (   ) k- [1] DBM [7] 3.4 [1] 3.5 k- (   )
1: 〈 := true 2:  for i := n down to 2 do 3: 4: 5:
6: e := (lprcv, g, p, X, lcurr) {∈ edges} 7: ζ := free(ζ, e) ∧ gc ∧ inv(lprcv) 8: Zω[ｽ] := ζ {Zω[ｽ]سER := ERU (l,lcurr,e,c){ 9: down(ζ) 10: 11: end for 12:  return  (Z, ER) } 2.2 3.5.1 Algorithm1 1 e = (lprcv, 9c, Pc, Xc, l) l lprev free [7] free l e = free(inv(l), e) ∧ gc ∧ inv(lprcv) down down w Algorithm1 PTA 1.1 ζ lpren 3 Zω [ï] lo lpres = p Algorithm 2 IsCompatible(Ω, Z, index) 1: ζ := true, NSIM := ∅, N LS := ∅ 2:  for all ω ′ ∈ Ω such that |ω ′ | > index do lnext := ω ′ [index + 1] 3: if Incxt & NLS then 4: NLS := NLSU {Inext} 5: Ωιπακε := 0 6: end if 7: } { 'u' } } } } } } 8: 9:  end for 10:  if |NLS| ≥ 2 then for all ω ′ ∈ Ω do 11: ζ := ζ ∧ Ζω [index] 12: if ζ = false then 13: NSIM := NSIM ∪ {ω'[index]} { 14: NSIM } break 15: 16: end if end for 17: for all lnext E N LS do 18: NSIM := NSIM ∪ IsCompatible(index + 1, Ω l n ext ) 19: end for 20: 21: end if 22: return NSIM isCompatible IsCompatible  Algorithm2 z ω C C NSIM IsCompatible 3.6 Algorithm 3 TransformPTA(PTA, Z, NSIM) 1:  DLS := ∅, POWZ := ∅ 2:  for all l ∈ NSIM do POWZ := PowZ(l,Z) 3: l E :=getTransitionSet(l) { E 4: DLS := MakeDuplicateZoneLocation( l , DLS) 5: MakeTransition( l , a , POWZ, DLS) 6: RemoveTransition( E ) { 7: E 1 8: end for 9: return PTA } Algorithm 4 MakeDuplicateZoneLocation( l , DLS) 1: for all ltmp ∈ NEXT(l) do ldup := newLocation() { 2: } for all ( lprcv, l ′ , e, ζtmp ) ∈ ER such that lprcv = l and 3: ltmp = l' do inv(ldup) := dupinv(l,ltmp,e,Çtmp) 4: end for 5: 6: L := L ∪ {ldup} DLS := DLS ∪ {ldup} { 7: } for all ( lprcv, g, p, X, l' ) E edges such that lprcv = ltmp 8: and g ∈ inv(ldup) do 9: edges := edges ∪ {( ldup, g, p, X, l ′ )} 10: end for 11: end for 12: return  DLS PTA M ī inv( ) l dupinv inv(l) dupinv(l,lprcv,e,C) = ／ ((¬ζ ∧ inv(lprcv) ∧ gc)[X := 0]) ∧ inv(l) l 1 e lprev ς l Algorithm2 l l NSIM formPTA(Algorithm3) TransformPTA PTA MDP ER Algorithm4 dupinv 4 ī ī inv( ζ ) Algorithm4 Trans- 19 ValueIteration Algorithm 5 PowZ(l, ER) 1: ζροω := true, Zoc := 0, POW Z [ l ] 2:  for all ( lcurr , l ′ , e, ζ ) ∈ ER such that lcurr = l do Zoc := Zoc U {ζ} {l 3: } 4:  end for 5: for all Z ∈ POWERSET(Zoc) do {POWERSET 6: Z } 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: Çpow := Çpow ∧ ¬Çl end if end for if ζροω ≠ ∅ then POWZ[l] := POWZ[l] ∪ {{pow} end if ζροω := true 17: 18: end for 19: return POWZ[i]
Algorithm 6 MakeTransition( l , POWZ[ l ], DLS)
1:  for all ζ ∈ POWZ[l] do for all lnext ∈ NEXT(l) do 2: l { NEXT 3: } if Incxt E DLS then 4: ldup := DupZoneMap(lnext) 5: for all (lprcv, g, p, X, l') ∈ edges such that lprcv = 6: l do 7: edges := edges ∪ {(lprev, g, p, X, ldup)} end for 8: for all ( lprcv, 9, p, X, l ′ ) ∈ edges such that lprcv = l and l' = lnext do edges := edgesし{(l, g, p, X, l')} end for PTA 2 6 4. for all ζ ¹ ∈ Zoc do if ζ l ∈ Z then Çpow := Çpow Λ Çl else 4.1. M Algorithm3 4.1 5. DBM not not C (21500036) ( ) IT 9: 10: 11: 12: 13: 14: end if end for 15: end for 6 4. ζ1 , ζ2 ¬Ç1 ∧ Ç2   Ç1 ∧ ¬Ç2 51 ∧ 52 PowZ Algorithm5 [1] T. Nagaoka, K. Okano, and S. Kusumoto. An abstrac- tion refinement technique for timed automata based on counterexample-guided abstraction refinement loop. IEICE Transactions on Information and Systems , Vol. E93-D, No. 5, p. to appear, May 2010. T. Han and J. Katoen. Counterexamples in probabilis- [2] tic model checking. Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS), pp. 72– 86, 2007. M. Kwiatkowska, G. Norman, J. Sproston, and [3] F. Wang.  Symbolic model checking for probabilistic timed automata. Inf. and Comp., Vol. 205(7), pp. 1027– 1077, 2007. [4] A. David, J. Hakansson, K. G. Larsen, and P. Petterson. Model checking timed automata with priorities using dbm subtraction. Lecture Notes in Computer Science, Vol. 2402, pp. 128–142, 2006. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. [5] Counterexample-guided abstraction refinement. Inter- national Conference on Computer Aided Verification (CAV'00) , pp. 154–169, 2000. D.P. Bertsekas.  Dynamic programming and optimal [6] control. Athena Scientific, 1995. http://www-sdl.ist.osaka-u.ac.jp/~a-ito/proof/ [7] pta_cegar_full.pdf. 13 "S [7] else