BISIMULATIONS MEET PCTL EQUIVALENCES FOR PROBABILISTIC AUTOMATA
文献类型：期刊论文
| 作者 | Song, Lei ; Zhang, Lijun ; Godskesen, Jens Chr. ; Nielson, Flemming |
| 刊名 | LOGICAL METHODS IN COMPUTER SCIENCE
 |
| 出版日期 | 2013 |
| 卷号 | 9期号:2 |
| 关键词 | PCTL Probabilistic automata Characterization Bisimulation |
| ISSN号 | 1860-5974 |
| 中文摘要 | 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. |
| 英文摘要 | 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. |
| 收录类别 | SCI |
| 语种 | 英语 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16699]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 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). |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。