Campus Units
Aerospace Engineering, Computer Science, Electrical and Computer Engineering, Mathematics
Document Type
Article
Publication Version
Published Version
Publication Date
7-12-2019
Journal or Book Title
Lecture Notes in Computer Science
Volume
11562
First Page
3
Last Page
22
DOI
10.1007/978-3-030-25543-5_1
Abstract
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 MLTL0 , the variant of MLTL where all intervals start at 0, is PSPACE-complete. We introduce translations for MLTL-to-LTL, MLTL-to-LTLf , MLTL-to-SMV, and MLTL-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.
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Copyright Owner
The Authors
Copyright Date
2019
Language
en
File Format
application/pdf
Recommended Citation
Li, Jianwen; Vardi, Moshe Y.; and Rozier, Kristin Y., "Satisfiability Checking for Mission-Time LTL" (2019). Aerospace Engineering Publications. 147.
https://lib.dr.iastate.edu/aere_pubs/147
Included in
Software Engineering Commons, Systems Engineering and Multidisciplinary Design Optimization Commons
Comments
This article is published as Li, Jianwen, Moshe Y. Vardi, and Kristin Y. Rozier. "Satisfiability Checking for Mission-Time LTL." Lecture Notes in Computer Science 11562 (2019): 3-22. DOI: 10.1007/978-3-030-25543-5_1. Posted with permission.