中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
Title:
Incremental bisimulation abstraction refinement
Author: Song, Lei (1) ; Zhang, Lijun (2) ; Hermanns, Holger (1) ; Godskesen, Jens Chr. (3)
Conference Name: 2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013
Conference Date: July 8, 2013 - July 10, 2013
Issued Date: 2013
Conference Place: Barcelona, Spain
Keyword: Algorithms ; Experimentation ; Verification ; Bisimulation ; CEGAR ; probabilistic automata
Publish Place: Institute of Electrical and Electronics Engineers Inc., 3 Park Avenue, 17th Floor, New York, NY 10016-5997, United States
Indexed Type: SCI ; EI
ISSN: 15504808
ISBN: 9780769550350
Department: (1) Saarland University, Germany; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China; (3) IT University of Copenhagen, Denmark; (4) Max-Planck-Institut für Informatik, Saarbrücken, Germany
Abstract: Abstraction refinement techniques in probabilistic model checking are prominent approaches to the verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This paper proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach. © 2013 IEEE.
English Abstract: Abstraction refinement techniques in probabilistic model checking are prominent approaches to the verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This paper proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach. © 2013 IEEE.
Language: 英语
Citation statistics:
Content Type: 会议论文
URI: http://ir.iscas.ac.cn/handle/311060/16502
Appears in Collections:软件所图书馆_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Song, Lei ,Zhang, Lijun ,Hermanns, Holger ,et al. Incremental bisimulation abstraction refinement[C]. 见:2013 13th International Conference on Application of Concurrency to System Design, ACSD 2013. Barcelona, Spain. July 8, 2013 - July 10, 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
[Song, Lei (1)]'s Articles
[Zhang, Lijun (2)]'s Articles
[Hermanns, Holger (1)]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Song, Lei (1)]‘s Articles
[Zhang, Lijun (2)]‘s Articles
[Hermanns, Holger (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-2020  中国科学院软件研究所 - Feedback
Powered by CSpace