| LTL satisfiability checking revisited | |
| Li, Jianwen (1); Zhang, Lijun (2); Pu, Geguang (1); Vardi, Moshe Y. (3); He, Jifeng (1) | |
| 2013 | |
| 会议名称 | 20th International Symposium on Temporal Representation and Reasoning, TIME 2013 |
| 页码 | 91-98 |
| 会议日期 | September 26, 2013 - September 28, 2013 |
| 会议地点 | Pensacola, FL, United states |
| 收录类别 | EI |
| 出版地 | Institute of Electrical and Electronics Engineers Inc. |
| ISBN | 9780769551128 |
| 部门归属 | (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 |
| 摘要 | 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. |
| 语种 | 英语 |
| 内容类型 | 会议论文 |
| URI标识 | http://ir.iscas.ac.cn/handle/311060/16685 |
| 专题 | 中国科学院软件研究所 |
| 推荐引用方式 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. |
| 条目包含的文件 | 条目无相关文件。 | |||||
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论