平稳分布马尔可夫过程的概率规划代数及其应用

269理论计算机科学电子笔记45（2001）网址：http://www.elsevier.nl/locate/entcs/volume45.html11页平稳分布的推广与概率规划代数A.K. McIver1，2澳大利亚新南威尔士州麦考瑞大学计算机系摘要我们概括的经典概念的平稳分布的马尔可夫过程的概率程序，其中包括恶魔的非决定性的模型。以及删除一些通常所需的条件平稳性，我们的generalisation允许发展一个完整的理论，连接固定的行为，长期的平均行为-后者是一个重要的属性，位于表达范围之外的标准逻辑的概率程序。关键词：概率程序语义，概率，恶魔不确定性，马尔可夫过程，平稳分布，马尔可夫决策过程。1介绍在执行过程中能够做出概率性选择的程序或进程表现出一系列（概率性）行为，这些行为超出了纯定性形式主义所能描述的范围;此外，即使是熟悉的程序逻辑的众所周知的定量适应-最重要的是概率时态逻辑[18，2]-在某些情况下仍然不够表达。其中之一是所谓的程序FP代表了一种简单的故障修复机制。它所描述的系统旨在重复执行，并且状态根据特定的概率语句而演变。FP的平均长期行为决定了（例如）状态正常的时间比例，并且总是定义良好的[4]。其他相关术语是在这种特殊情况下，初等分析表明，1这项工作是在英国牛津大学完成的，由EPSRC资助2 电子邮件地址：anabel@ics.mq.edu.au2000年1月，出版社dbyElsevierScienceB。 V. 在CC BY-NC-ND许可下开放访问。MCIVER270HH--FP：=如果可以然后（ok2/3ok）[]okelse（ok1/2ok）[]okFiok和<$ok切换对应于工作和中断行为的状态。运算符2/3记录概率更新，而[]记录非确定性更新。像这样一起使用，我们能够指定故障率的容差-在每次执行时，至少有1 / 2的概率重新建立ok（因为概率分支的唯一其他替代方案确定地建立ok）。Fig. 1. 抽象的故障修复机制平均至少有3/ 5的时间，但概率时间逻辑不能描述这种行为。(de Alfaro对这些问题进行了很好的讨论[3]。在初等概率论中，长期平均行为在某些特殊情况下由“平稳分布”决定虽然一些作者[10，16]使用马尔可夫过程作为概率程序的模型，但最近发现一种广义形式这就是我们将在这里使用的模型，我们将在第二节中给出详细信息。五、因此，我们的主要贡献（在第二。3)就是给出一个公理化的解释稳定的行为和收敛到它，一个扩展和简化的经典概念。我们的广义收敛概念不仅适用于所有马尔可夫过程（而不仅仅是某些特殊情况），而且它完成了将平稳行为与平均长期行为联系起来的理论。有关详情载于第五、我们发展我们的理论代数风格已经在理论的并发性，在那里它已被证明是一个强大的工具，用于分析不确定性的程序，重复执行。我们用“。” for function application; ≤, + and比”更多“，加法和最小值适用于实值函数。其中S是一个有限的状态空间，S是{F |S → [0，1]·s：SF.s = 1}，S上的（离散）概率分布集。对于实数k，我们把k写成值域为k的常数实值函数。如果α是S上的实值函数，则（α）和（α）分别表示当状态在S上变化时α所取的最大值和最小值;（kα）或k（α）表示函数α逐点乘以实数k。我们在需要时引入其他符号。MCIVER271⊕−HH±⊕¬±2概率顺序程序我们总结了概率规划的两个等价模型;更多细节在其他地方给出[13，9]。概率顺序程序的语义支持传统的编程控制结构的解释与二元概率选择算子p的结合，其中操作表达式Ap B的含义是执行A或B，概率分别为p或1p。由于没有确定的输出，这种行为有时被称为“概率非确定性”。然而，概率非确定性与“恶魔非确定性”非常不同这两个算子的模型非常不同-通常概率信息由最终状态的（输出）概率分布描述，而恶魔行为则由可能输出的子集描述。把这两个概念放在一起，就可以得到一个模型，在这个模型中，程序对应于从初始状态到最终状态上的分布集的函数，其中结果集的多重性代表一定程度的不确定性，而分布记录了不确定性得到解决后的概率信息。对于在抽象状态空间S，3上运行的程序，我们对概率程序空间S [9，13]有 以 下 定义 ，其对非确定性的处理类似于其他型号[2，15，4]：HS：= S→PS。更一般地说，像马尔可夫过程一样，S中的每个程序都可以被认为是初始状态上的概率分布的函数，但在这种情况下是最终状态上的概率分布集[9]。我们使用程序精化来排序程序，它比较了非确定性的程度--精化顺序越高的程序比下面的程序表现出更少的非确定性：Q± P i =（S·P.s <$Q.s）。经典的马尔可夫过程可以用“确定性”的子类来识别例如，（恶魔决定论的）程序ok1/2ok根本没有适当的精化。上面的一个结果是（最坏情况）随着程序变得更加精细，定量属性得到改善。如果Q保证以至少为p的概率建立一个谓词φ（不考虑非决定性），那么P也必须以至少为相同的p的概率建立φ。概率系统的观察观点（其中记录了输出的频率）更普遍地被“期望值”的概念所捕获Kozen是第一个在他的概率程序逻辑[3]这个基本模型也可以被增强，包括不终止[13]和奇迹[14]。MCIVER272不EE不H不± HT--E∫F（但对于确定性程序）。他的见解是将程序视为以目标导向的方式转换实值函数的运算符，就像标准程序可以被建模为谓词转换器一样[5]。使用实值函数而不是谓词允许表达式包含定量（以及定性）信息。这个想法已经被其他人[13]扩展到包括恶魔的非决定论以及概率。我们将S写为S上的实值函数（期望）的空间，并将S写为“期望变换器”的相关空间，定义定义2.1设r：S→P（S）是一个将S中的初始状态取为S上的最终分布集的程序。则在程序r的状态s处的最大有保证的前期望∫wp.r.s. s ：=（HF：r.s·α），F哪里α表示α相对于分布F的期望值。4我们说wp.r是对应于r的期望Transformer，我们定义TS为wp。HS.程序通过比较定性观察的结果来排序：因此t±tJi（tα：E+S·t.α≤tJ.α），在哪里+S表示非预期。 在使用““来表示S和S中的阶时，这是不连续的，因为定义对应于[13]。在特殊情况下，后期望取0， 1的值，因此表示谓词，前期望表示程序建立该谓词的最大保证概率。非决定论，如谓词变压器，解释恶魔。虽然这两种观点是等价的[13]，但我们通常使用S，因为它的算术性质使它比S更便于证明。S中的变换是连续的（在实值函数的意义上）和次可加的，即t. （kα+kJβ−kJJ）≥k（t.α）+kJ（t.β）−kJJ，在确定性程序（经典马尔可夫过程）的情况下，它可以被加强到可加性。我们将基本程序结构解释为对变换器的操作：因此（t; tJ）.α：=t。（tJ.α）;（t[]tJ）.α：=t.α[]tJ.α和（tp<$tJ）.α：=p（t.α）+（1−p）（tJ.α），由此我们可以看出决定论是[001 pdf 1st-31files]下一个引理可以用TS的概念非常简单地证明。定义规范||. ||α||：=（H α）-（H α）。||:= (Hα) − (Hα).我们的定义意味着∫4事实上Σα只是s：Sα.s×F.s，因为S是有限的，F是离散的[6]。公司现采用国际- 符号，因为它不那么混乱，并且与更一般的情况一致FMCIVER273不不||||H⊕如果||α||= 0，则α在S上是常数。引理2.2设t，tJ是TS中的期望变换. 如果t是决定性的，且tJ; t = tJ;而且如果存在某个0 ≤ c <1，使得对于任何α，我们有||t.α||≤ c||α||，则tJ是确定性的。证明：上 面 的讨论表明，我们只需要证明tJ是可加的，这是T S中变换的连续性。即使莱姆。2.2对于满足条件的S中的任何程序更普遍地成立，它实际上表征了马尔可夫过程是否收敛于其所谓的平稳分布的性质，即它的行为就像关于的收缩。.然而，术语相反，如果tn不是对t的任何幂的收缩，那么可以证明存在一些状态的真子集，它们对tn保持不变，对于一些人来说，这样的程序也被称为3“平稳行为”的程序代数处理在本节中，我们将研究重复执行的程序或系统的一些代数性质代数方法已经被证明在并发理论的发展中非常强大[1];我们发现它们在这种情况下也非常有效。我们的基本语言（图2）由两个二元运算符（“;"，顺序组合和“[]"，恶魔的非确定性选择），一个常数（1，“什么都不做”）和一个一元运算符（““，“Kleene星”）组成 两者;及[]是结合的，[]是交换的; 1是;的恒等式。观察到对于概率模型[]不能向左分布。（其他非概率性解释将允许完全分配[1]。我们将T S中的x∈解释为Transformer x∈.α：=（νY·α x; Y），5，它对应于从初始状态s输出最强不变状态集的程 序，S. 我们还将使用特殊的程序混沌，它表示对S中所有状态的非决定性选择。一个可以从所有初始状态到达所有状态的程序t（概率为1）没有适当的不变量，因此满足t=混沌。接下来，我们介绍我们的第一个推广-概率算子p;[19]他的作品也是在《易经》中出现的二、观察到，p∈ S对应于TS的次可加性。我们说S中的概率分布F相对于马尔可夫过程t是平稳的，如果每当输入状态分布为F时，5ν形成关于≤的最大不动点。MCIVER274⊕ ⊕ ⊕⊕−x±y惠x[]y=xx= 1 []x[]x;xx;（y[] 1）±x <$ x;y<$=xx;（y[]z）±x;y[]x;z x;y±y<$x <$;y=y（y[]z）;x=y;x[]z;xxpy=y1−pxx[]y±xpyx;yp<$x;z±x;（yp<$z）（yp<$z）;x =y;xp<$z;xxp（yq z）=（xpy）（p+qpq）z（p+q−pq）x，y，z被解释为TS中的程序，并且0

0）xx∞=xn∞为了避免混乱，我们写xn∞等。而不是（xn）∞。图三.基本定理你好 事实上，S中的t∞是递增的程序链的极限tt; t; t2. t; t n... 由于S是有向完备的，所以这个极限是有明确定义的，因此我们有另外的事实：（1）（n> 0·x≠ 0; xn± y）<$x∞±y.图3我们给出了关于∞和∞的一些一般定理，这些定理都是由的公理。2和在Def.3.1和（1）。为了了解λ和∞之间的区别，我们重新考虑图1中的FP。唯一的非平凡不变状态集是ok，ok，因此FP∞=ok [] ok;但这个程序相对于FP不是静止的，因此FP∞=FP∞。事实上，FP∞=（ok3/5ok）[] ok，在广义分布中，ok的概率至少是3/5。4扩展马尔可夫理论从（1）很容易看出，在一般情况下，任何程序t（如果执行足够长的时间）都实现了由程序t∞封装的某种稳定行为的概念。但这并不是经典马尔可夫过程理论的观点。去看看一般的和古典的神学-列发散，考虑程序b：= 1 b，其中变量b只能取0和 1中的值。经典理论认为这个程序不会收敛（因为它在b的两个值之间振荡）。 另一方面，（b：= 1 b）∞=（b：= 1b）∞=（b：= 0 []b：= 1），这意味着长期平稳行为是一个程序，它从它的类型非确定地分配给b。这种行为是不符合经典理论的，因为它不是确定性的，因此不表示分布。 我们将在下一节讨论这个解决方案背后的现在，我们在结束这一节时，要证明我们的广义收敛概念确实取代了经典理论。本文给出了关于收敛于平稳分布的重要结果的一个新的证明MCIVER276不不证明关键依赖于假设所有马尔可夫过程都回想一下，分布被建模为独立于初始状态的确定性分配。对应于这样一个分配的一个Transformert是可加的，并且对于任何α，期望t.α是一个常数函数。例如WP。（ok2/3ok）.α返回期望（最终）值α的值为2（α.ok）/3+ α。（<$ok）/3，无论初始值如何。因此，在我们的术语中，我们所需要做的就是证明∞将非周期确定性程序映射到对应于确定性as的变换器- 是的非周期性是t的一个性质，前提是所有状态最终都可以从所有其他状态到达，并且以有限周期返回到原始状态的概率严格小于1 [8]。第一个性质相当于说t=混沌，第二个性质相当于说tn=t对于所有n>1-在等式对于某个n失败的情况下，我们说，t的周期为n。关于马尔可夫过程收敛的一般定理如下。定理4.1若S中的t是确定的非周期的，则t∞是确定的分配.证明：Lem之后的评论。 2.2意味着t n必须是某个n> 0的压缩，因此t n∞必须是确定性分配（也由Lem. 2.2）。结果由图3得出，因为t n= t。5长期平均行为的应用无限执行的系统的性质通常使用时态逻辑的适应来研究-在我们的情况下是概率时态逻辑。公式在执行路径树上进行解释-在我们的情况下，执行路径上的概率分布[15，2]。在路径分布上解释一个典型的公式φ，得到满足φ的路径的比例。然而，正如de Alfaro所指出的，这种但这正是对失效系统的可用性或长期平均分析在这一节我们将说明，即使对于包括非确定性的系统，如图1中的FP，两者都由t∞1.一、我们像de Alfaro [3]那样定义长期平均行为给予期望的序列化，使序列化的元素，并部分和k seq = seq1+ seq2+. + seq k.定义5.1设t在S中无限地执行，α是一个谓词。当t执行时，观察到α保持不变的长期平均出现次数MCIVER277−−HE- -不由Vt.α给出，Vt.α：=liminfΣkSeq，其中，在这种情况下，seqk：=tk;tk.α。k→∞k定义5.1对应于在t重复执行时以任意时间间隔采样系统状态之后的平均结果。这里我们假设在第k个 当t对应于经典收敛的马尔可夫过程，平均值为由平稳分布决定。我们在这里有一个相应的结果，但它对所有程序都有效。引理5.2设t是S中的规划，α是S中的期望。 则我们有t∞.α=VP.α。为了说明上述情况，回想一下程序b：= 1b，并让[b= 0]表示期望值，在b为0的状态下为1，在其他状态下为0。 TocalculateVb：=1−b. [b=0]我们认为wp. （b：= 1−b）n;（b：= 1−b）n. [b=0]=0，因此Vb：=1−b。[b=0]=0aswell.或者，（b：= 1 b）∞=（b：= 0[] b：= 1），因此是wp。（b：= 1b）∞. [b= 0] = 0。这些结果可以在测试人员的上下文中操作地理解，测试人员可以选择何时对程序的状态进行采样。 明确如果测试器仅在偶数次执行b：= 1之后观察状态那么他将推断出b平均值永远不会为0（甚至根本不会）。经典理论中关于非周期规划的观点是，平均测量在某种程度上对这种偶然的测试偏差是鲁棒的。 和这同样适用于这里：无论拟议的测试制度，由于FP∞=（ok3/5），因此FP是ok的时间的至少为3<$ok）[]ok.6结论我们的主要贡献是扩展马尔可夫过程的平稳行为的概念，包括恶魔的非决定性的模型，设置它与其他编程概念。主要的见解是将静态行为明确地建模为S中的分布生成程序;这允许访问程序代数和概率模型的技术[1，13]。这里所提出的推广使得将长期平均行为和平稳行为联系起来的理论得以完成--两者现在总是被定义的，而且它们相互决定。此外，我们的推广提供了一个惊人的简化经典理论的收敛。MCIVER278这里提出的算子t_n不能表达de Alfaro [3]提出的更详细的框架所描述的许多的主要区别在于结果被分配给状态而不是转换。然而，许多有用的业绩衡量标准都包含在这个更简单的框架中。例子包括平均等待时间和可用性措施。需要进一步的工作来整合其他编程概念，如“子”[12]，它显着提高了代数推理的能力一个重要的结果是，静态行为现在容易受到其他编程技术的影响，例如精化和数据抽象[7]。引用[1] 厄尼·科恩。分离和还原。在数学的程序建设，第五届国际会议，葡萄牙，2000年7月，第1837号在LNCS，第45Springer Verlag，2000年。[2] L. 德·阿尔法罗性能和可靠性规范的时序逻辑1997年STACS '97会议录[3] L.德·阿尔法罗如何指定和验证仿射系统的长期平均行为。1998年6月23日至24日，印第安纳波利斯，“LICS”98会议记录[4] C.德曼 有限状态马尔可夫决策过程 中国科学院出版社，1970年.[5] E.W. 迪 杰 斯 特 拉 程 序 设 计 的 一 门 学 科 。 Prentice Hall International ，Englewood Cli Jersey，新泽西州，一九七六年[6] W. 费勒概率论及其应用导论第一卷Wiley，第二版，1971年。[7] P. H. B. Gardiner和C.C. Morgan. 同品种变压器的数据细化理论计算机科学，87：143[8] G. Grimmett和D.威尔士语概率：一个介绍。牛津科学出版社，1986年。[9] 何继锋，K. Seidel和A. K.麦基弗保护命令语言的概率模型。Science ofComputer Programming，28（2，3）：171[10] D.浩善概率程序的语义。计算机与系统科学杂志，22：328[11] D.浩善Kleene代数与正则事件代数的完备性定理。信息与计算，110：336[12] C. C. Morgan. 从规范编程。Prentice-Hall，第二版，1994年。MCIVER279[13] C. C.摩根A. K. McIver和K.赛德尔 可能是同品种变压器。ACM Transactionson Programming Languages and Systems，18（3）：325 - 353，May 1996.[14] C.C. Morgan.私人交流。一九九五年[15] R.塞加拉随机分布实时系统的建模与验证。博士论文，1995年。[16] M. Sharir，A.Pnueli和S.哈特验证概率程序。SIAM Journal on Computing，13（2）：292[17] N. Storey. 安全关键计算机系统。Addison-Wesley，1996年。[18] M.瓦迪概率并发有限状态系统的自动验证。第26届IEEE计算机科学基础研讨会论文集第327-338页