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.
|
|
|