时序逻辑 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv.

Presentation on theme: "时序逻辑 中国科学院软件研究所 张文辉 http://lcs.ios.ac.cn/~zwh/pv."— Presentation transcript:

1 时序逻辑 中国科学院软件研究所 张文辉

2 系统运行过程描述：例子 初始状态 s0 t0 x=0 y=0 t=0 s0 t0 y=1,t=1 x=1,t=0 s1 t1
2

3 性质：例子 安全性质 响应性质 公平性质 申请马上得到 申请保证得到 先申请者优先 先申请者先得到 3

4 线性时序逻辑

5 性质：例子 安全性质： G (!(a=s2b=t2)) 响应性质： F (a=s2b=t2) 公平性质： G F (a=s2)
申请马上得到： G (a=s1  X (a=s2)) 申请保证得到： G (a=s1  F (a=s2)) 先申请者优先： G (a=s1b!=t1b!=t2  (a=s2 R b!=t2)) 先申请者先得到： G (a=s1b!=t1b!=t2  (b!=t2 U a=s2)) 5

6 例子：Op  Op ζ |= Op ζ1 |= p ζ1 |= p ζ |= Op ζ |= Op 6

7 例子：pRq  (qU(qp))[]q
对任意i0, ζi |= q 或 存在i0, ζi |= p 且对任意ji, ζj |= q ζ |= pRq 对任意i0, 若对所有j<i, ζj |=p, 则ζi |=q 7

8 例子：(p[]Op) → []p Op → (p → Op) [](Op → (p → Op)) []Op → [](p → Op)
8

9 例子：(Op → Oq) → O(p → q) q → (p → q) [](q → (p → q)) O(q → (p → q))
(Oq Op) → O(p → q) p → (p → q) [](p → (p → q)) O(p → (p → q)) Op → O(p → q) 9

10 分枝时序逻辑

11 性质：例子 安全性质： AG (!(a=s2b=t2)) 响应性质： AF (a=s2b=t2) 公平性质：
申请马上得到： AG (a=s1  AX (a=s2)) 申请保证得到： AG (a=s1  AF (a=s2)) 先申请者优先： AG (a=s1b!=t1b!=t2  A(a=s2 R b!=t2)) 先申请者先得到： AG (a=s1b!=t1b!=t2  A(b!=t2 U a=s2)) 11

12 例子：Z.f(Z)=Z.fZ) Z.f(Z) = {Z|f(Z)Z} Z.f(Z) = {Z|f(Z)Z}
Z.f(Z) = S\ {Z|f(Z)Z} Z.f(Z) = {S\Z|f(Z)Z} Z.f(Z) = {Z|f(Z)Z} Z.f(Z) = {Z|f(Z)Z} = Z.f(Z) 12

13 自动售茶机 s0 取钱 1 2 s1 s2 取茶 1 2 1 2 2 s6 s3 s4 s7 1 找钱/取钱 出茶 退钱 s5

14 自动售茶机 {p0,q0} s0 1 2 {p1,q0} {p2,q0} s1 s2 1 2 1 2 出茶/取茶 2 {p4,q1} s3
找钱/取钱 s5 {p3,q2}

15 自动售茶机 {p0,q0} s0 {p1,q0} {p2,q0} s1 s2 {p4,q1} s3 s4 {p2,q0} s5

16 自动售茶机：E(q0Uq2) E(q0Uq2) = Z.(q2(q0EX Z)) S0=false S1=q2 = {s5}
S2={s5}({s0,…,s3}{s1,…,s4}) = {s1,s2,s3,s5} S3={s5}({s0,…,s3}{s0,…,s4}) = {s0,s1,s2,s3,s5} S4={s5}({s0,…,s3}{s0,…,s5}) = {s0,s1,s2,s3,s5} 该模型满足E(q0Uq2)

17 自动售茶机： AG(q0q2) AG(q0q2) = Z.((q0q2)  AX Z) S0=true
S1=q0q2 = {s0,s1,s2,s3,s5} S2={s0,s1,s2,s3,s5}{s0,s1,s4,s5} = {s0,s1,s5} S3={s0,s1,s2,s3,s5}{s4,s5} = {s5} S4={s0,s1,s2,s3,s5}{s4} = {} S5={} 该模型不满足AG(q0q2)

18 CTL*

19 表示能力 E(GFp)不同于EGEFp 考虑A(FGp): A(FGp)不同于AFAGp p p p 19

20 表示能力 AGEF p 不等价于任何PLTL公式 M: M’: M |= AGEF p 且 M’ |= AGEF p
若M |= Aφ 则 M’ |= Aφ, 矛盾． p p p 20

21 表示能力 F(pXp) 不等价于任何CTL公式 M1: N1: Mi+1: Ni+1: p p p p p p p Mi p p
21

22 表示能力 E(GFp)不等价于任何CTL和PLTL公式 PLTL: CTL: 考虑A(FGp) A(FGp)不等价于任何CTL公式 p
22

23 -演算

24 自动售茶机 {p0,q0} s0 1 2 {p1,q0} {p2,q0} s1 s2 1 2 1 2 出茶/取茶 2 {p4,q1} s3
找钱/取钱 s5 {p3,q2}

25 自动售茶机：X.(q2<1>X)
S0=false S1=q2<1>{} = {s5} S2={s5}{s2,s3} = {s2,s3,s5} S3={s5}{s1,s2,s3} = {s1,s2,s3,s5} S4={s5}{s0,s1,s2,s3} = {s0,s1,s2,s3,s5} S5={s5}{s0,s1,s2,s3} = {s0,s1,s2,s3,s5}

26 自动售茶机：X.(q2[1]X) S0=true S1=q2 = {s0,s1,s2,s3,s4}
S2={s0,s1,s2,s3,s4}{s0,s1,s4,s5} = {s0,s1,s4} S3={s0,s1,s2,s3,s4}{s0,s4,s5} = {s0,s4} S4={s0,s1,s2,s3,s4}{s4,s5} = {s4} S5={s0,s1,s2,s3,s4}{s4,s5} = {s4}

27 自动售茶机：X.(q2[1]X) S0=false S1=q2[1]{} = {s5}{s4,s5} = {s4,s5}
S2={s5}{s2,s3,s4,s5} = {s2,s3,s4,s5} S3={s5}{s1,s2,s3,s4,s5} = {s1,s2,s3,s4,s5} S4={s5}{s0,s1,s2,s3,s4,s5} = {s0,s1,s2,s3,s4,s5} S5={s0,s1,s2,s3,s4,s5}