MITL规范可满足性的判定
Deciding the Satisfiability of MITL Specifications
摘要：
在本文中，我们提出了一个可满足性保持减少MITL解释有限变量连续行为的约束LTL时钟，CLTL的一个变种，是可判定的，并为一个SMT为基础的有界可满足性检查。其结果是一个新的完整的和有效的决策程序的MITL。虽然MITL的决策程序已经存在，他们采用的自动机为基础的技术似乎是很难实现在实践中，而且，据我们所知，目前还没有实现它们。一个原型工具MITL的基础上的编码在这里提出的，而不是，已经实施，并公开提供。
英文摘要：
In this paper we present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
