想要学习线性时序逻辑的论文.pdf

发布时间：2022-06-10 发布人：admin 分类：说明书资料大小：0.10M 资料格式：pdf 举报版权申诉

mawubin525-3575329-4744300845397510412.pdf-第1页.png

第1页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第2页.png

第2页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第3页.png

第3页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第4页.png

第4页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第5页.png

第5页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第6页.png

第6页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第7页.png

第7页 / 共27页

mawubin525-3575329-4744300845397510412.pdf-第8页.png

第8页 / 共27页

文本预览

Linear Temporal Logic

Safety vs. Liveness • Safety : something bad never happens A counterexample is an ﬁnite execution leading to something bad happening (e.g. an assertion violation). • Liveness : something good eventually happens A counterexample is an inﬁnite execution on which nothing good happens (e.g. the program does not terminate).

Veriﬁcation of Reactive Systems • Classical veriﬁcation `a la Floyd-Hoare considered three problems: – Partial Correctness : {ϕ} P {ψ} iﬀ for any s |= ϕ, if P terminates on s, then P (s) |= ψ – Total Correctness : {ϕ} P {ψ} iﬀ for any s |= ϕ, P terminates on s and P (s) |= ψ – Termination : P terminates on s • Need to reason about inﬁnite computations : – systems that are in continuous interaction with their environment – servers, control systems, etc. – e.g. “every request is eventually answered”

Reasoning about inﬁnite sequences of states • Linear Temporal Logic is interpreted on inﬁnite sequences of states • Each state in the sequence gives an interpretation to the atomic propositions • Temporal operators indicate in which states a formula should be interpreted Example 1 Consider the sequence of states: {p, q} {¬p, ¬q} ({¬p, q} {p, q})ω Starting from position 2, q holds forever. 2

Kripke Structures Let P = {p, q, r, . . .} be a ﬁnite alphabet of atomic propositions. A Kripke structure is a tuple K = hS, s0, −→, Li where: • S is a set of states, • s0 ∈ S a designated initial state, • −→ : S × S is a transition relation, • L : S → 2P is a labeling function.

Paths in Kripke Structures A path in K is an inﬁnite sequence π : s0, s1, s2 . . . such that, for all i ≥ 0, we have si −→ si+1. By π(i) we denote the i-th state on the path. By πi we denote the suﬃx si, si+1, si+2 . . .. inf(π) = {s ∈ S | s appears inﬁnitely often on π} If S is ﬁnite and π is inﬁnite, then inf(π) 6= ∅.

Linear Temporal Logic: Syntax The alphabet of LTL is composed of: • atomic proposition symbols p, q, r, . . ., • boolean connectives ¬, ∨, ∧, →, ↔, • temporal connectives , 2, 3, U , R. The set of LTL formulae is deﬁned inductively, as follows: • any atomic proposition is a formula, • if ϕ and ψ are formulae, then ¬ϕ and ϕ • ψ, for • ∈ {∨, ∧, →, ↔} are also formulae. • if ϕ and ψ are formulae, then ϕ, 2ϕ, 3ϕ, ϕU ψ and ϕRψ are formulae, • nothing else is a formula.

Temporal Operators • is read at the next time (in the next state) • 2 is read always in the future (in all future states) • 3 is read eventually (in some future state) • U is read until • R is read releases

分享到：

赞收藏

资料库

想要学习线性时序逻辑的论文.pdf

相关推荐

网络技术

热门标签

最新资料