ในการตรวจสอบแบบจำลอง (model checking ) ตรรกะเชิงเวลาแบบช่วงเวลาเมตริก (Metric Interval Temporal Logicหรือ MITL) เป็นส่วนหนึ่งของตรรกะเชิงเวลาเมตริก (Metric Temporal Logicหรือ MTL) ส่วนย่อยนี้มักได้รับความนิยมมากกว่า MTL เนื่องจากปัญหาบางอย่างที่ไม่สามารถตัดสินได้ด้วย MTL กลับสามารถตัดสินได้ด้วย MITL

สูตร MITL คือสูตร MTL ​​ซึ่งแต่ละเซตของจำนวนจริงที่ใช้ในตัวห้อยเป็นช่วงที่ไม่ใช่เซตที่มีสมาชิกเพียงตัวเดียว และขอบเขตของช่วงเหล่านั้นเป็นจำนวนธรรมชาติหรือเป็นอนันต์

MTL สามารถแสดงข้อความเช่นประโยคS ได้ ว่า " Pถูกถือครองเมื่อ 10 หน่วยเวลาที่ผ่านมา" ซึ่งเป็นไปไม่ได้ใน MITL MITL สามารถแสดงได้เพียงTว่า " Pถูกถือครองระหว่าง 9 ถึง 10 หน่วยเวลาที่ผ่านมา" เนื่องจาก MITL สามารถแสดงT ได้ แต่ไม่สามารถแสดง S ได้ดังนั้นในแง่หนึ่ง MITL จึงเป็นข้อจำกัดของ MTL ที่อนุญาตให้แสดงข้อความที่มีความแม่นยำน้อยกว่าเท่านั้น

เหตุผลหนึ่งที่ควรหลีกเลี่ยงประโยคอย่างS ก็ คือค่าความจริง ของประโยคนี้ อาจเปลี่ยนแปลงได้หลายครั้งในช่วงเวลาหนึ่งหน่วย ที่จริงแล้ว ค่าความจริงของประโยคนี้อาจเปลี่ยนแปลงได้มากเท่ากับค่าความจริงของPและPเองก็อาจเปลี่ยนแปลงได้หลายครั้งในช่วงเวลาหนึ่งหน่วยเช่นกัน

ต่อไปนี้เราจะพิจารณาระบบ เช่นออโตมาตาแบบกำหนดเวลาหรือออโตมาตาแบบส่งสัญญาณซึ่งต้องการทราบว่าเงื่อนไขSเป็นจริงหรือไม่ในแต่ละขณะ ระบบนี้จะต้องจดจำทุกสิ่งที่เกิดขึ้นในช่วง 10 หน่วยเวลาที่ผ่านมา ดังที่เห็นข้างต้น หมายความว่าระบบจะต้องจดจำเหตุการณ์จำนวนมากอย่างไม่จำกัด ซึ่งระบบที่มีหน่วยความจำและนาฬิกาจำกัดไม่สามารถทำได้

ข้อดีหลักอย่างหนึ่งของ MITL คือ ตัวดำเนินการแต่ละตัวมีคุณสมบัติความแปรผันที่จำกัด ตัวอย่างเช่น:

กำหนดให้ข้อความTนิยามไว้ข้างต้น ทุกครั้งที่ค่าความจริงของTเปลี่ยนจากเท็จเป็นจริง มันจะยังคงเป็นจริงอย่างน้อยหนึ่งหน่วยเวลา พิสูจน์: ณ เวลาtที่Tกลายเป็นจริง หมายความว่า:

• เมื่อประมาณ 9 ถึง 10 หน่วยเวลาที่ผ่านมาPเป็นจริง
• ก่อนเวลาtเล็กน้อยPเป็นเท็จ

ดังนั้นPจึงเป็นจริงเมื่อ 9 หน่วยเวลาที่ผ่านมาพอดี จึงสรุปได้ว่า สำหรับแต่ละค่า ที่เวลาP ก็เป็นจริงเมื่อ หน่วยเวลาที่ผ่านมาเช่นกัน เนื่องจากที่เวลาT จึงเป็นจริง ${\displaystyle t'\in [0,1]}$${\displaystyle t+t'}$${\displaystyle 9+t'}$${\displaystyle 9+t'\in [9,10]}$${\displaystyle t'}$

ระบบต้องการทราบค่าของT ในแต่ละขณะ ระบบดังกล่าวต้องจดจำสิ่งที่เกิดขึ้นในช่วงสิบหน่วยเวลาที่ผ่านมา อย่างไรก็ตาม ด้วยคุณสมบัติความแปรปรวนที่จำกัด ระบบจะต้องจดจำได้มากที่สุด 10 หน่วยเวลาเมื่อTเป็นจริง และ 11 ครั้งเมื่อTเป็นเท็จ ดังนั้น ระบบนี้ต้องจดจำเหตุการณ์ได้มากที่สุด 21 เหตุการณ์ และด้วยเหตุนี้จึงสามารถนำไปใช้ในรูปแบบของออโตมาตาแบบกำหนดเวลาหรือออโตมาตาแบบส่งสัญญาณได้

ตัวอย่างสูตร MITL:

• ${\displaystyle \square \diamond _{(0,1)}p}$ระบุว่าตัวอักษรนั้นต้องปรากฏอย่างน้อยหนึ่งครั้งในแต่ละช่วงว่างที่มีความยาว 1${\displaystyle p}$
• ${\displaystyle \triangleright _{\{i\}}p}$ตัวดำเนินการพยากรณ์ถูกกำหนดไว้อย่างไรและระบุว่าการเกิดขึ้นครั้งแรกของในอนาคตจะอยู่ในหน่วยเวลาใด${\displaystyle \triangleright _{\{i\}}p}$${\displaystyle \square _{(0,i)}\neg p\land \diamond _{(0,i]}p}$${\displaystyle p}$${\displaystyle i}$
• ${\displaystyle p\land \square (p\implies \triangleright _{\{1\}}p)}$ระบุว่าข้อความนี้เป็นจริงอย่างแน่นอน ณ เวลาจำนวนเต็มแต่ละเวลา และไม่เป็นจริงในเวลาอื่นใด${\displaystyle p}$

ส่วนย่อยSafety-MTL ถูกกำหนดให้เป็นเซตย่อยของ MITL ที่มีเฉพาะสูตรในรูปแบบปกติบวกโดยที่ช่วงเวลาของตัวดำเนินการ until ทุกตัวมีขอบเขตบน ตัวอย่างเช่น สูตรที่ระบุว่าแต่ละตามมาด้วย ในเวลาน้อยกว่าหนึ่งหน่วยเวลาถือเป็นตรรกะนี้^{[ 1 ]}${\displaystyle \Box (a\implies \Diamond _{(0,1]}b)}$${\displaystyle a}$${\displaystyle b}$

ส่วนประกอบOpen-MTLประกอบด้วยสูตรในรูปแบบปกติเชิงบวกดังนี้:

• สำหรับแต่ละรายการนั้นเปิดอยู่ และ${\displaystyle {\คณิตศาสตร์ {U}__{I}}$${\displaystyle I}$
• สำหรับแต่ละอันจะปิดลง${\displaystyle {\คณิตศาสตร์ {R}__{I}}$${\displaystyle I}$

ส่วนประกอบClosed-MITLประกอบด้วยการปฏิเสธของสูตรในOpen- MITL

ส่วนประกอบFlat-MTLประกอบด้วยสูตรในรูปแบบปกติเชิงบวกดังนี้:

• สำหรับแต่ละค่าถ้าไม่มีขอบเขตจำกัด แล้วจะเป็นสูตร LTL${\displaystyle \phi _{1}{\คณิตศาสตร์ {U}__{I}\phi _{2}}$${\displaystyle I}$${\displaystyle \phi _{1}}$
• สำหรับแต่ละค่าถ้าไม่มีขอบเขตจำกัด แล้วจะเป็นสูตร LTL${\displaystyle \phi _{1}{\คณิตศาสตร์ {R}__{I}\phi _{2}}$${\displaystyle I}$${\displaystyle \phi _{2}}$

ส่วนประกอบCoflat-MITLประกอบด้วยการปฏิเสธของสูตรในFlat- MITL

เมื่อกำหนดส่วนย่อยL ใดๆ ส่วนย่อยL ^nsคือการจำกัดของLโดยใช้เฉพาะตัวดำเนินการที่ ไม่เข้มงวด เท่านั้น

สำหรับเศษส่วนL ใดๆ เศษส่วนL คือเซตย่อยของLที่ขอบล่างของแต่ละช่วงเป็น 0 หรือขอบบนเป็นอนันต์ ในทำนองเดียวกัน เราใช้สัญลักษณ์L (และL ตามลำดับ ) แทนเซตย่อยของLที่ขอบล่างของแต่ละช่วงเป็น 0 (และขอบบนของแต่ละช่วงเป็น ∞ ตามลำดับ)

เมื่อพิจารณาสัญญาณ MITL จะแสดงออกได้มากเท่ากับ MITL ซึ่งสามารถพิสูจน์ได้โดยการใช้กฎการเขียนใหม่ต่อไปนี้กับสูตร MITL ^{[ 2 ]}

• ${\displaystyle \phi {\mathcal {U}__{(a,b)}\psi }$เทียบเท่ากับ(การสร้างช่วงครึ่งปิดและช่วงปิดนั้นคล้ายกัน)${\displaystyle \Box _{(0,a]}\phi {\mathcal {U}}\psi \land \Diamond _{(a,b)}\psi }$
• ${\displaystyle \Diamond _{(a,b)}\phi }$เทียบเท่ากับถ้า${\displaystyle \Diamond _{(2a-b,a)}\Box _{(0,ba)}\Diamond _{(0,ba)}\phi }$${\displaystyle 2a-b\geq 0}$
• ${\displaystyle \Diamond _{(a,b)}\phi }$เทียบเท่ากับถ้า${\displaystyle \Diamond _{(a,ba)}\Diamond _{(0,a)}\phi }$${\displaystyle a<b}$
• ${\displaystyle \Diamond _{(a,+\infty )}\phi }$เทียบเท่ากับ.${\displaystyle \Box _{(0,a)}\Diamond \phi }$

การใช้กฎการเขียนใหม่เหล่านั้นจะทำให้ขนาดของสูตรเพิ่มขึ้นอย่างมาก ที่จริงแล้ว ตัวเลขและนั้นโดยทั่วไปเขียนในรูปแบบเลขฐานสอง และควรใช้กฎเหล่านั้นซ้ำกันหลายครั้ง ${\displaystyle a}$${\displaystyle b}$${\displaystyle O\left({\frac {b}{ba}}\right)}$

ตรงกันข้ามกับกรณีของสัญญาณ MITL มีความสามารถในการแสดงออกมากกว่า MITL อย่างเคร่งครัด กฎการเขียนใหม่ที่กล่าวมาข้างต้นใช้ไม่ได้กับกรณีของคำที่มีเวลา เพราะในการเขียนใหม่นั้นต้องมีสมมติฐานว่าเหตุการณ์บางอย่างเกิดขึ้นระหว่างเวลา 0 และ∞ ซึ่งไม่จำเป็นต้องเป็นเช่นนั้นเสมอไป ${\displaystyle \Diamond _{(a,b)}}$${\displaystyle a}$

ปัญหาในการตัดสินใจว่าสูตร MITL สามารถทำให้เป็นจริงได้หรือไม่บนสัญญาณนั้นเป็นปัญหาEXPSPACE-completeในขณะที่ความสามารถในการทำให้เป็นจริงสำหรับ MITL เป็นปัญหาPSPACE-complete ^{[ 3 ]}

R. Alur, T. Feder และ TA Henzinger. ประโยชน์ของการผ่อนคลายความตรงต่อเวลาวารสาร ACM , 43(1):116–146, 1996. R. Alur และ TA Henzinger. ตรรกะและแบบจำลองของเรียลไทม์: การสำรวจ ใน Proc. REX Workshop, Real-time: Theory in Practice, หน้า 74–106. LNCS 600, Springer, 1992. TA Henzinger. ถึงเวลาแล้ว: การทบทวนตรรกะเรียลไทม์ ใน Proc. CONCUR'98, หน้า 439–454. LNCS 1466, Springer, 1998.