时序逻辑演示课件.ppt

自动售茶机 s0 1 1 1 2 1 s1 s3 s5 2 s2 2 s4 找钱/取钱 2 出茶/取茶 {p3,q2} {p2,q0} {p0,q0} {p1,q0} {p2,q0} {p4,q1} 好好的 自动售茶机 s0 s1 s3 s5 s2 s4 {p0,q0} {p4,q1} {p3,q2} {p2,q0} {p1,q0} {p2,q0} 好好的 自动售茶机：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 时序逻辑 中国科学院软件研究所 张文辉 /~zwh/pv 好好的 x==0||t==0 好好的 系统运行过程描述：例子 t0 x=1,t=0 t1 t2 y==0||t==1 t3 x=0 s0 y=1,t=1 s1 s2 s3 y=0 初始状态 s0 t0 x=0 y=0 t=0 好好的 性质：例子 安全性质 响应性质 公平性质 申请马上得到 申请保证得到 先申请者优先 先申请者先得到 线性时序逻辑 好好的 好好的 性质：例子 安全性质： 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)) 好好的 例子：Op ? ?O?p ζ |= Op ζ1 |= p ζ1 |= ?p ζ |= O?p ζ |= ?O?p 好好的 例子：pRq ? (qU(q?p))?[]q ζ |= (qU(q?p))?[]q 对任意i?0, ζi |= q 或 存在i?0, ζi |= p 且对任意j?i, ζj |= q ζ |= pRq 对任意i?0, 若对所有ji, ζj |=p, 则ζi |=q 好好的 例子：(p?[]Op) → []p Op → (p → Op) [](Op → (p → Op)) []Op → [](p → Op) [](p → Op) p → []p []p 好好的 例子：(Op → Oq) → O(p → q) q → (p → q) [](q → (p → q)) O(q → (p → q)) Oq → O(p → q) (Oq ?O?p) → O(p → q) ?p → (p → q) [](?p → (p → q)) O(?p → (p → q)) O?p → O(p → q) 分枝时序逻辑 好好的 好好的 性质：例子 安全性质： 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)) 好好的 例子：?Z.f(Z)=??Z.?f?Z) ?Z.f(Z) = ?{Z|f(Z)?Z} ?Z.?f(?Z) = ?{Z|?f(?