部分准时度量时态逻辑是可判定的
Partially Punctual Metric Temporal Logic is Decidable
摘要：
度量时态逻辑$\mathsf{MTL}[\until_I,\since_I]$是研究最多的实时的逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。Henzinger等人，在他们的开创性论文中表明，称为$\mathsf{MITL}$的$\mathsf{MTL}$的非准时片段是可判定的。在本文中，我们锐化这一可判定性的结果表明，部分准时片段的$\mathsf{MTL}$（表示$\mathsf{PMTL}$）是可判定的严格单调有限的逐点时间。在这个片段中，我们要么允许准时的未来模态，要么允许准时的过去模态，但绝不能两者同时存在。给出了从$\mathsf{PMTL}$到可判定逻辑$\mathsf{MTL}[\until_I]$的两个保满足性约简。第一次减少使用简单的预测，而第二次减少使用一种新的技术的时间预测过采样。我们研究了这两个减少之间的权衡：而第二次减少允许在底层模型中引入额外的动作点，equisatifiable $\mathsf{MTL}[\until_I]$公式获得的是指数简洁比通过第一次减少，其中没有过采样的底层模型是必要的。我们还表明，$\mathsf{PMTL}$是严格的表达比片段$\mathsf{MTL}[\until_I,\since]$和$\mathsf{MTL}[\until,\since_I]$。
英文摘要：
Metric Temporal Logic $\mathsf{MTL}[\until_I,\since_I]$ is one of the most studied real time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. Henzinger et al., in their seminal paper showed that the non-punctual fragment of $\mathsf{MTL}$ called $\mathsf{MITL}$ is decidable. In this paper, we sharpen this decidability result by showing that the partially punctual fragment of $\mathsf{MTL}$ (denoted $\mathsf{PMTL}$) is decidable over strictly monotonic finite point wise time. In this fragment, we allow either punctual future modalities, or punctual past modalities, but never both together. We give two satisfiability preserving reductions from $\mathsf{PMTL}$ to the decidable logic $\mathsf{MTL}[\until_I]$. The first reduction uses simple projections, while the second reduction uses a novel technique of temporal projections with oversampling. We study the trade-off between the two reductions: while the second reduction allows the introduction of extra action points in the underlying model, the equisatisfiable $\mathsf{MTL}[\until_I]$ formula obtained is exponentially succinct than the one obtained via the first reduction, where no oversampling of the underlying model is needed. We also show that $\mathsf{PMTL}$ is strictly more expressive than the fragments $\mathsf{MTL}[\until_I,\since]$ and $\mathsf{MTL}[\until,\since_I]$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
