SAT-Based Explicit LTLf Satisfiability Checking Li, Jianwen Rozier, Kristin Pu, Geguang Zhang, Yueling Vardi, Moshe
dc.contributor.department Aerospace Engineering
dc.contributor.department Computer Science
dc.contributor.department Electrical and Computer Engineering 2020-02-27T23:05:44.000 2020-06-29T22:45:07Z 2020-06-29T22:45:07Z Tue Jan 01 00:00:00 UTC 2019 2018-01-01 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="" target="_blank">10.1609/aaai.v33i01.33012946</a>. Posted with permission.</p>
dc.format.mimetype application/pdf
dc.identifier archive/
dc.identifier.articleid 1050
dc.identifier.contextkey 16670841
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath aere_conf/50
dc.language.iso en
dc.source.bitstream archive/|||Sat Jan 15 00:41:22 UTC 2022
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
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
15.03 KB
Adobe Portable Document Format