Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) extend Linear Temporal Logic (LTL) for real-time constraints, with MTL using time-bounded modalities and TPTL employing freeze quantifiers. Satisfiability for both is generally undecidable; however, MTL becomes decidable under certain non-punctual and partially-punctual restrictions. Punctuality can be restored trivially under similar non-punctual restrictions on TPTL even for one variable fragment. Our first contribution is to study more restricted notion of openness for 1-TPTL, under which punctuality can not be recovered. We show that even under such restrictions, the satisfiability checking does not get computationally easier. This implies that 1-TPTL (and hence TPTL) does not enjoy benefits of relaxing punctuality unlike MTL. As our second contribution we introduce a refined, partially adjacent restriction in 1-TPTL (PA-1-TPTL), and prove decidability for its satisfiability checking. We show that this logic is strictly more expressive than partially punctual Metric Temporal Logic, making this as one of the most expressive known boolean-closed decidable timed logic.

翻译：度量时序逻辑（MTL）与时间命题时序逻辑（TPTL）扩展了线性时序逻辑（LTL）以处理实时约束：MTL采用时间界定的模态算子，而TPTL使用冻结量词。两者的可满足性问题通常不可判定；然而，MTL在特定非瞬时及部分瞬时限制下可变为可判定。对于TPTL，即使在单变量片段上，通过施加类似的非瞬时限制亦可平凡地恢复瞬时性。我们的首要贡献是研究1-TPTL中更具限制性的开放性概念，在此概念下瞬时性无法恢复。我们证明即使在此类限制下，可满足性检验的计算复杂度并未降低。这意味着1-TPTL（进而TPTL）无法像MTL那样通过放宽瞬时性获得益处。作为第二项贡献，我们在1-TPTL中引入一种精化的部分邻接限制（PA-1-TPTL），并证明其可满足性检验的可判定性。我们证明该逻辑的表达能力严格强于部分瞬时度量时序逻辑，使其成为目前已知表达能力最强的布尔闭包可判定时序逻辑之一。