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 |
会议日期 | September 26, 2013 - September 28, 2013 |
会议地点 | Pensacola, FL, United states |
页码 | 91-98 |
中文摘要 | 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. |
收录类别 | EI |
会议录出版地 | Institute of Electrical and Electronics Engineers Inc. |
语种 | 英语 |
ISBN号 | 9780769551128 |
内容类型 | 会议论文 |
源URL | [http://ir.iscas.ac.cn/handle/311060/16685] |
专题 | 软件研究所_软件所图书馆_会议论文 |
推荐引用方式 GB/T 7714 | 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. |
个性服务 |
查看访问统计 |
相关权益政策 |
暂无数据 |
收藏/分享 |
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。
修改评论