SAT-based explicit LTL reasoning and its application to satisfiability checking

Jianwen Li; Shufang Zhu; Geguang Pu; Lijun Zhang; Moshe Y. Vardi

doi:10.1007/s10703-018-00326-5

SAT-based explicit LTL reasoning and its application to satisfiability checking

Jianwen Li
, Shufang Zhu
, Geguang Pu^*
, Lijun Zhang
, Moshe Y. Vardi

^*Corresponding author for this work

Software Engineering Institute

Rice University
East China Normal University
University of Chinese Academy of Sciences

Research output: Contribution to journal › Article › peer-review

17 Scopus citations

Abstract

We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.

Original language	English
Pages (from-to)	164-190
Number of pages	27
Journal	Formal Methods in System Design
Volume	54
Issue number	2
DOIs	https://doi.org/10.1007/s10703-018-00326-5
State	Published - 1 Nov 2019

Keywords

Linear temporal logic
SAT-based LTL checking
Satisfiability checking

Access to Document

10.1007/s10703-018-00326-5

Cite this

@article{553fce5591b3441b845c23fedd1721d7,

title = "SAT-based explicit LTL reasoning and its application to satisfiability checking",

abstract = "We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.",

keywords = "Linear temporal logic, SAT-based LTL checking, Satisfiability checking",

author = "Jianwen Li and Shufang Zhu and Geguang Pu and Lijun Zhang and Vardi, \{Moshe Y.\}",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Science+Business Media, LLC, part of Springer Nature.",

year = "2019",

month = nov,

day = "1",

doi = "10.1007/s10703-018-00326-5",

language = "英语",

volume = "54",

pages = "164--190",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - SAT-based explicit LTL reasoning and its application to satisfiability checking

AU - Li, Jianwen

AU - Zhu, Shufang

AU - Pu, Geguang

AU - Zhang, Lijun

AU - Vardi, Moshe Y.

PY - 2019/11/1

Y1 - 2019/11/1

N2 - We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.

AB - We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. The crux of our approach is a construction of temporal transition system that is based on SAT-solving rather than tableau to construct states and transitions. As a proof-of-concept of this framework, we describe a new LTL satisfiability algorithm. We tested the effectiveness of this approach by demonstrating that it significantly outperforms all existing LTL-satisfiability-checking algorithms.

KW - Linear temporal logic

KW - SAT-based LTL checking

KW - Satisfiability checking

UR - https://www.scopus.com/pages/publications/85059581436

U2 - 10.1007/s10703-018-00326-5

DO - 10.1007/s10703-018-00326-5

M3 - 文章

AN - SCOPUS:85059581436

SN - 0925-9856

VL - 54

SP - 164

EP - 190

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 2

ER -

SAT-based explicit LTL reasoning and its application to satisfiability checking

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this