Satisfiability Checking for Mission-Time LTL
dc.contributor.author | Li, Jianwen | |
dc.contributor.author | Vardi, Moshe | |
dc.contributor.author | Rozier, Kristin Yvonne | |
dc.contributor.department | Department of Aerospace Engineering | |
dc.contributor.department | Department of Computer Science | |
dc.contributor.department | Department of Electrical and Computer Engineering | |
dc.contributor.department | Mathematics | |
dc.date | 2019-09-14T17:18:48.000 | |
dc.date.accessioned | 2020-06-29T22:45:36Z | |
dc.date.available | 2020-06-29T22:45:36Z | |
dc.date.copyright | Tue Jan 01 00:00:00 UTC 2019 | |
dc.date.issued | 2019-07-12 | |
dc.description.abstract | <p>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 <strong>MLTL<sub>0 </sub></strong>, the variant of MLTL where all intervals start at <strong>0</strong>, is PSPACE-complete. We introduce translations for MLTL-to-LTL, <strong>MLTL-to-LTL<em><sub>f</sub></em></strong> , 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.</p> | |
dc.description.comments | <p>This article is published as Li, Jianwen, Moshe Y. Vardi, and Kristin Y. Rozier. "Satisfiability Checking for Mission-Time LTL." <em>Lecture Notes in Computer Science </em>11562 (2019): 3-22. DOI: <a href="http://dx.doi.org/10.1007/978-3-030-25543-5_1" target="_blank">10.1007/978-3-030-25543-5_1</a>. Posted with permission.</p> | |
dc.format.mimetype | application/pdf | |
dc.identifier | archive/lib.dr.iastate.edu/aere_pubs/147/ | |
dc.identifier.articleid | 1148 | |
dc.identifier.contextkey | 14952513 | |
dc.identifier.s3bucket | isulib-bepress-aws-west | |
dc.identifier.submissionpath | aere_pubs/147 | |
dc.identifier.uri | https://dr.lib.iastate.edu/handle/20.500.12876/1993 | |
dc.language.iso | en | |
dc.source.bitstream | archive/lib.dr.iastate.edu/aere_pubs/147/2019_RozierKristin_SatisfiabilityChecking.pdf|||Fri Jan 14 20:25:05 UTC 2022 | |
dc.source.uri | 10.1007/978-3-030-25543-5_1 | |
dc.subject.disciplines | Software Engineering | |
dc.subject.disciplines | Systems Engineering and Multidisciplinary Design Optimization | |
dc.title | Satisfiability Checking for Mission-Time LTL | |
dc.type | article | |
dc.type.genre | article | |
dspace.entity.type | Publication | |
relation.isAuthorOfPublication | 3c555e5b-8fd1-4c38-98c6-6a2449fab7cf | |
relation.isOrgUnitOfPublication | 047b23ca-7bd7-4194-b084-c4181d33d95d | |
relation.isOrgUnitOfPublication | f7be4eb9-d1d0-4081-859b-b15cee251456 | |
relation.isOrgUnitOfPublication | a75a044c-d11e-44cd-af4f-dab1d83339ff | |
relation.isOrgUnitOfPublication | 82295b2b-0f85-4929-9659-075c93e82c48 |
File
Original bundle
1 - 1 of 1
No Thumbnail Available
- Name:
- 2019_RozierKristin_SatisfiabilityChecking.pdf
- Size:
- 602.05 KB
- Format:
- Adobe Portable Document Format
- Description: