Satisfiability Checking for Mission-Time LTL

dc.contributor.author Li, Jianwen
dc.contributor.author Vardi, Moshe
dc.contributor.author Rozier, Kristin
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department 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.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
Now showing 1 - 1 of 1
Name:
2019_RozierKristin_SatisfiabilityChecking.pdf
Size:
602.05 KB
Format:
Adobe Portable Document Format
Description:
Collections