ตรรกะเชิงเวลาของช่วงเวลาเมตริก

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

คำนิยาม

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

ความแตกต่างจาก MTL

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

ปัญหาที่ MITL หลีกเลี่ยง

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

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

ความแปรผันที่มีขอบเขต

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

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

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

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

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

ตัวอย่าง

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

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

ชิ้นส่วน

ความปลอดภัย-MTL

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

MITL แบบเปิดและปิด

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

สำหรับแต่ละคน ${\คณิตศาสตร์ {U}__{I}$ , $I$ เปิดแล้ว และ
สำหรับแต่ละคน ${\คณิตศาสตร์ {R}__{I}$ , $I$ ปิดทำการแล้ว

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

แฟลตและโคแฟลต MITL

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

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

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

รูปแบบที่ไม่เข้มงวด

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

MITL และ MITL

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

การแสดงออกผ่านสัญญาณ

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

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

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

การแสดงออกผ่านคำพูดที่กำหนดเวลาไว้

ตรงกันข้ามกับกรณีของสัญญาณ MITL มีความสามารถในการแสดงออกมากกว่า MITL อย่างชัดเจน กฎการเขียนใหม่ที่กล่าวมาข้างต้นใช้ไม่ได้กับกรณีของคำที่มีเวลา เนื่องจากในการเขียนใหม่ $\Diamond _{(a,b)}$ ข้อสันนิษฐานคือต้องมีเหตุการณ์บางอย่างเกิดขึ้นระหว่างเวลา 0 และ $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.

[ 1 ]

[ 2 ]

[ 3 ]