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

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

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

线性时序逻辑

性质：例子 安全性质： 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

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

例子：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

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

例子：(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

分枝时序逻辑

性质：例子 安全性质： 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

例子：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

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

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

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

自动售茶机：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)

自动售茶机： 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)

CTL*

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

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

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

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

-演算

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

自动售茶机：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}

自动售茶机：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}

自动售茶机：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}