PMAUDE：基于重写的概率对象系统

理论计算机科学电子笔记153（2006）213-239www.elsevier.com/locate/entcsPMaude：概率对象系统GulAgha1Jos'eMeseguer2KoushikSen3美国伊利诺伊大学香槟分校计算机科学系摘要我们介绍了一种基于重写的规范语言，用于建模概率并发和分布式系统。 该语言基于PMAUDE，既有严格的形式， 一种基于规则的高级程序设计语言的基础和特点。 此外，我们还提供工具支持，用于对用PMAUDE编写的模型进行离散事件模拟，并根据通过离散事件模拟生成的样本对此类模型的各个定量方面进行统计分析。由于分布式和并发通信协议可以使用Actor（具有异步消息传递的并发对象）建模，因此我们提供了一个ActorPMAUDE模块。该模块有助于以概率演员形式主义编写规范。这使我们能够轻松地编写纯粹概率性的规范，而不仅仅是非确定性的规范。概率系统中这种（未量化的）非决定性的缺失，对于我们也讨论过的一种统计分析形式来说是必要的。 具体来说，我们引入了一种称为定量时态表达式（Quantitative Temporal Expressions，简称QUA TEX）的查询语言，用于查询概率模型的各种定量方面。我们还描述了一种统计技术来评估QUA TEX表达式的概率模型。关键词：规范语言，PMAUDE，演员，概率规范，非确定性规范，查询语言，QUA TEX1引言在对大规模并发系统进行建模时，考虑系统中影响事件的不同因素之间复杂的相互作用是不可行的例如，在像因特网这样的大规模计算机网络中，网络延迟，1电子邮件地址：agha@cs.uiuc.edu2 电子邮件地址：meseguer@cs.uiuc.edu3电子邮件地址：ksen@cs.uiuc.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.040214G. Agha等人/理论计算机科学电子笔记153（2006）213拥塞和故障以使得确定性地对系统建模不可行的方式相互影响。然而，非确定性模型不允许我们推理系统的可能行为;概率建模和分析是理解这种行为所必需的。一个概率模型允许我们量化并发系统中的不确定性的来源行为的确切持续时间通常取决于负载、负载等。并且可以由随机过程表示进程或网络故障可能以一定的速率发生。随机性也可以显式地出现：系统的某些部分可以实现随机算法。关于概率系统的模型已经有了相当多的研究轻量级的形式主义，如UML和SDL的扩展和严格的形式主义基于进程代数[17，16]，Petri网[23]和随机自动机[13]已经提出并成功地用于建模和分析概率系统。轻量级的形式主义更接近编程语言，易于工程师学习;然而，有些可能缺乏严格的语义。另一方面，严格的形式主义对于工程师来说可能过于繁琐。为了弥合轻量级和严格的形式主义之间的差距，我们提出了一个基于重写的规范语言，称为PMAUDE，用于指定概率并发系统 PMAUDE，这是基于概率重写理论，既有严格的形式基础，高级编程语言。4此外，我们还提供了工具支持，用于对用PMAUDE编写的模型进行离散事件模拟，并对此类模型的各种定量方面进行统计此外，由于各种分布式和并发通信协议可以使用异步消息传递并发对象或Actor [2，4]进行建模，因此我们提供了一个ActorPMAUDE模块，以帮助以概率-Actor形式主义编写规范。我们的PMAUDE语言扩展了支持概率的标准重写理论重写理论[24]已经被证明是一个自然和有用的语义框架，它统一了不同类型的并发系统[24]，以及实时模型[27]。Maude系统[11，12]为重写理论提供了一个执行环境。PMAUDE的离散事件模拟器已被实现为Maude的扩展。ActorPMAUDE扩展了并发计算的Actor模型[2，4]通过允许我们明确地将概率分布与时间联系起来，[4]请注意，还有其他形式主义，它们既提供了严格的形式基础，又提供了高级编程语言的特征[22，9]。PM从他们那里得到了启发，因为它扩展了重写理论，而不是扩展了基于过程代数或自动机的形式主义。G. Agha等人/理论计算机科学电子笔记153（2006）213215消息延迟和计算。Actor是固有的自治计算对象，它们通过发送异步消息相互交互。角色模型已经被形式化并应用于可靠计算[33]和软件架构[5]。在actorPMAUDE中编写规范的一个动机是，它允许我们轻松地编写没有未量化的非确定性的规范。在第3.1节中，我们概述了一些简单的要求，这些要求确保用actor PM AUDE编写的规范没有未量化的非确定性，即所有的非确定性都被量化的非确定性所取代，例如概率选择和随机实时。不存在（未量化）非决定论对于我们提出的统计分析是必要的这种分析技术扩展了现有的数值和统计模型检查技术[8，22，30，31]。特别是，在我们的统计分析中，我们允许评估定量的时间表达式，称为QUA TEX，这使我们能够获得更多的定量洞察概率模型比什么是可能使用传统的模型检查的时间属性。本文的贡献如下1. 我们介绍PMAUDE，一种用于编写概率重写理论规范的语言我们还解释了如何在底层Maude语言中模拟PMAUDE2. 我们提供了一个演员扩展的概率重写理论，我们声称是一个自然的模型来编写各种概率网络协议。这个扩展也帮助我们写出不受非决定论约束的规范这对于我们所介绍的统计分析的形式是必不可少的。3. 我们引入了一种新的查询语言QUATEX来编写定量时态表达式，该表达式可用于查询概率模型的各个定量方面，而没有非确定性。 我们描述了一种统计技术来评估这样的表达式，使用离散事件模拟。我们已经将该技术作为工具VE ST A的一部分实施。此外，我们描述了PMAUDE与VE ST A的集成。本文的其余部分组织如下。第2节介绍了PMAUDE及其基本的形式主义和从PMAUDE模块到标准Maude模块的翻译器。在第3节中，我们描述演员PM奥德模块的例子。我们在第4节中介绍了Q UA TE X和Q ua TE x的统计评估技术，然后是结论。216G. Agha等人/理论计算机科学电子笔记153（2006）2132PMaude及其形式主义基础在本节中，我们介绍PMAUDE及其潜在的形式主义开始-与一个简短的底漆上下午奥德和一个例子。这之后是正式介绍概率重写理论以及背景概念和符号。然后，我们解释如何在底层Maude语言中模拟PMAUDE中指定的概率模型概率重写理论的形式主义，以保持文件的独立性。关于形式主义的进一步细节可以在[20，21]中找到。读者可访问第2.5节跳过了第2.2节、第2.3节和第2.4节中给出的形式主义，而没有失去连续性。2.1关于PMAUDE在标准的重写理论[11]中，系统中的转换由以下形式的标记条件重写规则（关键字crl）描述：crl[L]：t（−→x）<$tJ（−→x）ifC（−→x）（1）这里我们假设条件C是纯等式的。直观地说，一个条件规则（与labelL）的hsformspeciesapat ternt（−→x）suchthat如果系统状态的某个片段模式tJ（−→x）可以表示平面。在概率重写规则中，我们添加概率这些规则的信息具体来说，我们提出的概率规则的形式，crl[L]：t（−→x）<$tJ（−→x ，−→y）ifC（−→x）其中概率y−→y：=π（−→x）（2）当h和side在tJ（−→x ，−→y）中出现一些新的变量−→y时，在t j（−→x，− →y）中的变量s在h和sidt（−→ x）中的取值是−→x. 当然，它不需要在−→x中的所有变量，也不需要在J（−→x ，→−y）中的所有变量。如果对于可变s−→x，这里有一个子s ∈θ，则规则将使得有一个静态框架这使得θ（t）等于状态片段，条件θ（C）为真。因为righh和sidetJ（−→x ，−→y）may有一个新的变量s−→y，所以下一个状态不是唯一确定的：它取决于为variables−→y选择一个额外的subsp。ρ的选择是根据概率函数π（θ），其中π不是固定的概率函数，而是函数族：其中一个是对变量s−→x的替换θ。重要的是要注意，我们的概率重写理论概念可以用以下方式G. Agha等人/理论计算机科学电子笔记153（2006）213217pmod指数时钟是* 以下导入保护POSREAL的正实数模块。* 以下导入定义分布指数的PMaude模块，* Bernoulli，Gamma，etc.保护PMAUDE。*** clock sort Clock。* 为Clock* 声明了一个坏时钟操作中断：PosReal PosReal →时钟。* T用于表示时钟的时间，* C表示时钟电池的电量*t表示时钟变量T C t：PosReal的时间增量。var B：Bool.操作时钟：PosReal PosReal →时钟。rl [advance]：clock（T，C）如果B，则时钟（T+t，C-C）1000其他 断裂（T，C-C）1000Fi其中概率yB：=Bernoulli（C）且t：=指数（1. 0）。1000endpmrl[reset]：clock（T，C）时钟（0.0，C）。Fig. 1. 说明概率非确定性系统意义：在并发系统中，在任何给定的点上，许多不同的规则都可以被触发。在概率重写理论中，选择哪些规则将被触发是不确定的。一旦在给定位置选择了一般形式（2）的给定概率规则的匹配θ，则随后的对于可变s−→y，使子sp可用于概率分布函数π（θ）。图1，我们通过一个简单的例子来说明非决定论和概率之间的相互作用，PM奥德，模拟一个电池操作的时钟与复位按钮。 PM AUDE中的注释以 * 开头。实施例2.1.图中的模块1导入模块POSREAL和PMAUDE，分别定义正实数和概率分布。处于正常稳定状态的时钟表示为术语clock（T，C），其中T是时间，C是表示时钟电池中剩余电荷量的实数。关键规则是advance，它有一个新的布尔变量B和一个正实数变量t在它的右边。如果一切顺利（B =218G. Agha等人/理论计算机科学电子笔记153（2006）21310001000→∈∈--如果B = true），则时钟将其时间增加t，并且电荷略微减少，但是如果B =false，则时钟将进入中断状态（T，C-C）。这里二元变量B（在这种情况下为布尔值）根据平均值为C的伯努利分布进行分布。因此，B的值在概率上取决于电池中剩余的电荷量：电池中剩余的电荷越少，时钟中断的机会就越大 这样，PM AUDE支持离散时间马尔可夫链中的离散概率选择。另一个额外的变量t在规则推进的右手边，按照速率为1的指数分布进行分布。0.因此，PM奥德也允许我们在连续时间马尔可夫链中发现随机连续时间模型。 重置规则，将时钟重置为时间0。0，在其右侧没有任何额外的变量，因此是标准的重写规则。给定一个时钟表达式clock（T，C），两个规则中的一个前进，或者复位被非确定性地选择以应用于术语clock（T，C）。如果选择了规则提前，则时钟按概率提前执行PMAUDE模块需要将其转换为相应的响应Maude模块，模拟其行为，如第二节所述。第2.5条。然后，可以通过给出具有初始基础项的重写命令来获得样本执行，例如时钟（0）。0， 1000）。结果将是一个执行，其中关于应用哪个规则的不确定性由公平调度器解决，但是高级规则的每个应用都概率性地选择B和t的值2.2背景和注释一个隶属方程理论[26]是一个对（k，E），其中k是一个由K个种类组成的签名，对于每一个种类k∈K，一个S k的种类，一个f：k1. k n k，其中k，k1，.，k n K，其中E是一组条件条件λ-方程和λ-隶属度，其形式为（−→x）t=tju1=v1.. . un=vn . wm：sm（−→x）t：su1=v1.. . un=vn . wm：sme−→x表示t中的变量i，tJ，ui，vi和wja ove。一个member-shipw：s，其中w是k类的项，s Sk断言w有s类。没有排序的术语被认为是错误术语。这使得成员资格方程理论能够在一个整体框架内指定部分函数一个X-代数B由一个K-指标集族X=Bkk∈K组成，并且(i) 对于ea chf：k1. . . Kn→k在函数fB：Bk1×. . ×Bkn→Bk(ii) 对于每个k∈K和每个s∈Sk，有一个子集Bs<$Bk。G. Agha等人/理论计算机科学电子笔记153（2006）213219FP我们用T表示隶属方程签名的项的代数。隶属方程理论（E，E）的模型是满足方程E的那些λ-代数.隶属方程逻辑的推理规则是可靠的和完备的[26]。任何隶属方程理论（E，E）都有一个初始项代数，记为T/E，使用隶属方程逻辑的推理规则并假设T无歧义 [26]，它被定义为项代数T的商，由• tEtJ惠Et=tJ• [t]E∈T/E，s惠Et：s在[10]中，关于方程简化、连续性、终止性和排序递减性的通常结果以一种自然的方式被推广到隶属方程理论。在这些假设下，隶属度方程理论可以通过使用从左到右的方程进行方程简化来执行，也许模一些结构公理A（例如，结合性、交换性和同一性）。具有方程E和结构轴A的初始代数记为T，EA.如果E是连续的，终止的，并且是减序模A[10]，则模A的完全单化项（标准型）的同构代数记为Can_n，E/A。符号[t]A表示由方程E完全简化的项t的A-等价类。在标准的重写理论[24]中，系统中的转换由以下形式的标记条件重写规则描述crl[L]：t（−→x）<$tJ（−→x）ifC（−→x）在tuitively，一个规则（与labelL）的s或mspecif is是一个pat ternt（−→x）uch，如果一些片段的系统的状态匹配该模式，并条件C，则该状态片段的局部转移，变为p模式tJ（-→x）c可以占据位置。Maud系统[11，12]提供了一个隶属关系方程理论和形式为（E，E，R）的重写理论的执行环境，其中（E，E）是隶属关系方程理论，R是条件重写规则的集合。Maude规范的几个例子可以在[25，12]中找到。为了简洁地定义概率重写理论，我们使用测度理论中的一些基本集合X上的σ-代数是X的子集的集合，包含X本身，在补和有限或可数的有限并下闭。例如，集合X的幂集（X）是X上的σ-代数。σ-代数的元素称为事件。我们用BR表示R上包含集合（−∞，x]的最小σ-代数，对所有x∈R.我们还提醒读者，概率空间是一个三元组（X，F，π），F是X上的σ-代数，π是概率测度函数，定义在σ -上。220G. Agha等人/理论计算机科学电子笔记153（2006）213∈∈→∪代数F，在X上的值为1，并且通过加法分布在不相交事件的有限个或可数个并集上对于X上的给定σ-代数F，我们用PFun（X，F）表示集合{π|（X，F，π）是概率空间}2.3概率重写理论接下来，我们在下面的定义之后定义概率重写理论定义1（E/A-正则基代换）对变量− → x的E/A-正则基代换是一个函数[θ]A：−→x→Cann，E/A。We对这样的函数使用符号[θ] A，以强调E/A-正则型结构是由一个n或n-正则型结构θ：−→x然而，对于每个x，−→x，θ（x）完全由Em od uloA简化。对于eac rulex，[θ]A=[ρ]Ai−→x，[θ（x）]A=[ρ（x）]A。 我们使用CanGSubtE/A（−→x）来确定变量− → x集合的所有E/A-正则化子集的集合。直觉的E/A-规范基替换表示用项代数T的基项替换相应种类的变量，使得所有项已经尽可能地通过方程E模结构公理A来约简。例如，替换10。0 ×2。0对于排序PosReal的变量不是规范基替代，替代20。0是一个典型的地面替代。现在我们继续定义概率重写理论。定义2（概率重写理论）概率重写理论是一个4元组R=（R，E<$A，R，π），其中（R，E<$A，R）是一个重写理论，规则r∈R的形式为：L：t（−→x）−→tJ（−→x ，→−y）如果C（−→x）哪里• −→x是t中的变量集，• −→y是tJt中不存在的变量的集合;因此，tJ可能有与t−→x−→y相同的变量;然而，并非所有变量都是必需的在−→xoccurintJ中，• C是一个条件的形式（10 -12-2013（kw k：s k），即， C是方程和隶属度的结合，以及uj，vj中的所有变量且wkarein−→x，并且π是一个函数，为每个重写规则r∈R分配一个函数G. Agha等人/理论计算机科学电子笔记153（2006）213221F−→∈1000πr：[[C]]→PFun（CanGSubstE/A（−→y），Fr）其中re[[C]]={[μ]A∈Can GS ubs tE/A（−→x）|E<$A<$μ（C）}是X的E/A-典型替换满足条件C，且r是CanGSubs tE/A（−→y）上的σ-代数。我们不能让她坐在这里函数πr，记作crl[L]：t（−→x）<$tJ（−→x ，−→y）ifC（−→x），概率y−→y：=πr（−→x）如果集合CanGSubstE/A（−→y）是有效的，因为us e−→y是有效的，那么πr（−→x）被称为定义了一个平凡分布;这对应于普通的重写。规则没有任何可操作性。 如果−→y是非空的，则yb utGS u b tE/A（−→y）是空的因为使用该资源对我来说是不可能的−→ybecausetthe e cor re-响应排序或种类为空，则该规则被认为是错误的，并且将在语义中被忽略。我们将概率重写理论类表示为PRwTh。对于例2.1中的具体化，规则推进在右侧有两个变量B和tB的可能替代是真和假，其中真以概率C被选择。类似地，t的可能替代是从速率为1的指数分布中采样的正实数。0.2.4概率重写理论设R=（E，E，A，R，π）是概率重写理论，使得：(i) E是连续的，终止的和排序递减模A[10]。(ii) 规则R与E模A是一致的[11]。定义3（上下文）上下文C是一个单次出现一个变量的项，称为孔。 两个上下文C和CJ是A-等价的当且仅当A）C = CJ.注意，上面定义的上下文的A-等价关系是上下文集合上的等价关系。我们使用[C]A表示包含上下文C的等价类。定义4（R/A-匹配）给定[u]A∈C，E/A，它的R/A-匹配是三元组（[C]A，r，[θ]A），其中如果r∈R是规则rl[L]：t（−→x）−→tJ（−→x ，−→y）ifC（−→x）其中概率y−→y：=πr（−→x）222G. Agha等人/理论计算机科学电子笔记153（2006）213∈ Ⓢ ←R则[θ] A[[C]]，即[θ] A满足条件C，且[u] A=[C（θ（t））] A，因此[u]A是将θ应用于termt（−→x）并将其置于tex t上的c的结果。例如，R/A-匹配术语clock（75. 0800。0）在示例中2.1 具体如下：• （[]A，advance，[T ← 75. 0，C ← 800。0]）• （[]A，reset，[T ← 75. 0，C ← 800。0]）定义5（E/A-规范一步R-重写）E/A-规范一步R-重写是以下形式的标记转换（[C]A，r，[θ]A，[ρ]A）[u]A−→[v]A哪里(i) [u]A，[v]A∈Can，E/A(ii) （[C]A，r，[θ]A）是[u]A的R/A-匹配(iii) [ρ]A∈CanGSubstE/A（−→y）（iv）[v]A=[C（θ←tJ（θ（−→x），ρ（−→y）]A上述定义描述了PRwTh的一步计算中涉及的步骤。首先，为r的左侧非确定地选择R/A匹配（[C]A，r，[θ]A），然后为新在r的右边，varables−→yπr（[θ]A）。然后将这两个子位置应用于项TJ（−→x ，−→y），产生最终项v，其等价类[v]A是计算步骤的结果与R/A匹配的选择相关的非确定性必须被移除，以便在计算空间上关联概率空间（这是规范的一步重写的有限序列非确定性被所谓的系统对手消除，它定义了R/A匹配集的概率分布。在[20]中，我们描述了计算路径集合上概率空间的关联我们在[20]中也证明了概率重写理论具有很强的表达能力。它们可以表达概率系统的各种已知模型，如连续时间马尔可夫链[ 32 ]，概率非确定性系统[ 28，29 ]和广义半马尔可夫过程[14]。2.5在Maude模拟PMAUDE由于其非确定性，概率重写规则不能直接执行。例如，考虑例2.1中的提前规则，G. Agha等人/理论计算机科学电子笔记153（2006）2132231000时钟。在它的右边有两个新的变量，即布尔变量B，它将决定时钟是继续正常工作还是中断，以及正实数变量t，它将决定时钟的实际时间提前。然而，PMAUDE中指定的概率系统可以在Maude中模拟。这是通过将PMAUDE规范转换为相应的Maude规范来实现的，其中新变量的实际值出现在概率重写规则的右手侧的分布函数是通过对相应的分布函数进行采样而获得的。例如，在我们的时钟示例中的前进规则中，布尔变量B必须根据伯努利分布BERNOULLI（C）进行采样，而正实变量必须根据指数分布EXPONENTIAL（1）进行采样。0）。这种理论转换使用三个关键的Maude模块作为基本的基础结构，即COUNTER、RANDOM和SAMPLER。COUNTER模块为非确定性重写规则的应用提供了内置策略：rl计数器N：Nat.将常量计数器重写为自然数。内置策略应用此规则，以便应用规则后获得的自然数恰好是前一个规则应用中获得的值的后继RANDOM模块是一个内置的Maude模块，提供了一个称为random的随机数生成器函数。SAMPLER模块为不同的概率分布提供采样功能。在上述高级规则中，所需的采样函数是指数运算：PosReal → PosReal。OP BERNOULLI：PosReal→Bool.SAMPLER模块中的关键规则是rl[rnd]：rand浮点数（random（counter+1）/4294967296）。其将常数RAND重写为根据均匀分布伪随机选择的0和1之间的浮动点数该浮动点数是通过将有理数随机（计数器）+1）/ 4294967296转换为正实数，其中4294967296是随机函数可以达到的最大值定义EXPONENTIAL和BERNOULLI采样函数语义的重写规则rlEXPONENTIAL（R）（- log（rand））/R。rlBERNOULLI（R）如果rand

下载后可阅读完整内容，剩余1页未读，立即下载