Faculty of Mathematics and Computer Science, University of Warmia and Mazury, Sloneczna 54, 10-710 Olsztyn, Poland.
Department of Mathematics and Computer Science, Jan Dlugosz University in Czestochowa, Armii Krajowej 13/15, 42-200 Czestochowa, Poland.
Sensors (Basel). 2022 Dec 6;22(23):9552. doi: 10.3390/s22239552.
Metric temporal logic (MTL) is a popular real-time extension of linear temporal logic (LTL). This paper presents a new simple SAT-based bounded model-checking (SAT-BMC) method for MTL interpreted over discrete infinite timed models generated by discrete timed automata with digital clocks. We show a new translation of the existential part of MTL to the existential part of linear temporal logic with a new set of atomic propositions and present the details of the new translation. We compare the new method's advantages to the old method based on a translation of the hard reset LTL (HLTL). Our method does not need new clocks or new transitions. It uses only one path and requires a smaller number of propositional variables and clauses than the HLTL-based method. We also implemented the new method, and as a case study, we applied the technique to analyze several systems. We support the theoretical description with the experimental results demonstrating the method's efficiency.
度量时序逻辑（MTL）是线性时序逻辑（LTL）的一种流行的实时扩展。本文提出了一种新的基于 SAT 的有界模型检查（SAT-BMC）方法，用于在由带数字时钟的离散时间自动机生成的离散无限时间模型上解释 MTL。我们展示了将 MTL 的存在部分转换为具有新原子命题集的线性时序逻辑的存在部分的新翻译，并介绍了新翻译的详细信息。我们将新方法的优点与基于硬重置 LTL（HLTL）的旧方法进行了比较。我们的方法不需要新的时钟或新的转换。它只使用一条路径，并且需要的命题变量和子句数比基于 HLTL 的方法少。我们还实现了新方法，并通过应用该技术分析了几个系统来作为案例研究。我们用实验结果支持理论描述，证明了该方法的效率。
