概率带测试克林代数

• 作 者: 乔瑞 吴尽昭
• 机 构: 中国科分院成都计算机应用研究所
• 出 处: 四川大学学报：工程科学版
• 发表日期: 2009年1期
• 关键词: 概率带测试克林代数 概率格局变迁系统 结构操作语义 互模拟等价 PKAT probabilistic configuration transition syst
• 基金项目: 国家973计划资助项目(2004CB318000,2007CB310800),, 国家高技术发展计划(863计划)资助项目(2007AA01Z143)

为了增强可形式刻画正则程序行为的带测试克林代数(KAT)的表达能力,提出了一个加概率的带测试克林代数(PKAT)的完整理论用于对加概率正则程序的推演。提出了状态为PKAT表达式和数据状态组成的序列对的概率格局变迁系统。然后在概率格局变迁系统的基础上给出结构操作语义。并给出PKAT的基于操作语义的概率互模拟等价关系。最后证明了PKAT中等式关于互模拟等价的可靠性。