Institutional Repository
| LTL satisfiability checking revisited | |
| Li, Jianwen (1); Zhang, Lijun (2); Pu, Geguang (1); Vardi, Moshe Y. (3); He, Jifeng (1) | |
| 2013 | |
| Conference Name | 20th International Symposium on Temporal Representation and Reasoning, TIME 2013 |
| Pages | 91-98 |
| Conference Date | September 26, 2013 - September 28, 2013 |
| Conference Place | Pensacola, FL, United states |
| Indexed Type | EI |
| Publish Place | Institute of Electrical and Electronics Engineers Inc. |
| 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 |
| 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.; 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 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Li, Jianwen ,Zhang, Lijun ,Pu, Geguang ,et al. LTL satisfiability checking revisited[C]. Institute of Electrical and Electronics Engineers Inc.,2013:91-98. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment