ISCAS OpenIR
BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA
Song, Lei; Zhang, Lijun; Godskesen, Jens Chr.; Nielson, Flemming
2013
SourceLOGICAL METHODS IN COMPUTER SCIENCE
ISSN1860-5974
Volume9Issue:2
English AbstractProbabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in [34], but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting.; Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a both sound and complete behavioral equivalence has been pointed out by Segala in [34], but remains open throughout the years. In this paper we introduce novel notions of strong bisimulation relations, which characterize PCTL and PCTL* exactly. We extend weak bisimulations that characterize PCTL and PCTL* without next operator, respectively. Further, we also extend the framework to simulation preorders. Thus, our paper bridges the gap between logical and behavioral equivalences and preorders in this setting.
Indexed TypeSCI
KeywordPctl Probabilistic Automata Characterization Bisimulation
Department[Song, Lei; Zhang, Lijun] Saarland Univ Comp Sci, Saarbrucken, Germany. [Zhang, Lijun] Tech Univ Denmark, DTU Informat, Chinese Acad Sci, State Key Lab Comp Sci,Inst Software, Lyngby, Denmark. [Godskesen, Jens Chr.] IT Univ Copenhagen, Copenhagen, Denmark. [Nielson, Flemming] Tech Univ Denmark, DTU Compute, Lyngby, Denmark.
Language英语
Content Type期刊论文
URIhttp://ir.iscas.ac.cn/handle/311060/16699
Collection中国科学院软件研究所
Recommended Citation
GB/T 7714
Song, Lei,Zhang, Lijun,Godskesen, Jens Chr.,et al. BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA[J]. LOGICAL METHODS IN COMPUTER SCIENCE,2013,9(2).
APA Song, Lei,Zhang, Lijun,Godskesen, Jens Chr.,&Nielson, Flemming.(2013).BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA.LOGICAL METHODS IN COMPUTER SCIENCE,9(2).
MLA Song, Lei,et al."BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA".LOGICAL METHODS IN COMPUTER SCIENCE 9.2(2013).
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
[Song, Lei]'s Articles
[Zhang, Lijun]'s Articles
[Godskesen, Jens Chr.]'s Articles
Baidu academic
Similar articles in Baidu academic
[Song, Lei]'s Articles
[Zhang, Lijun]'s Articles
[Godskesen, Jens Chr.]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Song, Lei]'s Articles
[Zhang, Lijun]'s Articles
[Godskesen, Jens Chr.]'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.