核心概念
單變量時間命題時序邏輯 (TPTL) 中即使放寬時間約束至僅允許開放時間區間,其滿足性判定問題仍然十分困難,這突顯了研究非相鄰時間約束的重要性,並引出部分相鄰 TPTL 作為一個更具表達能力的可判定時間邏輯子類。
本論文探討了單變量時間命題時序邏輯 (TPTL) 中時間約束放寬至開放時間區間後的滿足性判定問題,並提出部分相鄰 TPTL 作為一個新的可判定時間邏輯子類。
研究背景
度量時序邏輯 (MTL) 和時間命題時序邏輯 (TPTL) 是線性時序邏輯 (LTL) 的兩種重要實時擴展。MTL 通過引入時間區間約束來擴展 LTL 的 Until 和 Since 模態算子,而 TPTL 則通過實值凍結量詞和對這些凍結變量的約束來實現同樣的目的。
開放性 TPTL 的不可判定性
論文首先研究了僅允許在拓撲開放時間區間內指定屬性的受限 TPTL 片段,稱為開放 TPTL (OpTPTL1)。儘管開放性比非間斷性更具限制性,但論文證明即使在這種限制下,OpTPTL1 的滿足性判定問題仍然與 1-TPTL 一樣困難,即在無限字上不可判定,在有限字上具有非原始遞歸下界。
部分相鄰 TPTL 的可判定性
論文進一步提出了部分相鄰性的概念,將非相鄰性的概念推廣到僅允許在過去或將來(而非兩個方向)存在相鄰時間約束。論文證明了部分相鄰的單變量 TPTL (PA-1-TPTL) 在有限時間字上是可判定的,並且它比 PMTL 更具表達能力,使其成為文獻中已知表達能力最強的可判定布爾封閉時間邏輯。
研究意義
本論文的研究結果表明,放鬆時間約束至開放時間區間並不能簡化單變量 TPTL 的滿足性判定問題,這突顯了研究非相鄰時間約束的重要性。同時,論文提出的部分相鄰 TPTL 為設計更具表達能力的可判定時間邏輯提供了新的思路。