SPEC属性的形式化表示一逻辑演算 ·数理逻辑（符号逻辑）：描述事实和属性 mone detailed I|=S more abstract "implementation "specification" 一逻辑演算、证明论、集合论、递归论、模型论 (system model) (system property】 "satisfies","implements","refines" ·命题逻辑(propositional logic) (satisfaction relation) 一命题：能判断真假的陈述句，“所有/有的水生动物是肺呼吸的” 》含：个体词（客体，对象）、谓词（个体的性质和关系）、量词 (全称量词、存在量词) 一原子命题：不能分解的命题(“此花是红的”，没有与或非组合) ·谓词逻辑(Predicate logic):命题逻辑的形式化（符号系统) -一阶逻辑（谓词逻辑）：只包含个体谓词和个体量词 》(3x)(F(x)∧G(x):“有的水生动物是肺呼吸的” 一高阶逻辑：包含高阶谓词和高阶量词（个体的个数） 》“是”是一元谓词，“大于”是二元，“在..之间”是三元. ·时态逻辑：时间属性 -时态(temporal)语句：“明天北京下雨” -算子：过去P,现在T,未来F
SPEC属性的形式化表示－逻辑演算 • 数理逻辑（符号逻辑）：描述事实和属性 – 逻辑演算、证明论、集合论、递归论、模型论 • 命题逻辑（propositional logic） – 命题：能判断真假的陈述句， “所有/有的水生动物是肺呼吸的” » 含：个体词（客体，对象）、谓词（个体的性质和关系）、量词 （全称量词、存在量词） – 原子命题：不能分解的命题（“此花是红的” ，没有与或非组合） • 谓词逻辑（Predicate logic）：命题逻辑的形式化（符号系统） – 一阶逻辑（谓词逻辑）：只包含个体谓词和个体量词 » (ヨx)(F(x)∧G(x))： “有的水生动物是肺呼吸的” – 高阶逻辑：包含高阶谓词和高阶量词（个体的个数） » “是”是一元谓词， “大于”是二元，“在…之间”是三元… • 时态逻辑：时间属性 – 时态（temporal）语句： “明天北京下雨” – 算子：过去P，现在T，未来F
CTL 时序逻辑CTL* CTL LTL Ψ1 Ψ2 Ψ3 4 包括两类 -线性时序逻辑LTL:时态运算符限定于描述从一个给定的 状态开始的某条路径上的事件 一分支时序逻辑(CTL,计算树逻辑)：时态运算符限定于 从一个给定的状态开始的所有可能路径上 主要差别：如何处理展开Kripke:结构所对应的计算树分支 a52n053a654n 53b a b 0 60616263 54 S5 Q50 S3c 84b 0·12 3 ·4 5 sib os2d o53d 55b c ,53e S2f· 01 ·2 3·4 5 A linear and a branching time model
时序逻辑CTL* • 包括两类 – 线性时序逻辑 LTL：时态运算符限定于描述从一个给定的 状态开始的某条路径上的事件 – 分支时序逻辑（CTL，计算树逻辑）：时态运算符限定于 从一个给定的状态开始的所有可能路径上 – 主要差别：如何处理展开Kripke结构所对应的计算树分支 A linear and a branching time model
线性时态逻辑LTL Linear--time Temporal Logic的特点 -将时间建模成状态序列(tick？),无限延伸到未来 ·该状态序列称为计算路径（简称“路径”） 一隐含了整个系统是按着一个路径向前发展演化的 -“隐含使用全称量词，不使用存在量词”一与CTL不同！ 一使用指示未来的连接词（时间操作符） ·未来一般不确定，出现若干可能路径（指G、F、X等？） -只表达一个路径上的不确定性，而CTL表达多个“路径” 52a653n654n: 652b。53b: 558 0 S5 6505152534 G50 52c653cd 84b 012345 51b52do53d: 、55b 53 S2f 0 '3 4 '5
线性时态逻辑LTL • Linear-time Temporal Logic的特点 – 将时间建模成状态序列（tick？），无限延伸到未来 • 该状态序列称为计算路径（简称“路径”） – 隐含了整个系统是按着一个路径向前发展演化的 – “隐含使用全称量词，不使用存在量词”——与CTL不同！ – 使用指示未来的连接词（时间操作符） • 未来一般不确定 未来一般不确定，出现若干可能路径 出现若干可能路径（指G、F、X等？） – 只表达一个路径上的不确定性，而CTL表达多个“路径
Linear Temporal Logic(LTL) 0 LTL公式的构成 -项(terms):The symbol“p”is an atomic proposition ·e.g.:DeviceEnabled 一经典布尔操作 ·(not),V(or),∧(and) 。-→(imply,.if-then:p→q,如果p发生则会出现g -基本时态操作(Basic temporal operators) ·▣(G,always)),◇(F,eventually),O(X,next,U(strong until) Gp-p holds globally in the future. ·Fp-p holds sometime(不确定性！)in the future.. ·Xp-p holds next time. pUq-p holds until g holds. 01 ·2 3 ·4 '5
Linear Temporal Logic (LTL) • LTL公式的构成 – 项（terms）：The symbol “p” is an atomic proposition • e.g. ：DeviceEnabled – 经典布尔操作 • ﹁ (not), ∨(or), ∧(and) • →(imply, if-then)：p →q，如果p发生则会出现q – 基本时态操作（Basic temporal operators temporal operators） • □ (G，always), ◇(F，eventually), ○(X，next), U (strong until). • Gp - p holds globally in the future. • Fp - p holds sometime（不确定性！） in the future. • Xp - p holds next time. • pUq - p holds until q holds
LTL语义 ·时序操作符 -<>p:p在以后某个时刻（最终）会真.future p -p：从当前时刻起，p总是为真.globlly p p p p p p p p p -Xp:p在下一时刻为真。next p
LTL语义 • 时序操作符 – <>p： p 在以后某个时刻（最终）会真. future – []p ：从当前时刻起， p总是为真. globlly p – []p ：从当前时刻起， p总是为真. globlly – Xp: p在下一时刻为真。next p p p p p p p p p p