| Title: | LTL satisfiability checking revisited |
| Author: | Li, Jianwen (1)
; Zhang, Lijun (2)
; Pu, Geguang (1)
; Vardi, Moshe Y. (3)
; He, Jifeng (1)
|
| Conference Name: | 20th International Symposium on Temporal Representation and Reasoning, TIME 2013
|
| Conference Date: | September 26, 2013 - September 28, 2013
|
| Issued Date: | 2013
|
| Conference Place: | Pensacola, FL, United states
|
| Publish Place: | Institute of Electrical and Electronics Engineers Inc.
|
| Indexed Type: | EI
|
| ISBN: | 9780769551128
|
| Department: | (1) Software Engineering, East China Normal University, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China; (3) Computer Science, Rice University, United States
|
| Abstract: | We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B'uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools. © 2013 IEEE. |
| English Abstract: | We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B'uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools. © 2013 IEEE. |
| Language: | 英语
|
| Content Type: | 会议论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/16685
|
| Appears in Collections: | 软件所图书馆_会议论文
|
|
There are no files associated with this item.
|
| Recommended Citation: | |
Li, Jianwen ,Zhang, Lijun ,Pu, Geguang ,et al. LTL satisfiability checking revisited[C]. 见:20th International Symposium on Temporal Representation and Reasoning, TIME 2013. Pensacola, FL, United states. September 26, 2013 - September 28, 2013.
|
|
|
