ตรรกะต้นไม้การคำนวณ (Computation Tree Logic หรือCTL ) เป็นตรรกะ แบบแตกแขนงตามเวลา หมายความว่าแบบจำลองเวลา ของมัน เป็น โครงสร้าง คล้ายต้นไม้ซึ่งอนาคตไม่ได้ถูกกำหนดไว้ล่วงหน้า มีเส้นทางที่แตกต่างกันในอนาคต ซึ่งแต่ละเส้นทางอาจเป็นเส้นทางที่เกิดขึ้นจริงได้ CTL ใช้ในการตรวจสอบอย่างเป็นทางการของซอฟต์แวร์หรือฮาร์ดแวร์ โดยทั่วไปแล้วจะใช้โดยโปรแกรมตรวจสอบแบบจำลอง ( model checker ) ซึ่งจะตรวจสอบว่าส่วนประกอบที่กำหนดนั้นมีคุณสมบัติด้านความปลอดภัยหรือความมีชีวิตชีวาหรือ ไม่ ตัวอย่างเช่น CTL สามารถระบุได้ว่าเมื่อเงื่อนไขเริ่มต้น บางอย่าง เป็นไปตามที่กำหนด (เช่น ตัวแปรโปรแกรมทั้งหมดเป็นค่าบวก หรือไม่มีรถบนทางหลวงคันใดวิ่งคร่อมสองเลน) การทำงานที่เป็นไปได้ทั้งหมดของโปรแกรมจะหลีกเลี่ยงเงื่อนไขที่ไม่พึงประสงค์บางอย่าง (เช่น การหารตัวเลขด้วยศูนย์ หรือรถสองคันชนกันบนทางหลวง) ในตัวอย่างนี้ คุณสมบัติด้านความปลอดภัยสามารถตรวจสอบได้โดยโปรแกรมตรวจสอบแบบจำลองที่สำรวจการเปลี่ยนสถานะที่เป็นไปได้ทั้งหมดจากสถานะของโปรแกรมที่ตรงตามเงื่อนไขเริ่มต้น และตรวจสอบให้แน่ใจว่าการทำงานทั้งหมดดังกล่าวเป็นไปตามคุณสมบัตินั้น ตรรกะต้นไม้การคำนวณจัดอยู่ในกลุ่มตรรกะเชิงเวลาซึ่งรวมถึงตรรกะเชิงเวลาเชิงเส้น  (LTL) แม้ว่าจะมีคุณสมบัติที่แสดงได้เฉพาะใน CTL และคุณสมบัติที่แสดงได้เฉพาะใน LTL แต่คุณสมบัติทั้งหมดที่แสดงได้ในตรรกะทั้งสองแบบก็สามารถแสดงในCTL ได้เช่นกัน *

CTL ถูกเสนอขึ้นครั้งแรกโดยEdmund M. ClarkeและE. Allen Emersonในปี 1981 ซึ่งพวกเขาใช้มันเพื่อสังเคราะห์สิ่งที่เรียกว่าโครงร่างการซิงโครไนซ์กล่าวคือนามธรรมของโปรแกรมแบบขนาน

นับตั้งแต่มีการนำ CTL มาใช้ มีการถกเถียงกันถึงข้อดีข้อเสียของ CTL และ LTL เนื่องจาก CTL มีประสิทธิภาพในการคำนวณมากกว่าในการตรวจสอบแบบจำลอง จึงเป็นที่นิยมใช้ในอุตสาหกรรมมากขึ้น และเครื่องมือตรวจสอบแบบจำลองที่ประสบความสำเร็จมากที่สุดหลายตัวใช้ CTL เป็นภาษากำหนดคุณสมบัติ^{[ 1 ]}

ภาษาของสูตรสำเร็จรูปสำหรับ CTL ถูกสร้างขึ้นโดยไวยากรณ์ต่อ ไปนี้ :

${\displaystyle {\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\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}}}$

โดยที่ครอบคลุมชุดของสูตรอะตอมไม่จำเป็นต้องใช้ตัวเชื่อมทั้งหมด – ตัวอย่างเช่น ประกอบด้วยชุดตัวเชื่อมที่สมบูรณ์ และตัวเชื่อมอื่นๆ สามารถกำหนดได้โดยใช้ตัวเชื่อมเหล่านั้น ${\displaystyle p}$${\displaystyle \{\neg ,\land ,{\mbox{AX}},{\mbox{AU}},{\mbox{EU}}\}}$

• ${\displaystyle {\mbox{A}}}$หมายถึง 'ตามเส้นทางทั้งหมด' (อย่างหลีกเลี่ยงไม่ได้)
• ${\displaystyle {\mbox{E}}}$หมายความว่า 'ตามเส้นทางอย่างน้อยหนึ่งเส้นทาง' (อาจจะ)

ตัวอย่างเช่น สูตร CTL ที่ถูกต้องมีรูปแบบดังต่อไปนี้:

${\displaystyle {\mbox{EF }}({\mbox{EG }}p\Rightarrow {\mbox{AF }}r)}$

สูตร CTL ต่อไปนี้ไม่ใช่สูตรที่ถูกต้อง:

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

ปัญหาของสตริงนี้คือมันจะเกิดขึ้นได้ก็ต่อเมื่อจับคู่กับหรือเท่านั้น ${\displaystyle \mathrm {U} }$${\displaystyle \mathrm {A} }$${\displaystyle \mathrm {E} }$

CTL ใช้ข้อเสนอเชิงอะตอมเป็นหน่วยพื้นฐานในการสร้างข้อความเกี่ยวกับสถานะของระบบ จากนั้นจึงนำข้อเสนอเหล่านี้มารวมกันเป็นสูตรโดยใช้ตัวดำเนินการเชิงตรรกะและ ตัวดำเนิน การ เชิงเวลา

ตัวดำเนินการทางตรรกะที่ใช้กันทั่วไป ได้แก่ ¬, ∨, ∧, ⇒ และ ⇔ นอกจากตัวดำเนินการเหล่านี้แล้ว สูตร CTL ยังสามารถใช้ค่าคงที่บูลีนtrueและfalseได้ อีกด้วย

ตัวดำเนินการเชิงเวลามีดังต่อไปนี้:

• ตัวบ่งปริมาณเหนือเส้นทาง
  • Φ – A ll: Φ ต้องเป็นจริงในทุกเส้นทางที่เริ่มต้นจากสถานะปัจจุบัน
  • E Φ – Eมีอยู่จริง: อย่างน้อยหนึ่งเส้นทางเริ่มต้นจากสถานะปัจจุบันที่ Φ เป็นจริง
• ตัวระบุปริมาณเฉพาะเส้นทาง
  • X φ  – Ne x t: φต้องเป็นจริงในสถานะถัดไป (ตัวดำเนินการนี้บางครั้งใช้สัญลักษณ์NแทนX )
  • G φ  – G lobally: φต้องคงอยู่ตลอดเส้นทางถัดไปทั้งหมด
  • F φ  – ในที่สุด: φจะต้องเป็นจริงในที่สุด (ในเส้นทางถัดไป)
  • φ U ψ  – จนกว่า : φจะต้องเป็นจริงอย่างน้อยจนกว่า ณ ตำแหน่งใดตำแหน่งหนึ่งψจะเป็นจริง ซึ่งหมายความว่าψจะได้รับการตรวจสอบในอนาคต
  • φ W ψ  – อ่อนจนกว่า: φต้องเป็นจริงจนกว่าψจะเป็นจริง ความแตกต่างจากUคือไม่มีการรับประกันว่าψจะได้รับการตรวจสอบเสมอไป ตัวดำเนินการ Wบางครั้งเรียกว่า "เว้นแต่"

ในCTL*ตัวดำเนินการเชิงเวลาสามารถผสมผสานกันได้อย่างอิสระ ใน CTL ตัวดำเนินการจะต้องถูกจัดกลุ่มเป็นคู่เสมอ กล่าวคือ ตัวดำเนินการเส้นทางหนึ่งตัว ตามด้วยตัวดำเนินการสถานะ ดูตัวอย่างด้านล่างCTL*มีความสามารถในการแสดงออกมากกว่า CTL อย่างชัดเจน

ใน CTL มีชุดตัวดำเนินการขั้นต่ำอยู่ชุดหนึ่ง สูตร CTL ทั้งหมดสามารถแปลงให้ใช้เฉพาะตัวดำเนินการเหล่านั้นได้ ซึ่งมีประโยชน์ในการตรวจสอบแบบจำลองชุดตัวดำเนินการขั้นต่ำชุดหนึ่งคือ: {true, ∨, ¬, EG , EU , EX }

การแปลงบางส่วนที่ใช้สำหรับตัวดำเนินการเชิงเวลา ได้แก่:

• EF φ == E [true U ( φ )] ( เนื่องจากF φ == [true U ( φ )] )
• AX φ == ¬ EX (¬ φ )
• AG φ == ¬ EF (¬ φ ) == ¬ E [true U (¬ φ )]
• AF φ == A [จริงU φ ] == ฌEG (‚ φ )
• A [ φ U ψ ] == ฌ( E [(‚ ψ ) Uฌ( φ ∨ ψ )] ∨ EG (ฌψ ) )

สูตร CTL ถูกตีความบนระบบการเปลี่ยนสถานะระบบการเปลี่ยนสถานะคือสามสิ่งโดยที่คือเซตของสถานะคือความสัมพันธ์การเปลี่ยนสถานะ ซึ่งถือว่าเป็นแบบอนุกรม กล่าวคือ ทุกสถานะมีผู้สืบทอดอย่างน้อยหนึ่งตัว และคือฟังก์ชันการติดป้าย ซึ่งกำหนดตัวอักษรเชิงประพจน์ให้กับสถานะ ให้เป็นแบบจำลองการเปลี่ยนสถานะดังกล่าว โดยที่และโดยที่คือเซตของสูตรที่สร้างขึ้นอย่างดี บนภาษาของ${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}$${\displaystyle S}$${\displaystyle {\rightarrow }\subseteq S\times S}$${\displaystyle L}$${\displaystyle {\mathcal {M}}=(S,\rightarrow ,L)}$${\displaystyle s\in S}$${\displaystyle \phi \in F}$${\displaystyle F}$${\displaystyle {\mathcal {M}}}$

จากนั้นความสัมพันธ์ของการอนุมาน เชิงความหมาย จะถูกกำหนดแบบเวียนซ้ำบน: ${\displaystyle ({\mathcal {M}},s\models \phi )}$${\displaystyle \phi }$

1. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \top {\Big )}\land {\Big (}({\mathcal {M}},s)\not \models \bot {\Big )}}$
2. ${\displaystyle {\Big (}({\mathcal {M}},s)\models p{\Big )}\Leftrightarrow {\Big (}p\in L(s){\Big )}}$
3. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \neg \phi {\Big )}\Leftrightarrow {\Big (}({\mathcal {M}},s)\not \models \phi {\Big )}}$
4. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
7. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}{\bigg )}}$
8. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
10. ${\displaystyle {\Big (}({\mathcal {M}},s)\models 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})\models \phi {\big )}{\Big )}}$
11. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
12. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
13. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
14. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$
15. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$

กฎข้อ 10–15 ข้างต้นอ้างถึงเส้นทางการคำนวณในแบบจำลอง และเป็นสิ่งที่กำหนดลักษณะเฉพาะของ "ต้นไม้การคำนวณ" ในที่สุด โดยเป็นการยืนยันเกี่ยวกับธรรมชาติของต้นไม้การคำนวณที่มีความลึกไม่สิ้นสุดซึ่งมีรากฐานอยู่ที่สถานะที่กำหนด ${\displaystyle s}$

สูตรและจะถือว่ามีความหมายเทียบเท่ากัน หากสถานะใดๆ ในแบบจำลองใดๆ ที่สอดคล้องกับสูตรหนึ่ง ก็จะสอดคล้องกับอีกสูตรหนึ่งด้วย ซึ่งจะใช้สัญลักษณ์แทนด้วย${\displaystyle \phi }$${\displaystyle \psi }$${\displaystyle \phi \equiv \psi }$

จะเห็นได้ว่าและเป็นคู่กัน โดยเป็นตัวบ่งปริมาณเส้นทางการคำนวณแบบสากลและแบบมีอยู่จริงตามลำดับ: . ${\displaystyle \mathrm {A} }$${\displaystyle \mathrm {E} }$${\displaystyle \neg \mathrm {A} \Phi \equiv \mathrm {E} \neg \Phi }$

นอกจากนี้ และ ก็เช่น กัน${\displaystyle \mathrm {G} }$${\displaystyle \mathrm {F} }$

ดังนั้น ตัวอย่างหนึ่งของกฎของเดอ มอร์แกนสามารถกำหนดได้ใน 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 }$

สามารถแสดงให้เห็นได้โดยใช้เอกลักษณ์ดังกล่าวว่า เซตย่อยของตัวเชื่อมเวลา CTL นั้นเหมาะสม หากประกอบด้วยอย่างน้อยหนึ่งตัวจากและอย่างน้อยหนึ่งตัวจากและตัวเชื่อมบูลีน ${\displaystyle EU}$${\displaystyle \{AX,EX\}}$${\displaystyle \{EG,AF,AU\}}$

ความเท่าเทียมกันที่สำคัญด้านล่างนี้เรียกว่ากฎการขยายตัวซึ่งช่วยให้สามารถตรวจสอบความถูกต้องของตัวเชื่อมต่อ CTL ไปสู่ตัวเชื่อมต่อรุ่นต่อๆ ไปในเวลาได้

${\displaystyle AG\phi \equiv \phi \land AXAG\phi }$

${\displaystyle EG\phi \equiv \phi \land EXEG\phi }$

${\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

${\displaystyle EF\phi \equiv \phi \lor EXEF\phi }$

${\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])}$

ให้ "P" หมายถึง "ฉันชอบช็อกโกแลต" และ "Q" หมายถึง "อากาศข้างนอกอบอุ่น"

• เอจีพี

"นับจากนี้ไป ฉันจะชอบช็อกโกแลต ไม่ว่าอะไรจะเกิดขึ้นก็ตาม"

• อีเอฟ .พี

"เป็นไปได้ว่าสักวันฉันอาจจะชอบช็อกโกแลต อย่างน้อยก็สักวันหนึ่ง"

• AF . EG .P

"เป็นไปได้เสมอ (AF) ที่ฉันจะเริ่มชอบช็อกโกแลตไปตลอดกาล" (หมายเหตุ: ไม่ใช่แค่ตลอดชีวิตของฉัน เพราะชีวิตของฉันมีจำกัด ในขณะที่Gนั้นไม่มีที่สิ้นสุด)

• EG . AF .P

"ขึ้นอยู่กับว่าจะเกิดอะไรขึ้นในอนาคต (E) เป็นไปได้ว่าตลอดช่วงเวลาที่เหลือ (G) ฉันจะได้รับการรับประกันว่าจะมีอย่างน้อยหนึ่งวัน (AF) ที่ฉันชอบช็อกโกแลตอยู่ข้างหน้า อย่างไรก็ตาม หากมีอะไรผิดพลาดเกิดขึ้น ทุกอย่างก็พลิกผัน และไม่มีอะไรรับประกันได้ว่าฉันจะชอบช็อกโกแลตอีกหรือไม่"

ตัวอย่างสองข้อต่อไปนี้แสดงให้เห็นถึงความแตกต่างระหว่าง CTL และ CTL* เนื่องจากอนุญาตให้ตัวดำเนินการ until ไม่จำเป็นต้องระบุคุณสมบัติเพิ่มเติมด้วยตัวดำเนินการเส้นทางใดๆ ( AหรือE ):

• AG (P U Q)

"นับจากนี้ไปจนกว่าอากาศจะอุ่นขึ้น ฉันจะกินช็อกโกแลตทุกวัน พออากาศอุ่นขึ้นแล้ว ฉันก็ไม่แน่ใจแล้วว่าจะยังชอบช็อกโกแลตอยู่ไหม อ้อ และรับรองได้เลยว่าอากาศจะอุ่นขึ้นในที่สุด ถึงแม้จะเป็นแค่เพียงวันเดียวก็ตาม"

• EF (( EX .P) U ( AG .Q))

"เป็นไปได้ว่า: ในที่สุดจะมีช่วงเวลาหนึ่งที่อากาศจะอบอุ่นตลอดไป (AG.Q) และก่อนถึงเวลานั้น จะมี วิธี ใด วิธีหนึ่ง ที่จะทำให้ฉันชอบช็อกโกแลตในวันรุ่งขึ้นเสมอ (EX.P)"

ตรรกะต้นไม้การคำนวณ (CTL) เป็นส่วนย่อยของ CTL* เช่นเดียวกับแคลคูลัสโมดอล μ นอกจากนี้ CTL ยังเป็นส่วนหนึ่งของ ตรรกะเชิงเวลาแบบสลับเวลา (ATL) ของ Alur, Henzinger และ Kupferman อีกด้วย

ตรรกะต้นไม้การคำนวณ (CTL) และตรรกะเชิงเวลาเชิงเส้น (LTL) ต่างก็เป็นเซตย่อยของ CTL* CTL และLTLไม่เท่ากัน และมีเซตย่อยร่วมกัน ซึ่งเป็นเซตย่อยที่แท้จริงของทั้ง CTL และ LTL

• FG .P มีอยู่ใน LTL แต่ไม่มีอยู่ใน CTL
• AG (P⇒(( EX .Q)∧( EX ¬Q))) และAG.EF .P มีอยู่ใน CTL แต่ไม่มีอยู่ใน LTL

CTL ได้รับการขยายด้วยการกำหนดปริมาณลำดับที่สองและตรรกะต้นไม้การคำนวณเชิงปริมาณ (QCTL) ^{[ 2 ]}มีความหมายสองแบบ: ${\displaystyle \exists p}$${\displaystyle \forall p}$

• ความหมายของต้นไม้ เราติดป้ายกำกับโหนดของต้นไม้การคำนวณ QCTL* = QCTL = MSOบนต้นไม้ การตรวจสอบแบบจำลองและความสามารถในการทำให้เป็นจริงนั้นสมบูรณ์แบบในเชิงต้นไม้
• ความหมายของโครงสร้าง เรากำหนดป้ายกำกับให้กับสถานะ QCTL* = QCTL = MSO บนกราฟการตรวจสอบแบบจำลองนั้นสมบูรณ์แบบ PSPACEแต่ความสามารถในการทำให้เป็นจริงนั้นไม่สามารถตัดสินได้

มีการเสนอการลดปัญหาการตรวจสอบแบบจำลองของ QCTL ด้วยความหมายเชิงโครงสร้าง ไปสู่ ​​TQBF (สูตรบูลีนเชิงปริมาณที่แท้จริง) เพื่อใช้ประโยชน์จากตัวแก้ปัญหา QBF ^{[ 3 ]}

• CTL เชิงความน่าจะเป็น
• ตรรกะต้นไม้การคำนวณที่เป็นธรรม
• ตรรกะเชิงเวลาเชิงเส้น

• สไลด์ประกอบการสอนของ CTL