概率带测试克林代数

《概率带测试克林代数》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、第41卷第1期四川大学学报(工程科学版)Vol.41No.12009年1月JOURNALOFSICHUANUNIVERSITY(ENGINEERINGSCIENCEEDITION)Jan.2009文章编号:1009-3087(2009)01-0134-05概率带测试克林代数乔瑞,吴尽昭(中国科分院成都计算机应用研究所,四川成都610041)摘要:为了增强可形式刻画正则程序行为的带测试克林代数(KAT)的表达能力,提出了一个加概率的带测试克林代数(PKAT)的完整理论用于对加概率正则程序的推演。提出了状

2、态为PKAT表达式和数据状态组成的序列对的概率格局变迁系统。然后在概率格局变迁系统的基础上给出结构操作语义。并给出PKAT的基于操作语义的概率互模拟等价关系。最后证明了PKAT中等式关于互模拟等价的可靠性。关键词:概率带测试克林代数;概率格局变迁系统;结构操作语义;互模拟等价中图分类号:TP301.2;TP302.7文献标识码:AProbabilisticKleeneAlgebrawithTestsQIAORui,WUJin-zhao(ChengduInst.ofComputerApplication

3、,ChineseAcademyofSci.,Chengdu610041,China)Abstract:InordertoimprovetheexpressivenessofKleenealgebrawithtests(KAT),whichformalizesthebehav-iorofregularprograms,acompletetheoryofprobabilisticKleenealgebrawithtests(PKAT)forreasoningregularprogramswithproba

4、bilitywasproposed.Amodeltermedprobabilisticconfigurationtransitionsystemswaspro-posed,whicharecomposedofapairofaPKATexpressionandadata-state.OperationalsemanticsforPKATbasedonthemodelwasputforward,andaprobabilisticbisimulationequivalencerelationinPKATwa

5、sestablished.ThesoundnessoftheequationsofPKATwasvalidatedwithrespecttothebisimulation.Keywords:PKAT;probabilisticconfigurationtransitionsystems;structuraloperationalsemantics;bisimulation正则程序是有着顺序合成,不确定选择,和有概率程序有很多优点,如高有效性,结果程序的[1-2][3][6]限迭代操作的程序。带测试克林

6、代数(KAT)概念简单性等。带有概率的正则程序有着比正是正则程序的代数模型。测试是用于建模传统的程则程序更丰富和更强的表达能力。概率选择和不确序结构的不可缺少的元素,如if条件和while循环,定选择两者的重要区别在于:前者由一个概率机制并且可处理断言。在应用方面,带测试克林代数能所决定,后者完全是自由的。假设执行次数是无限[4]够代替Hoare逻辑进行程序正确性证明。在文献的,当在语句集s1和s2之间不确定选择一个时,选[5]中提到基于KAT的定理证明器。择s1和s2次数的比例不是一个常数。而概率选

7、择两者时,则比例是一个常数。当建模系统时,一些选择收稿日期:2007-10-25只能用不确定选择来表示,而不能用概率选择表基金项目:国家973计划资助项目(2004CB318000;示。如果当一个选择确实由一定概率决定,则可以2007CB310800);国家高技术发展计划(863计用概率选择表示。因此,两种选择可以在单个语言划)资助项目(2007AA01Z143)作者简介:乔瑞(1981-),女,博士生.研究方向:形式化方中出现。为了将两种选择混用在一个程序中,有必法.要指定两种选择的顺序。有3种方式

8、:第1种总是第1期乔瑞,等:概率带测试克林代数135先执行不确定选择,第2种总是先执行概率选择,克林代数是一个结构κ=(K,+,·,＊,0,1),＊第3种是谁先出现就先执行谁。这里采用第一种方其中,(K,+,·,0,1)是一个等幂半环。操作s含义式。然而KAT不能用来推演概率程序。它不能表同形式语言理论中的克林星号。带测试克林代数是示概率程序中的语句如:“投一个两面的硬币”。因一个带有嵌入的布尔代数的克林代数。形式的它为此定义了一种KAT的扩展代数形式,