SAT-Based Explicit LTLf Satisfiability Checking

dc.contributor.author Li, Jianwen
dc.contributor.author Rozier, Kristin
dc.contributor.author Pu, Geguang
dc.contributor.author Zhang, Yueling
dc.contributor.author Vardi, Moshe
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department Electrical and Computer Engineering
dc.date 2020-02-27T23:05:44.000
dc.date.accessioned 2020-06-29T22:45:07Z
dc.date.available 2020-06-29T22:45:07Z
dc.date.copyright Tue Jan 01 00:00:00 UTC 2019
dc.date.embargo 2018-01-01
dc.date.issued 2019-07-17
dc.description.abstract <p>We present a SAT-based framework for LTL<sub><em>f</em> </sub>(Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTL<sub><em>f</em></sub> formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTL<sub><em>f</em> </sub> Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTL<sub><em>f</em> </sub>satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.</p>
dc.description.comments <p>This is a manuscript of a proceeding published as Li, Jianwen, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, and Moshe Y. Vardi. "SAT-Based Explicit LTL<em><sub>f</sub></em> Satisfiability Checking." In <em>Proceedings of the AAAI Conference on Artificial Intelligence </em>33, no. 1 (2019): 2946-2953. DOI: <a href="http://dx.doi.org/10.1609/aaai.v33i01.33012946" target="_blank">10.1609/aaai.v33i01.33012946</a>. Posted with permission.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/aere_conf/50/
dc.identifier.articleid 1050
dc.identifier.contextkey 16670841
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath aere_conf/50
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/1930
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/aere_conf/50/0-2020_AAAI_PermGrant.pdf|||Sat Jan 15 00:41:22 UTC 2022
dc.source.uri https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1135&context=aere_pubs
dc.subject.disciplines Theory and Algorithms
dc.supplemental.bitstream 2020_AAAI_PermGrant.pdf
dc.title SAT-Based Explicit LTLf Satisfiability Checking
dc.type article
dc.type.genre conference
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
File
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
0-2020_AAAI_PermGrant.pdf
Size:
15.03 KB
Format:
Adobe Portable Document Format
Description: