ISCAS OpenIR
Probably safe or live
Katoen, Joost-Pieter (1); Song, Lei (2); Zhang, Lijun (3); Zhang, L.(zhanglj@ios.ac.cn)
2014
Conference NameJoint Meeting of the 23rd Annual EACSL Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/ IEEE Symposium on Logic in Computer Science, LICS 2014
Conference DateJuly 14, 2014 - July 18, 2014
Conference PlaceVienna, Austria
Indexed TypeEI
Publish PlaceAssociation for Computing Machinery
ISBN9781450328869
Department(1) Software Modelling and Verification, RWTH Aachen University, Germany; (2) Max-Planck-Institut für Informatik, Dependable Systems and Software, Universität des Saarlandes, Germany; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China
English AbstractThis paper presents a formal characterisation of safety and liveness properties for fully probabilistic systems. As for the classical setting, it is established that any (probabilistic tree) property is equivalent to a conjunction of a safety and liveness property. A simple algorithm is provided to obtain such a property decomposition for flat probabilistic CTL (PCTL). A safe fragment of PCTL is identified that provides a sound and complete characterisation of safety properties. For liveness properties, we provide two PCTL fragments, a sound and a complete one, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. We show that safety properties only have finite counterexamples, whereas liveness properties have none. We compare our characterisation for qualitative properties with the one for branching time properties by Manolios and Trefler, and present sound and complete PCTL fragments for characterising the notions of strong safety and absolute liveness coined by Sistla. Copyright © 2014 ACM.; This paper presents a formal characterisation of safety and liveness properties for fully probabilistic systems. As for the classical setting, it is established that any (probabilistic tree) property is equivalent to a conjunction of a safety and liveness property. A simple algorithm is provided to obtain such a property decomposition for flat probabilistic CTL (PCTL). A safe fragment of PCTL is identified that provides a sound and complete characterisation of safety properties. For liveness properties, we provide two PCTL fragments, a sound and a complete one, and show that a sound and complete logical characterisation of liveness properties hinges on the (open) satisfiability problem for PCTL. We show that safety properties only have finite counterexamples, whereas liveness properties have none. We compare our characterisation for qualitative properties with the one for branching time properties by Manolios and Trefler, and present sound and complete PCTL fragments for characterising the notions of strong safety and absolute liveness coined by Sistla. Copyright © 2014 ACM.
Language英语
Content Type会议论文
URIhttp://ir.iscas.ac.cn/handle/311060/16623
Collection中国科学院软件研究所
Corresponding AuthorZhang, L.(zhanglj@ios.ac.cn)
Recommended Citation
GB/T 7714
Katoen, Joost-Pieter ,Song, Lei ,Zhang, Lijun ,et al. Probably safe or live[C]. Association for Computing Machinery,2014.
Files in This Item:
There are no files associated with this item.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Katoen, Joost-Pieter (1)]'s Articles
[Song, Lei (2)]'s Articles
[Zhang, Lijun (3)]'s Articles
Baidu academic
Similar articles in Baidu academic
[Katoen, Joost-Pieter (1)]'s Articles
[Song, Lei (2)]'s Articles
[Zhang, Lijun (3)]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Katoen, Joost-Pieter (1)]'s Articles
[Song, Lei (2)]'s Articles
[Zhang, Lijun (3)]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

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