Logic cây tính toán

Logic cây tính toán - Wikipedia

Logic cây tính toán (CTL) là logic thời gian phân nhánh, nghĩa là mô hình thời gian của nó là một cấu trúc giống như cây trong đó tương lai không được xác định; có những con đường khác nhau trong tương lai, bất kỳ một trong số đó có thể là một con đường thực tế được nhận ra. Nó được sử dụng để xác minh chính thức các tạo phẩm phần mềm hoặc phần cứng, thường là bởi các ứng dụng phần mềm được gọi là trình kiểm tra mô hình xác định xem một tạo phẩm cụ thể có thuộc tính an toàn hoặc độ bền không. Ví dụ: CTL có thể chỉ định rằng khi một số điều kiện ban đầu được thỏa mãn (ví dụ: tất cả các biến chương trình là dương hoặc không có ô tô trên đường cao tốc đi hai làn), thì tất cả các thực thi có thể của chương trình sẽ tránh một số điều kiện không mong muốn (ví dụ: chia số cho không hoặc hai chiếc xe va chạm trên đường cao tốc). Trong ví dụ này, thuộc tính an toàn có thể được xác minh bởi trình kiểm tra mô hình khám phá tất cả các chuyển đổi có thể ra khỏi trạng thái chương trình thỏa mãn điều kiện ban đầu và đảm bảo rằng tất cả các thực thi đó thỏa mãn thuộc tính. Logic cây tính toán nằm trong một lớp logic thời gian bao gồm logic thời gian tuyến tính (LTL). Mặc dù có các thuộc tính chỉ có thể biểu thị trong CTL và các thuộc tính chỉ có thể biểu thị bằng LTL, nhưng tất cả các thuộc tính có thể biểu thị theo logic cũng có thể được biểu thị bằng CTL *.

CTL lần đầu tiên được đề xuất bởi Edmund M. Clarke và E. Allen Emerson vào năm 1981, người đã sử dụng nó để tổng hợp cái gọi là bộ xương đồng bộ hóa i.e .

Cú pháp của CTL [ chỉnh sửa ]

Ngôn ngữ của các công thức được hình thành tốt cho CTL được tạo bởi ngữ pháp sau:

{displaystyle {begin{aligned}phi &::=bot mid top mid pmid (neg phi )mid (phi land phi )mid (phi lor phi )mid (phi Rightarrow phi )mid (phi Leftrightarrow phi )&mid quad {mbox{AX }}phi mid {mbox{EX }}phi mid {mbox{AF }}phi mid {mbox{EF }}phi mid {mbox{AG }}phi mid {mbox{EG }}phi mid {mbox{A }}[phi {mbox{ U }}phi ]mid {mbox{E }}[phi {mbox{ U }}phi ]end{aligned}}}

trong đó ${ displaystyle p}$ nằm trong một tập hợp các công thức nguyên tử . Không cần thiết phải sử dụng tất cả các kết nối - ví dụ: ${ displaystyle { neg, Land, { mbox {AX}}, { mbox {AU}}, { mbox {EU}} }}$ bao gồm một bộ kết nối hoàn chỉnh và những cái khác có thể được xác định bằng cách sử dụng chúng.

${ displaystyle { mbox {A}}}$ có nghĩa là 'dọc theo tất cả các đường dẫn' (chắc chắn)
${ displaystyle { mbox {E}}}$ có nghĩa là 'dọc theo ít nhất (có tồn tại) một đường dẫn' (có thể)

Ví dụ, sau đây là một giếng hình thành công thức CTL:

{ displaystyle { mbox {EF}} ({ mbox {EG }} p Rightarrow { mbox {AF}} r}

)

Sau đây không phải là tốt công thức CTL định dạng:

{displaystyle {mbox{EF }}{big (}r{mbox{ U }}q{big )}}

Vấn đề với chuỗi này là ${ displaystyle U}$ chỉ có thể xảy ra khi được ghép nối với ${ displaystyle A}$ hoặc ${ displaystyle E}$ . Nó sử dụng các đề xuất nguyên tử làm các khối xây dựng của nó để đưa ra tuyên bố về các trạng thái của một hệ thống. CTL sau đó kết hợp các đề xuất này thành các công thức bằng cách sử dụng các toán tử logic và logic thời gian.

Toán tử [ chỉnh sửa ]

Toán tử logic [ chỉnh sửa ]

Toán tử logic là những toán tử thông thường: ¬, ∨,, Và. Cùng với các toán tử này, các công thức CTL cũng có thể sử dụng các hằng số boolean đúng và sai.

Toán tử tạm thời [ chỉnh sửa ]

Các toán tử tạm thời như sau:

Bộ định lượng trên các đường dẫn
- A φ - A ll: φ phải giữ trên tất cả các con đường bắt đầu từ trạng thái hiện tại.
- E φ - E xist: tồn tại ít nhất một đường dẫn bắt đầu từ trạng thái hiện tại nơi giữ.
- X φ - Ne x t: φ phải giữ ở trạng thái tiếp theo (toán tử này đôi khi được ghi chú của X ).
- G φ - G lobally: φ phải giữ trên toàn bộ con đường tiếp theo. F φ - F inally: cuối cùng phải giữ (ở đâu đó trên con đường tiếp theo).
- φ U ψ - U ntil: phải giữ ít nhất là cho đến khi tại một vị trí nào đó . Điều này ngụ ý rằng ψ sẽ được xác minh trong tương lai.
- φ W ψ - W eak cho đến khi: phải giữ cho đến khi giữ. Sự khác biệt với U là không có gì đảm bảo rằng sẽ được xác minh. Toán tử W đôi khi được gọi là "trừ khi".

Trong CTL *, các toán tử tạm thời có thể được trộn lẫn tự do. Trong CTL, toán tử phải luôn được nhóm thành hai: toán tử một đường dẫn theo sau là toán tử trạng thái. Xem các ví dụ dưới đây. CTL * hoàn toàn biểu cảm hơn CTL.

Tập hợp toán tử tối thiểu [ chỉnh sửa ]

Trong CTL có một tập hợp toán tử tối thiểu. Tất cả các công thức CTL có thể được chuyển đổi để chỉ sử dụng các toán tử đó. Điều này rất hữu ích trong việc kiểm tra mô hình. Một nhóm toán tử tối thiểu là: {true, ∨,, EG EU EX }.
Một số phép biến đổi được sử dụng cho toán tử tạm thời là:

EF φ == E [true U ( φ ]] (bởi vì ] φ == [true U ( φ )])

AX == ¬ EX φ )

AG φ == ¬ EF (¬ φ ) == ¬ đúng U (¬ φ )]

AF φ == A [true U ] == EG (¬ φ )

A [ φ U ψ ( E [(¬ ψ ) U ¬ ( φ ∨ ψ ] ∨ (¬ ))

Ngữ nghĩa của CTL [ chỉnh sửa ]

Định nghĩa [ ]]

Công thức CTL được diễn giải trên Hệ thống chuyển tiếp. Một hệ thống chuyển đổi là một bộ ba ${ displaystyle mathcal {M}} = (S, { rightarrow}, L)}$ trong đó ${ displaystyle S}$ là một tập hợp các trạng thái, ${displaystyle {rightarrow }subseteq Stimes S}$ là một mối quan hệ chuyển tiếp, được coi là nối tiếp, tức là mọi trạng thái đều có ít nhất một người kế vị và ${ displaystyle L}$ là một chức năng ghi nhãn, gán các chữ cái mệnh đề cho các trạng thái. Đặt ${ displaystyle { M}} = (S, rightarrow, L)}$ là một mô hình chuyển tiếp như vậy
với ${displaystyle sin S,phi in F}$ trong đó F là tập hợp của wffs trên ngôn ngữ của ${displaystyle {mathcal {M}}}$ .
Sau đó, mối quan hệ của ngữ nghĩa đòi hỏi ${ displaystyle ({ mathcal {M}}, s model phi)}$ được định nghĩa đệ quy trên ${ displaystyle phi}$ :

${ displaystyle { Big (} ({ mathcal {M} }, s) model top { Big)} đất { Big (} ({ mathcal {M}}, s) not model bot { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model p { Big)} Leftrightarrow { Big (} p in L ( s) { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model neg phi { Big )} Leftrightarrow { Big (} ({ mathcal {M}}, s) not model phi { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model phi _ {1} Land phi _ {2} { Big)} Leftrightarrow { Big (} { big (} ({ mathcal {M}}, s) model phi _ { 1} { big)} đất { big (} ({ mathcal {M}}, s) model phi _ {2} { big)} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model phi _ {1} lor phi _ {2} { Big)} Leftrightarrow { Big (} { big (} ({ mathcal {M}}, s) model phi _ { 1} { big)} lor { big (} ({ mathcal {M}}, s) model phi _ {2} { big)} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model phi _ {1} Rightarrow phi _ {2} { Big)} Leftrightarrow { Big (} { big (} ({ mathcal {M}}, s) not model phi _ {1} { big)} lor { big (} ({ mathcal {M}}, s) model phi _ {2} { big)} { Big)}}$

${ displaystyle { bigg (} ({ mathcal {M}}, s) model phi _ {1} Leftrightarrow phi _ {2} { bigg)} Lef trightarrow { bigg (} { Big (} { big (} ({ mathcal {M}}, s) model phi _ {1} { big)} đất { big (} ({ mathcal {M}}, s) model phi _ {2} { big)} { Big)} lor { Big (} neg { big (} ({ mathcal {M}}, s ) model phi _ {1} { big)} Land neg { big (} ({ mathcal {M}}, s) model phi _ {2} { big)} { Lớn )} { bigg)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model AX phi { Lớn)} Leftrightarrow { Big (} forall langle s rightarrow s_ {1} rangle { big (} ({ mathcal {M}}, s_ {1}) model phi { big )} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model EX phi { Lớn)} Leftrightarrow { Big (} tồn tại langle s rightarrow s_ {1} rangle { big (} ({ mathcal {M}}, s_ {1}) model phi { big )} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model AG phi { Big)} Leftrightarrow { Big (} forall langle s_ {1} rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) forall i { big (} ({ mathcal {M}}, s_ {i}) model phi { big)} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model EG phi { Big)} Leftrightarrow { Big (} tồn tại langle s_ {1} rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) forall i { big (} ({ mathcal {M}}, s_ {i}) model phi { big)} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model AF phi { Big)} Leftrightarrow { Big (} forall langle s_ {1} rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) tồn tại tôi { big (} ({ mathcal {M}}, s_ {i}) model phi { big)} { Big)}}$

${ displaystyle { Big (} ({ mathcal {M}}, s) model EF phi { Big)} Leftrightarrow { Big (} tồn tại langle s_ {1} rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) tồn tại i { big (} ({ mathcal {M}}, s_ {i}) model phi { big)} { Big)}}$

${ displaystyle { bigg (} ({ mathcal {M}}, s) model A [phi _{1}Uphi _{2}] { bigg)} Leftrightarrow { bigg (} forall langle s_ {1} rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) tồn tại tôi { Big (} { big (} ({ mathcal {M}}, s_ {i}) model phi _ {2} { big)} đất { big (} forall (j <i) ({ mathcal {M}}, s_ {j}) model phi _ {1} { big)} { Big)} { bigg)}}$

$<math > ( ( M s ) ⊨ E [ ϕ 1 U ϕ 2 ] ] ⇔ ( ∃ ⟨ s 1 → s 2 → Chèo ⟩ ( s = [19659418] s 1 ) ∃ i ( ( ( M [1965918] ) ⊨ ϕ 2 ) ∧ ( ∀ ( j [1965920i) ( M s j ) ⊨ ϕ 1 19659499]) { displaystyle { bigg (} ({ mathcal {M}}, s) model E [phi _{1}Uphi _{2}] { bigg)} Leftrightarrow { bigg (} tồn tại langle s_ {1 } rightarrow s_ {2} rightarrow ldots rangle (s = s_ {1}) tồn tại i { Big (} { big (} ({ mathcal {M}}, s_ {i}) model phi _ {2} { big)} đất { big (} forall (j <i) ({ mathcal {M}}, s_ {j}) model phi _ {1} { big )} { Big)} { bigg)}} <img src = "https: //wikierra.org/api/rest_v1/media/math/render/svg/0d04777cb8e0ba5d53918b4b64927615b6 fallback-image-inline "aria-hidden =" true "style =" vertical-align: -2.505ex; chiều rộng: 102.024ex; height: 6.176ex; "alt =" bigg (( mathcal {M}, s) model E [phi_1 U phi_2] bigg) Leftrightarrow bigg ( tồn tại langle s_1 rightarrow s_2 rightarrow ldots rangle ( s = s_1) tồn tại i Big ( big (( mathcal {M}, s_i) model phi_2 big) Land big ( forall (j < i) (mathcal{M}, s_j) models phi_1 big) Big) bigg)"/>$
Đặc tính của CTL [[19659888] chỉnh sửa ]

Quy tắc 10 Thay15 ở trên đề cập đến các đường dẫn tính toán trong các mô hình và cuối cùng là đặc trưng của "Cây tính toán"; chúng là những khẳng định về bản chất của cây tính toán sâu vô hạn bắt nguồn từ trạng thái đã cho ${ displaystyle s}$ .

Tương đương về ngữ nghĩa [ chỉnh sửa ]

Các công thức ${ displaystyle phi}$ ψ { displaystyle psi} $psi$ được cho là tương đương về mặt ngữ nghĩa nếu bất kỳ trạng thái nào trong bất kỳ mô hình nào thỏa mãn cái này cũng thỏa mãn cái kia. Điều này được ký hiệu là ${ displaystyle phi Equiv psi}$ .
Hơn nữa, G và F. cũng vậy.
Do đó, một thể hiện của Luật De Morgan có thể được xây dựng trong CTL:

${ displaystyle neg AF phi Equiv EG neg phi}$

${ displaystyle neg EF phi Equiv AG neg phi}$

${ displaystyle neg AX phi Equiv EX neg phi}$
Examples[edit]

Let "P" mean "I like chocolate" and Q mean "It's warm outside."

"I will like chocolate from now on, no matter what happens."
"It's possible I may like chocolate some day, at least for one day."
"It's always possible (AF) that I will suddenly start liking chocolate for the rest of time." (Note: not just the rest of my life, since my life is finite, while G is infinite).
"This is a critical time in my life. Depending on what happens next (E), it's possible that for the rest of time (G), there will always be some time in the future (AF) when I will like chocolate. However, if the wrong thing happens next, then all bets are off and there's no guarantee about whether I'll ever like chocolate."
The two following examples show the difference between CTL and CTL*, as they allow for the until operator to not be qualified with any path operator (A or E):

"From now until it's warm outside, I will like chocolate every single day. Once it's warm outside, all bets are off as to whether I'll like chocolate anymore. Oh, and it's guaranteed to be warm outside eventually, even if only for a single day."
"It's possible that: there will eventually come a time when it will be warm forever (AG.Q) and that before that time there will always be some way to get me to like chocolate the next day (EX.P)."
Relations with other logics[edit]

Computation tree logic (CTL) is a subset of CTL* as well as of the modal µ calculus. CTL is also a fragment of Alur, Henzinger and Kupferman's Alternating-time Temporal Logic (ATL).
Computation tree logic (CTL) and Linear temporal logic (LTL) are both a subset of CTL*. CTL and LTL are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL.

FG.P exists in LTL but not in CTL.

AG(P ${displaystyle Rightarrow }$ ((EX.Q) ${displaystyle land }$ (EX¬Q))) and AG.EF.P exist in CTL but not in LTL.
See also[edit]

References[edit]

E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic". Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131. Springer, Berlin: 52–71.

Michael Huth; Mark Ryan (2004). "Logic in Computer Science (Second Edition)". Cambridge University Press: 207. ISBN 0-521-54310-X.

Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.

Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.

Emerson, E. A. (1990). "Temporal and modal logic". In Jan van Leeuwen. Handbook of Theoretical Computer Science, vol. B. Báo chí MIT. pp. 955–1072. ISBN 0-262-22039-3.
External links[edit]