Title

Satisfiability Checking for Mission-Time LTL

Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering, Mathematics

Document Type

Conference Proceeding

Conference

31st International Conference on Computer Aided Verification

Publication Version

Published Version

Publication Date

7-12-2019

Journal or Book Title

Computer Aided Verification: 31st International Conference

First Page

3

Last Page

22

DOI

10.1007/978-3-030-25543-5_1

Conference Title

31st International Conference on Computer Aided Verification

Conference Date

July 15-18, 2019

City

New York, New York

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 proceeding is published as Li, Jianwen, Moshe Y. Vardi, and Kristin Y. Rozier. "Satisfiability checking for mission-time LTL." In: Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Isil Dillig and Serdar Tasiran, editors. Lecture Notes in Computer Science 11562 (2019): 3-22. DOI: 10.1007/978-3-030-25543-5_1. Posted with permission.

Creative Commons License

Creative Commons Attribution 4.0 License
This work is licensed under a Creative Commons Attribution 4.0 License.

Copyright Owner

The Author(s)

Language

en

File Format

application/pdf

Share

Article Location

 
COinS