(temporal logic) (modal logic)!! LTL! CTL! liveness safety properties! (Model Checking)!
LTL (linear-time temporal logic) Syntax! p Atoms (propositional atoms)! φ::= T p ( φ) (φ φ) (φ φ) (φ φ) (X φ)!! next (F φ)!! some Future state (G φ)!! Globally (all future states) (φ U φ)!! Until (φ W φ)!! Weak until (φ R φ)!! Release
Semantics ( ) Transition System! transition system (model) M=(S,, L)! S : (state)! : S S : (transition relation)! L : S P(Atoms)!!! : (labelling function)! Atoms: (atomic formulas)! (computation path)! s1, s2, si S, si si+1! π=s1 s2! πi: si π (suffix)! : π3=s3 s4
s0 p, q q, r r s2 s0 s2 s2 s2 s2 s2 s0 s1 s2 s2 s2 s2 s0 s1 s0 s2 s2 s2 s0 s1 s0 s1 s2 s2... s1 s0 s1 s2 s0 s2 s2 1 s1 s2 s2 s2
Semantics ( ) M=(S,, L), π=s1 s2! : (satisfaction relation)! π! =! T! π! =!! π! =! p!!! iff p L(s1)! π! =! φ!! iff π! = φ! π! =! φ1 φ2! iff π! = φ1 and π =φ2! π! =! φ1 φ2! iff π! = φ1 or π = φ2! π! =! φ1 φ2! iff π! = φ2 whenever π =! φ1
π! =! Xφ!!!! iff! π 2! =! φ! π! =! Gφ!!!! iff! π i! =! φ for every i 1! π! =! Fφ!!!! iff! π i! =! φ for some i 1! π! =! φuψ!!! iff! π i! =! ψ for some i 1 and!!!!!! π j! =! φ for every j!! such that 1 j<i! π! =! φwψ!!! iff! π i! =! ψ for some i 1 and!!!!!! π j! =! φ for every j! ( φwψ!! (φuψ) Gφ!!! )!!! such that 1 j<i!!!!!! or!!!!!! π k! =! φ for every k 1! π! =! φrψ!!! iff! π i! =! φ for some i 1 and!!!!!! π j! =! ψ for every j! such that 1 j i!!!!!! or! ( φrψ!! ψw(φ ψ)!! )! π k! =! ψ for every k 1
G (started ready)! started ready! G(requested F acknowledged)! request! G F enabled! enabled! ) enabled sm sm+1 F enabled n>m sn enabled
F G deadlock! deadlock! G F enabled G F running! enabled! G(floor2 directionup BottonPressed5 (directionup U floor5))! 2 5 5
M=(S,, L), s S! d M, s φ s M π π φ!! M! s φ
s0 s0 p q s0 Xr p, q s0 X(q r) s0 G(r q) q, r r s2 s0 F(p r) s0 pur s2 FGr s1 s s F( q r) FGr
! M! (a)-(e)( φ ) (1)(2)! (a) Gp (b) puq (c) pux(p q)! (d) X q G( p q)! (e) X(p q) F( p q) (1) s3 φ! (2) M,s3 =φ s1 s2 p, q p, q p, q p, q s3 s4 A model of M
LTL! LTL φ ψ M M π! π = φ iff π = ψ! φ ψ! φ ψ!!! φ χ φ ψ χ φ ψ χ
! Gφ F φ! Fφ G φ! Xφ X φ! (φuψ) φr ψ! (φrψ) φu ψ! F(φ ψ) Fφ Fψ! G(φ ψ) Gφ Gψ! Fφ TUφ! Gφ Rφ!!
/ (mutual exclusion)! Safety property : (critical section) 1 (mutual exclusion)! Liveness property: ( ) (Starvation-free/deadlock-free)! No strict sequencing:! Non-blocking:
1 2 non-critical n1 n2 t1 t2 trying to enter critical section c1 c2 critical section
Safety : G (c1 c2)! Liveness: G(t1 Fc1)! No strict sequencing: G(c1 c1w( c1 c1wc2))! c1 c1 c2 c1!...... c1 c1 c1 c1... c2 c1 strict seq. Non-Blocking: n1 t1 LTL ( )
1 n1n2 s0 s1 t1n2 s5 n1t2 s2 c1n2 s3 t1t2 s6 n1c2 s4 c1t2 n: non-critical state t: trying to enter critical state c: critical state s7 t1c2
Safety : G (c1 c2)! Liveness: G(t1 Fc1)! No strict sequencing: G(c1 c1w( c1 c1wc2))! c1 c1 c2 c1
2 s0 n1n2 s1 t1n2 s5 n1t2 s2 c1n2 s3 t1t2 s9 t1t2 s6 n1c2 s4 s7 c1t2 t1c2
s3, s9! Safety! Liveness! No strict sequencing
3 n1 Main1 Main2 n2 t1 I=1? n I=2? n t2 y y CS1 CS2 c1 c2 I:=2 I:=1
s0 n1n21 s6 n1n22 s1 t1n21 s2 n1t21 s7 t1n22 s8 n1t22 s3 c1n21 s4 t1t21 s9 t1t22 s10 n1c22 s5 c1t21 s11 t1c22
Safety! Liveness! ( Starvation-free: GF c1! No strict sequencing! Main )!
4 Dekker s Solution (logical version) LL (LR MR)? (LR MR) TL? LR (LL ML)? (LL ML) TL? ML CS1! TL false MR CS2 TL true TL? SL TL? SR PL Main1 PR Main2
Safety! Liveness (Main OK)! No strict sequencing