Satisfiability Checking for Mission-Time LTL

Date
2019-07-12
Authors
Li, Jianwen
Vardi, Moshe
Rozier, Kristin
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Aerospace Engineering
Organizational Unit
Computer Science
Organizational Unit
Mathematics
Organizational Unit
Journal Issue
Series
Department
Aerospace EngineeringComputer ScienceElectrical and Computer EngineeringMathematics
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.

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.

Description
Keywords
Citation
DOI
Collections