TY - GEN
T1 - Satisfiability checking for mission-time LTL
AU - Li, Jianwen
AU - Vardi, Moshe Y.
AU - Rozier, Kristin Y.
N1 - Publisher Copyright:
© The Author(s) 2019.
PY - 2019
Y1 - 2019
N2 - Mission-time LTL (MLTL) is a bounded variant of 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. We prove that the MLTL satisfiability checking problem is NEXPTIME-complete and that satisfiability checking, the variant of MLTL where all intervals start at 0, is PSPACE-complete. We introduce translations for MLTL-to-LTL,, MLTL-to-SMV, and MLTf-to-SMT, creating four options for MLTL satisfiability checking. Our extensive experimental evaluation shows that the MLTL-to-SMT transition with the Z3 SMT solver offers the most scalable performance.
AB - Mission-time LTL (MLTL) is a bounded variant of 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. We prove that the MLTL satisfiability checking problem is NEXPTIME-complete and that satisfiability checking, the variant of MLTL where all intervals start at 0, is PSPACE-complete. We introduce translations for MLTL-to-LTL,, MLTL-to-SMV, and MLTf-to-SMT, creating four options for MLTL satisfiability checking. Our extensive experimental evaluation shows that the MLTL-to-SMT transition with the Z3 SMT solver offers the most scalable performance.
UR - https://www.scopus.com/pages/publications/85069803289
U2 - 10.1007/978-3-030-25543-5_1
DO - 10.1007/978-3-030-25543-5_1
M3 - 会议稿件
AN - SCOPUS:85069803289
SN - 9783030255428
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 22
BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings
A2 - Dillig, Isil
A2 - Tasiran, Serdar
PB - Springer Verlag
T2 - 31st International Conference on Computer Aided Verification, CAV 2019
Y2 - 15 July 2019 through 18 July 2019
ER -