| 概率带测试克林代数 |
| |
| 引用本文： | 乔瑞,吴尽昭. 概率带测试克林代数[J]. 四川大学学报(工程科学版), 2009, 41(1): 134-138 |
| |
| 作者姓名： | 乔瑞 吴尽昭 |
| |
| 作者单位： | 中国科分院成都计算机应用研究所 |
| |
| 基金项目： | 国家重点基础研究发展计划(973计划)，国家高技术研究发展计划(863计划) |
| |
| 摘 要： | 为了增强可形式刻画正则程序行为的带测试克林代数(KAT)的表达能力,提出了一个加概率的带测试克林代数(PKAT)的完整理论用于对加概率正则程序的推演。提出了状态为PKAT表达式和数据状态组成的序列对的概率格局变迁系统。然后在概率格局变迁系统的基础上给出结构操作语义。并给出PKAT的基于操作语义的概率互模拟等价关系。最后证明了PKAT中等式关于互模拟等价的可靠性。
|
| 关 键 词： | 概率带测试克林代数 概率格局变迁系统 结构操作语义 互模拟等价 |
| 收稿时间： | 2007-10-25 |
Probabilistic Kleene Algebra with Tests |
| |
| QIAO Rui,WU Jin-zhao. Probabilistic Kleene Algebra with Tests[J]. Journal of Sichuan University (Engineering Science Edition), 2009, 41(1): 134-138 |
| |
| Authors: | QIAO Rui WU Jin-zhao |
| |
| Affiliation: | Chengdu Inst. of Computer Application,Chinese Academy of Sci., Chengdu 610041,China;Chengdu Inst. of Computer Application,Chinese Academy of Sci., Chengdu 610041,China |
| |
| Abstract: | In order to improve the expressiveness of Kleene algebra with tests(KAT),which formalizes the behavior of regular programs,a complete theory of probabilistic Kleene algebra with tests(PKAT) for reasoning regular programs with probability was proposed.A model termed probabilistic configuration transition systems was proposed,which are composed of a pair of a PKAT expression and a data-state.Operational semantics for PKAT based on the model was put forward,and a probabilistic bisimulation equivalence relation in PKAT was established.The soundness of the equations of PKAT was validated with respect to the bisimulation. |
| |
| Keywords: | PKAT probabilistic configuration transition systems structural operational semantics bisimulation |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《四川大学学报(工程科学版)》浏览原始摘要信息 |
|
点击此处可从《四川大学学报(工程科学版)》下载全文 |
