プログラム理論2014.key

Size: px

Start display at page:

Download "プログラム理論2014.key"

えのおおかわち
4 years ago
Views:

1 (temporal logic) (modal logic)!! LTL! CTL! liveness safety properties! (Model Checking)!

2 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

3 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

4 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

5 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

6 π! =! 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

7 G (started ready)! started ready! G(requested F acknowledged)! request! G F enabled! enabled! ) enabled sm sm+1 F enabled n>m sn enabled

8 F G deadlock! deadlock! G F enabled G F running! enabled! G(floor2 directionup BottonPressed5 (directionup U floor5))! 2 5 5

9 M=(S,, L), s S! d M, s φ s M π π φ!! M! s φ

10 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

11 ! 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

12 LTL! LTL φ ψ M M π! π = φ iff π = ψ! φ ψ! φ ψ!!! φ χ φ ψ χ φ ψ χ

13 ! Gφ F φ! Fφ G φ! Xφ X φ! (φuψ) φr ψ! (φrψ) φu ψ! F(φ ψ) Fφ Fψ! G(φ ψ) Gφ Gψ! Fφ TUφ! Gφ Rφ!!

14 / (mutual exclusion)! Safety property : (critical section) 1 (mutual exclusion)! Liveness property: ( ) (Starvation-free/deadlock-free)! No strict sequencing:! Non-blocking:

15 1 2 non-critical n1 n2 t1 t2 trying to enter critical section c1 c2 critical section

16 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 ( )

17 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

18 Safety : G (c1 c2)! Liveness: G(t1 Fc1)! No strict sequencing: G(c1 c1w( c1 c1wc2))! c1 c1 c2 c1

19 2 s0 n1n2 s1 t1n2 s5 n1t2 s2 c1n2 s3 t1t2 s9 t1t2 s6 n1c2 s4 s7 c1t2 t1c2

20 s3, s9! Safety! Liveness! No strict sequencing

21 3 n1 Main1 Main2 n2 t1 I=1? n I=2? n t2 y y CS1 CS2 c1 c2 I:=2 I:=1

22 s0 n1n21 s6 n1n22 s1 t1n21 s2 n1t21 s7 t1n22 s8 n1t22 s3 c1n21 s4 t1t21 s9 t1t22 s10 n1c22 s5 c1t21 s11 t1c22

23 Safety! Liveness! ( Starvation-free: GF c1! No strict sequencing! Main )!

24 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

25 Safety! Liveness (Main OK)! No strict sequencing

( ) P, P P, P (negation, NOT) P ( ) P, Q, P Q, P Q 3, P Q (logical product, AND) P Q ( ) P, Q, P Q, P Q, P Q (logical sum, OR) P Q ( ) P, Q, P Q, ( P

( ) P, P P, P (negation, NOT) P ( ) P, Q, P Q, P Q 3, P Q (logical product, AND) P Q ( ) P, Q, P Q, P Q, P Q (logical sum, OR) P Q ( ) P, Q, P Q, ( P Advent Calendar 2018 @Fukuso Sutaro,,, ( ) Davidson, 5, 1 (quantification) (open sentence) 1,,,,,, 1 1 (propositional logic) (truth value) (proposition) (sentence) 2 (2-valued logic) 2, true false (truth