ในด้านการตรวจสอบแบบจำลองซึ่งเป็นสาขาหนึ่งของวิทยาศาสตร์คอมพิวเตอร์ตรรกะเชิงเวลาแบบประพจน์ที่มีเวลา ( TPTL ) เป็นส่วนขยายของตรรกะเชิงเวลาเชิงเส้นแบบ ประพจน์ (LTL) โดยมีการนำตัวแปรมาใช้ในการวัดช่วงเวลาระหว่างสองเหตุการณ์ ตัวอย่างเช่น ในขณะที่ LTL อนุญาตให้ระบุว่าแต่ละเหตุการณ์pจะตามมาด้วยเหตุการณ์q ในที่สุด TPTL ยังอนุญาตให้กำหนดขีดจำกัดเวลาสำหรับการเกิดขึ้นของ q ได้อีกด้วย

ส่วนประกอบในอนาคตของ TPTLถูกกำหนดในลักษณะเดียวกับตรรกะเชิงเวลาเชิงเส้นซึ่งนอกจากนี้ ยัง สามารถแนะนำตัวแปร นาฬิกา และเปรียบเทียบกับค่าคงที่ได้ ในทางทฤษฎีแล้ว MTLสร้างขึ้นจาก ชุดของนาฬิกา :${\displaystyle X}$

• เซตจำกัดของ ตัวแปร เชิงประพจน์AP
• ตัวดำเนินการตรรกะ ¬ และ ∨ และ
• ตัวดำเนินการโมดอลเชิงเวลาU ,
• การเปรียบเทียบนาฬิกาโดยใช้ตัวเลขและตัวดำเนินการเปรียบเทียบ เช่น <, ≤, =, ≥ หรือ >${\displaystyle x\sim c}$${\displaystyle x\in X}$${\displaystyle c}$${\displaystyle \sim }$
• ตัวดำเนินการหาปริมาณแบบแช่แข็งสำหรับสูตร TPTL ที่มีชุดนาฬิกา${\displaystyle x.\phi }$${\displaystyle \phi }$${\displaystyle X\cup \{x\}}$

นอกจากนี้ สำหรับช่วงเวลาหนึ่งๆถือว่าเป็นตัวย่อของ; และในทำนองเดียวกันสำหรับช่วงเวลาประเภทอื่นๆ ทุกประเภท ${\displaystyle I=(a,b)}$${\displaystyle x\in I}$${\displaystyle x>a\land x<b}$

ตรรกะTPTL+Past ^{[ 1 ]}ถูกสร้างขึ้นเป็นเศษส่วนในอนาคตของTLSและยังประกอบด้วย

• ตัวดำเนินการโมดอลเชิงเวลาS

ตัวดำเนินการถัดไปNไม่ถือว่าเป็นส่วนหนึ่งของ ไวยากรณ์ MTLแต่จะถูกกำหนดจากตัวดำเนินการอื่นๆ แทน

สูตรปิดคือสูตรบนเซตนาฬิกา ที่ว่างเปล่า ^{[ 2 ]}

ให้แทนเซตของเวลาโดยสัญชาตญาณ ให้ เป็นฟังก์ชันที่เชื่อมโยงแต่ละช่วงเวลากับเซตของข้อความจากAPแบบจำลองของสูตร TPTL คือฟังก์ชันดังกล่าวโดยปกติจะเป็นคำหรือสัญญาณ ที่มีเวลา ในกรณีเหล่านั้นจะเป็นเซตย่อยแบบไม่ต่อเนื่องหรือช่วงที่มีค่า 0 อยู่ ${\displaystyle T\subseteq \mathbb {R} _{+}}$${\displaystyle \gamma :T\to {\mathcal {P}}(AP)}$${\displaystyle t\in T}$${\displaystyle \gamma }$${\displaystyle \gamma }$${\displaystyle T}$

ให้และเป็นไปตามที่กล่าวมาข้างต้น ให้เป็นเซตของนาฬิกาให้( การประเมินค่านาฬิกาเหนือ) ${\displaystyle T}$${\displaystyle \gamma }$${\displaystyle X}$${\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}$${\displaystyle X}$

ต่อไปนี้เราจะอธิบายว่าสูตร TPTL เป็นจริง ณ เวลาใดเวลาหนึ่งสำหรับการประเมินค่า หมายความว่าอย่างไร ซึ่งเราจะ ใช้สัญลักษณ์ แทนด้วยให้และเป็นสองสูตรบนเซตของนาฬิกาเป็นสูตรบนเซตของนาฬิกา, , , เป็นตัวเลข และเป็นตัวดำเนินการเปรียบเทียบ เช่น <, ≤, =, ≥ หรือ >: เราจะพิจารณาสูตรที่มีตัวดำเนินการหลักอยู่ใน LTL ก่อน: ${\displaystyle \phi }$${\displaystyle t}$${\displaystyle \nu }$${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \phi }$${\displaystyle \psi }$${\displaystyle X}$${\displaystyle \xi }$${\displaystyle X\cup \{y\}}$${\displaystyle x\in X}$${\displaystyle l\in {\mathtt {AP}}}$${\displaystyle c}$${\displaystyle \sim }$

• ${\displaystyle \gamma ,t,\nu \models l}$เป็นจริงถ้า,${\displaystyle l\in \gamma (t)}$
• ${\displaystyle \gamma ,t,\nu \models \neg \phi }$ถือไว้หาก${\displaystyle \gamma ,t,\nu \not \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \lor \psi }$เป็นจริงหากเงื่อนไขใดเงื่อนไขหนึ่งหรือทั้งสอง เงื่อนไขเป็นจริง${\displaystyle \gamma ,t,\nu \models \phi }$${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi }$เป็นจริงก็ต่อเมื่อมีอยู่ซึ่งและและสำหรับแต่ละโดยที่,   ,${\displaystyle t''}$${\displaystyle t<t''}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t'}$${\displaystyle t<t'<t''}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {S}} \psi }$เป็นจริงก็ต่อเมื่อมีอยู่ซึ่งและและสำหรับแต่ละโดยที่ ,   ,${\displaystyle t''}$${\displaystyle t''<t}$${\displaystyle \gamma ,t'',\nu \models \psi }$${\displaystyle t'}$${\displaystyle t''<t'<t}$${\displaystyle \gamma ,t',\nu \models \phi }$
• ${\displaystyle \gamma ,t,\nu \models x\sim c}$เป็นจริงถ้า,${\displaystyle t-\nu (y)\sim c}$
• ${\displaystyle \gamma ,t,\nu \models y.\xi }$คงอยู่ถ้าคงอยู่${\displaystyle \gamma ,t,\nu [y\to t]\models \phi }$

ตรรกะเชิงเวลาแบบเมตริก เป็นส่วนขยายอีกอย่างหนึ่งของ LTL ที่ช่วยให้สามารถวัดเวลา ได้แทนที่จะบวกตัวแปร มันจะบวกตัวดำเนินการจำนวนอนันต์สำหรับช่วงของจำนวนที่ไม่เป็นลบ ความหมายของสูตรณ เวลาใดเวลาหนึ่งนั้นโดยพื้นฐานแล้วเหมือนกับความหมายของสูตรโดยมีข้อจำกัดว่าเวลาที่ สูตรนี้ต้องเป็นจริงนั้นเกิด ขึ้น ในช่วง${\displaystyle {\mathcal {U}}_{I}}$${\displaystyle {\mathcal {S}}_{I}}$${\displaystyle I}$${\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }$${\displaystyle t}$${\displaystyle \phi \mathbin {\mathcal {U}} \psi }$${\displaystyle t''}$${\displaystyle \psi }$${\displaystyle t+I}$

TPTL มีความสามารถในการแสดงออกอย่างน้อยเท่ากับ MTL อันที่จริง สูตร MTL ​​เทียบเท่ากับสูตร TPTL โดยที่เป็นตัวแปรใหม่^{[ 2 ]}${\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi }$${\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )}$${\displaystyle x}$

ดังนั้น ตัวดำเนินการอื่นๆ ที่แนะนำในหน้าMTLเช่นและก็สามารถกำหนดให้เป็นสูตร TPTL ได้เช่นกัน ${\displaystyle \Box }$${\displaystyle \Diamond }$

TPTL มีความสามารถในการแสดงออกมากกว่า MTL อย่างชัดเจน^{[ 1 ] : 2} ทั้งในส่วนของคำที่กำหนดเวลาและสัญญาณ ในส่วนของคำที่กำหนดเวลา ไม่มีสูตร MTL ​​ใดเทียบเท่ากับในส่วนของสัญญาณ ไม่มีสูตร MTL ​​ใดเทียบเท่ากับซึ่งระบุว่าข้อเสนออะตอมสุดท้ายก่อนจุดเวลา 1 คือ ${\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))}$${\displaystyle x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))}$${\displaystyle a}$

คำอนันต์มาตรฐาน (ไม่จำกัดเวลา) คือฟังก์ชันจากไปยังเราสามารถพิจารณาคำดังกล่าวโดยใช้เซตของเวลาและฟังก์ชันในกรณีนี้ สำหรับสูตร LTL ใดๆ ก็ต่อเมื่อโดยที่ถือเป็นสูตร TPTL ที่มีตัวดำเนินการแบบไม่เข้มงวด และเป็นฟังก์ชันเดียวที่กำหนดบนเซตว่าง ${\displaystyle w=a_{0},a_{1},\dots ,}$${\displaystyle \mathbb {N} }$${\displaystyle A}$${\displaystyle T=\mathbb {N} }$${\displaystyle \gamma (i)=a_{i}}$${\displaystyle \phi }$${\displaystyle w,i\models \phi }$${\displaystyle \gamma ,i,\nu \models \phi }$${\displaystyle \phi }$${\displaystyle \nu }$