AI 中文总结
研究MITL可满足性，基于跟踪时间约束义务的想法提出新方法，通过引入时间概念增强检查LTL公式真值的方式，用简单机制消除或合并冗余义务，发展出基于区域的符号过程。
AI 中文摘要
度量区间时态逻辑（MITL）的可满足性是一个被广泛研究的主题。在这项工作中，我们基于沿着单词跟踪时间约束义务的想法，提出了一种新的、且可以说是更简单的MITL可满足性方法。为检查线性时态逻辑（LTL）公式在单词的某个位置是否为真，自然会生成在后续点需要满足的某些义务。例如，对于严格直到语义的$a ~\mathcal{U}~ b$，若在位置$i + 1$处$b$或集合$\{a, a ~\mathcal{U}~ b\}$为真，则在位置$i$处为真。我们通过在这些义务中引入时间概念在MITL背景下增强了这一想法。然而，一个简单的过程可能会导致沿着单词生成越来越多的义务且数量无界。我们提出了一种简单机制来消除或合并冗余义务。对于MITL，该机制确保在整个定时单词中仅维持有限数量的义务。我们将这一观察发展为一种使用区域的MITL可满足性的符号过程。
英文摘要
Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, based on an idea of tracking time-constrained obligations along a word. To check whether a Linear Temporal Logic (LTL) formula is true at a position of a word, it is natural to generate certain obligations that need to be satisfied at a later point. For instance, $a ~\mathcal{U}~ b$ (with strict Until semantics) is true at position $i$ if either $b$ or the set $\{a, a ~\mathcal{U}~ b\}$ is true at $i+1$. We enhance this idea in the context of MITL by introducing a notion of time inside these obligations. However, a naïve procedure could lead to more and more obligations getting generated along the word, with no bound on the number. We propose a simple mechanism to eliminate or merge redundant obligations. For MITL, this mechanism ensures that only a bounded number of obligations are maintained along the entire timed word. We develop this observation into a symbolic procedure for MITL satisfiability using regions.
