中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
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:软件所图书馆_会议论文

Files in This Item:

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.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Li, Jianwen (1)]'s Articles
[Zhang, Lijun (2)]'s Articles
[Pu, Geguang (1)]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Li, Jianwen (1)]‘s Articles
[Zhang, Lijun (2)]‘s Articles
[Pu, Geguang (1)]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace