Satisfiability checking for Mission-time LTL (MLTL)
Satisfiability checking for Mission-time LTL (MLTL)
复制标题
任务时间零担 (MLTL) 的满意度检查
DOI：
10.1016/j.ic.2022.104923
复制
发表时间：
2022
影响因子：
1
通讯作者：
Rozier, Kristin Y.
中科院分区：
文献类型：
--
作者：
Li, Jianwen;Vardi, Moshe Y.;Rozier, Kristin Y.
任务时间线性时序逻辑（LTL），缩写为MLTL，是度量时序逻辑（MTL）在自然逻辑上的有界变体，旨在通用地指定飞机，航天器，车辆和机器人常见的基于任务的系统操作的要求。尽管MLTL作为规范逻辑的效用，但在分析MLTL时仍然存在主要差距，例如，用于规范调试或模型检查，集中在没有任何完整的MLTL可满足性检查器。在本文中，我们探讨了MLTL可满足性检查的理论和算法问题。我们证明了MLTL的可满足性检查问题是NEXPTIME-完全的，而MLTL的所有区间从0开始的变体MLTL 0的可满足性检查是PSPACE-完全的。为了探索MLTL可满足性检查的最佳算法解决方案，我们将该问题分别归结为LTL可满足性检查、LTLf（LTL over finite traces）可满足性检查和模型检查，从而进行MLTL到LTL、MLTL到LTLf和MLTL到SMV的转换。此外，我们提出了一个新的基于SMT的解决方案MLTL可满足性检查，并创建一个翻译MLTL到SMT。我们广泛的实验评估表明，虽然使用NuXmv模型检查器的MLTL到SMV转换在间隔范围较小（小于100）的基准测试中表现最好，但使用Z3 SMT求解器的MLTL到SMT转换提供了最具可扩展性的性能。
Mission-time Linear Temporal Logic (LTL), abbreviated as MLTL, is a bounded variant of Metric Temporal Logic (MTL) over naturals designed to generically specify requirements for mission-based system operation common to aircraft, spacecraft, vehicles, and robots. Despite the utility of MLTL as a specification logic, major gaps remain in analyzing MLTL, e.g., for specification debugging or model checking, centering on the absence of any complete MLTL satisfiability checker. In this paper, we explore both the theoretical and algorithmic problems of MLTL satisfiability checking. We prove that the MLTL satisfiability checking problem is NEXPTIME-complete and that satisfiability checking MLTL0, the variant of MLTL where all intervals start at 0, is PSPACE-complete. To explore the best algorithmic solution for MLTL satisifiability checking, we reduce this problem to LTL satisfiability checking, LTLf(LTL over finite traces) satisfiability checking, and model checking respectively, thus conducting translations for MLTL-to-LTL, MLTL-to-LTLf, and MLTL-to-SMV. Moreover, we propose a new SMT-based solution for MLTL satisfiability checking and create a translation for MLTL-to-SMT. Our extensive experimental evaluation shows that while the MLTL-to-SMV translation with NuXmv model checker performs best on the benchmarks whose interval ranges are small (than 100), the MLTL-to-SMT translation with the Z3 SMT solver offers the most scalable performance.
基于 SMT 的 MITL 可满足性检查方法
影响因子：
1
作者：
M. Bersani;M. Rossi;P. S. Pietro
通讯作者：
P. S. Pietro
影响因子：
2.5
作者：
Alur, R;Feder, T;Henzinger, TA
通讯作者：
Henzinger, TA