随机并发约束程序设计

理论计算机科学电子笔记164（2006）65-80www.elsevier.com/locate/entcs随机并发约束程序设计卢卡·博尔托鲁西1意大利乌迪内大学数学与计算机科学系摘要我们提出了一个随机版本的并发约束编程（CCP），在那里我们将速率与约束存储交互的每个基本指令。 我们给出了一个操作语义，可以提供一个离散或连续的时间模型。 观测量的概念进行了讨论，无论是离散和连续的版本，并给出两者之间的连接。最后，一个可能的应用建模生物网络。关键词：并发约束编程，随机语言，概率语义，连续时间。1介绍并发约束编程[22]（CCP）是一种基于“存储为约束”思想的语言。 它具有简单进程代数的语法，但具有在约束系统上工作的能力，这是一种存储器形式，其中存储了对变量的约束，并且信息被单调地细化。在其15年的生命中，它在不同的方向上得到了扩展：时间语义[23]，分布式设置[15]，以及（离散时间）概率语义[10，9]，仅举几例。它的名声可以与它的逻辑简单性有关，允许对并发性进行推理，并且与约束系统的力量有关，能够用合理的e-排序来建模复杂的程序在这项工作中，我们扩展了[10]，通过给出一个不同的概率语法和语义，可以模拟离散和连续时间，允许更精细的形式的定量分析CCP程序。这种扩展的基本思想是为与约束存储器交互的每个指令分配速率，即，询问、告知和过程调用。这里的价格是1电子邮件：luca. dimi.uniud.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.01266L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65函数为约束存储的每个配置分配一个正实数。这种选择导致了一种灵活的语言，它将在后面介绍的应用程序中得到利用。通过在特定状态下启用的不同询问、告知和过程调用代理之间的竞争条件来获得随机行为。执行最快的进程，重新开始新的比赛。通过这种方式，我们给出了连续时间语义，与随机π-演算[19]，PEPA [17]，EMPA [2]或pKLAIM [8，7]相同。另一方面，我们可以把速率看作是赋予指令的权重或优先级，因此我们可以将活动代理的速率归一化，并将执行概率与它们中的每一个相关联，从而获得离散的概率计算。因此，可以使用相同的语法对连续时间和离散时间进行建模。为了恰当地捕捉这两种不同的行为，我们定义了一个抽象的多变迁图，然后用所选择的时间模型将其具体化。我们的方法存在一些技术问题，特别是有关 隐藏操作符：我们不将任何速率与之关联，因此在开始任何竞争条件之前必须将其“移除”。这是通过跟踪局部变量集的配置来解决的，并通过用新的自由变量替换隐藏变量来解决。将这里提出的离散时间语义与[10]中开发的语义进行比较，我们注意到主要的区别在于概率的分配方式。在[10]中，每个求和和并行组合都给出了概率分布，迫使参数化地定义这些运算符及其语义w.r.t.所涉及的进程的数量，从而失去了它们的一些代数性质（即结合性）。相反，将优先权赋予指令，使我们摆脱了这种限制（见第4节）。此外，我们可以在同一个框架中同时拥有离散和连续的时间模型。这种新语义的引入有几个动机。 首先，可以应用性能分析中开发的广泛技术，以便从程序中提取信息其次，扩展了建模能力，但保持了语法的简单性特别是，CCP的这种随机版本可以用于模拟生物系统，如代谢途径，信号级联，基因调控网络等，几乎与随机π演算[19]用于此任务的方式相同[20]。其基本思想是用过程来识别生物实体，并将它们的相互作用建模为一种通信形式，详见第6节。本文的结构如下。第二节回顾了一些初步概念。在第3节中讨论了语言的语法，以及处理隐藏删除的机制。第四节介绍了操作语义，第五节介绍了时间模型和可观测量的概念。最后，在第6节中，我们暗示了该语言在生物系统建模中的可能应用，在第7节中，我们讨论了一些相关的工作，在第8节中，我们得出了一些最终的结论。L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6567程序=D. AD = ε| D.D|p（x）：−AM = tell λ（c）.A|问λ（c）.A|M1 +M2A = 0|[p（x）] λ|M|阿克斯A|（A1至A2）表1随机CCP2预赛约束系统是CCP的基本组成部分之一，它们被定义为（参见。[6]或[24]）作为完全代数格，其中±的序由蕴涵关系的逆给出。通常，这样的约束系统是从一阶语言和解释中导出的，其中约束是语言的公式，并且如果每个满足c的赋值也满足d，则约束c引起约束d，c≠d。在这种情况下，我们写d±c。很明显，在每个实际实现中，谓词必须是可判定的。此外，为了对隐藏和参数传递进行建模，先前的晶格被丰富为圆柱形代数结构（参见图1）。[16]），即具有圆柱化算子和对角元素。形式上，约束系统C =（Con，Con0，V，±，H，T，n，nx，dxy）是一个完全代数格，其中Con是约束集，按±排序，Con0是有限元素集，H是最小上界（lub）运算，V是变量集，T和n分别是底部和顶部元素，{n x，n x，dxy|x ∈ V}是柱面化算子，{dxy|x，y ∈ V}是对角元素。使用约束系统时的一个重要工具是约束中变量的替换，允许以简单的方式对隐藏和递归调用进行建模。我们可以将替换看作映射f：V → V，其中|f（x）= f（x）|∞.|<∞.形式上，给定一个约束c，以及两个变量向量x <$fv（c）和y，我们将c中x与y的替换定义为约束c[x/y]=<$α（y=αH<$x（α=xHc）），其中hα<$（fv（c）<$y< $x）=<$and|α|为|X|为|y|. 置换满足一些基本性质，参见。[12]详细的评论。 特别地，如果f是 一个 双线 性 映射 ，则f（x）c[f]=（xxc）[f]，即. e. bounded变量总是可以重命名的。3语法表1给出了演算的语法。指令基本上是CCP的指令，并引入了比率λ。特别是，利率增加到三个68L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65指令，即询问，告诉和递归调用。速率是一个函数λ：C →R+，给约束存储的每个配置分配一个正实数。 我们可以将这些数字视为优先级，诱导离散概率分布（通过归一化），或者视为[17]意义上的速率，表示与相应指令相关的“速度”，其中速率越高，速度越高。当然，在第二种情况下，我们主要考虑的是连续时间模型，因此这些速率将被分配给指数分布，因此它们决定了要执行的指令所使用的时间特别地，我们可以将速率视为在单位时间内执行指令的预期次数在连续时间的情况下，将速率粘合到询问和告知操作背后的基本原理是，这些指令在系统的约束存储上操作，因此它们实际上需要一定量的时间来执行。这个时间可能取决于要被告知的约束的复杂性，或者取决于蕴涵关系的有效计算的复杂性。此外，我们可以认为系统需要时间来计算约束系统中的最小上界运算，因为这对应于约束传播的一种形式。此外，这些操作所需的时间可能取决于约束存储的当前配置;例如，存在的约束越多，计算蕴涵关系就越困难，参见。[1]关于约束传播的参考。请注意，还有一个与过程调用相关的速率。这可能是有问题的，但事实上，这样的操作也有成本：进程必须访问存储声明的存储库，并且它必须用指定的变量替换自由变量此外，这个假设是必要的，以避免在过渡系统中的无限分支，参见。下面这种对速率的双重解释在研究离散和连续时间模型之间关系的共同框架的定义中找到了其动机。唯一没有速率的规范指令是隐藏运算符。我们真的认为局部变量的声明是一个太简单的操作，不需要给它分配一个速率，但是，我们希望有一个语义，每个转换都有一些概率信息附加到它，所以不给隐藏速率意味着我们需要一个机制来隐藏转换系统之外的变量。从本质上讲，我们通过用一个新的隐藏变量替换一个隐藏变量来实现这一点，并保证没有其他代理可以访问它。最后，我们观察到，选择运营商是由要求和告诉指示，在通常的实践中，只要求代理人守卫。这并不麻烦，因为ask和tell总是通过竞争条件（由它们的速率决定）进行竞争，而且，我们总是可以认为tell代理前面有一个总是启用的askλ（T）指令。在表2中，我们定义了代理之间的一致关系。前三条规则简单地说明了平行算子是施事空间中的交换幺半群，而接下来的三条规则则暗示了选择算子的相同性质。最后三条规则处理隐藏运算符的一些基本属性。我们L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6569（CR1）A1（A2A3）（A1A2）A3（CR2）A1A2A2A1（CR3）A10A1（CR4）M1+（M2+M3）（M1+M2）+M3（CR5）（CR6）M1+M2=M2+M1M1+0M1（CR7）x（CR8）阿克斯AA[y/x]如果y在A（CR9）xA如果x在A中不是自由的表2随机CCP强调让所有可执行进程被速率封装的请求对于语义是至关重要的，参见。第4节更多详情。3.1隐藏的配置和移除系统的变迁由要执行的代理和存储的当前配置决定，因此配置空间应该是P ×C，其中P是进程空间（模表2的同余关系），C是约束系统。然而，去除隐藏的机制需要在上述乘积中引入另一首先，我们将变量V分成两个无限不相交的子集V1和V2，V1<$V2=V1<$V2。然后我们要求所有用于定义主体的变量都取自V1，因此V2中的所有变量在开始计算之前都是新鲜的。直观地说，我们将使用V2中的变量来替换代理中的隐变量.通过这种方式，我们可以避免与自由变量或其他隐藏变量的名称冲突。然而，我们还需要一种方法来记住我们使用了V2的哪些变量最简单的方法是将此信息直接传送到系统的编码器中。因此，如果d不等于hf（V2） =V2的有限子集的集合，则系统的配置将是空间P ×C× V中的一个点，由A，d，V表示。这种将局部变量集添加到系统配置中的想法是从[12]中借用的很定义3.1令A1，d1，V1<$，A2，d2，V2<$ ∈ P × C × V。A1，d1，V1，D当且仅当存在重命名f：V2→V2使得f（V2）=V1，d1[f]=d2andndA2[f]<$A1.很容易看出，r是一个同余关系（r留在这里是为了重命名）。70L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）652隐藏移除的机制将通过函数μ：P×C ×V → P × C × V/μr来实现，将配置映射到没有隐藏操作符的主动代理的配置。μ的定义是通过对施事的结构归纳给出的为了简化符号，在下文中，我们表示μ（μA，d，Vμ）此外，如果<$A，d，V<$μ=<$AJ，d，VJ<$，我们设置<$A，d，V<$μ=AJ且JA，d，V =V。3.2函数μ：P × C × V → P × C × V可归纳定义为：(i)0，d，V(ii)M，d，V（iii）<$[p（y）]λ，d，V<$μ=<$[p（y）]λ（c）.A，d，V<$;（iv）如果x在A的，则V <$xA，d，V<$μ=<$A[x/y]，d，V<${y}<$μ，(v) 如果x在A中不是自由的，则A，d，V<$μ=A，d，V<$μ;(vi) A1.A1，d，Vμ1 .A2，d，A 1，d，Vμ2Σ，d，μ1.ΣΣA2，d，V1，d，V2μ ;μ2上面的定义有点难以解析。然而，它的想法很简单：一个空代理，一个求和（因此所有代理都以ask和tell开始），或者一个递归调用都保持不变，而每当有一个隐藏运算符时，我们从V2中替换一个新变量到隐藏的变量，然后递归地操作剩下的代理。规则（vi）处理隐藏算子过量的情况，并且它可以通过规则（CR9）被移除。这个规则并不隐含在（v）中，因为在这种情况下我们不想在V中添加新的变量。最后，处理并行构造的规则简单地说，μ首先递归地应用于左代理，然后再应用于右代理。这是必要的，因为我们不能在左进程和右进程中使用相同的局部变量名称，所以我们需要在删除右进程中的隐藏时获得左进程的局部变量信息（反之亦然）。由于我们对局部变量的实际名称不感兴趣，所以正确的配置空间是C = P × C ×V/V。μ可以被安全地提升到这个新的空间。命题3.3函数μ：.ΣP ×C×V关于我们.ΣP ×C×V/r，其中[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][10][11][12][11][10][11Q最后，我们注意到，我们不能使用类似的机制来摆脱递归，因为过程调用的自动应用可能会产生无限的并行度。例如，考虑p：- tellλ（c）p;如果我们自动求解递归，我们将得到无限多个tell的副本这种消除隐藏操作符的机制可以被视为瞬时转换，在随机建模的语言中，这意味着具有与其相关联的无限速率的如果我们以这种方式模拟隐藏，我们可以简化系统的配置，1L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6571（SR1）告诉λ（c）.A，d，V<$−→（1，λ（d））<$A，dHc，V<$μ（SR2）λ（c），d，V<$−→（1，λ（d））<$A，d，V<$μ如果d（建议3）[p（y）]λ，d， V如果[p（y）]λ：−A<$M1，d，V<$−→（p，λ） <$AJ，dJ，V<$（SR4）1μ<$M1+M2，d， V<$−→（pJ，λJ）<$AJ，dJ， V<$1μ其中PJ=pλ，λJ=λ+ rate（A2，d）λ+率（A2，d）<$A1，d，V<$−→（p，λ）<$AJ，dJ，V<$（SR5）1μ<$A1<$A2，d，V<$−→（pJ，λJ）<$AJ<$A2，dJ，V<$1μ其中PJ=pλ，λJ=λ+ rate（A2，d）λ+率（A2，d）表3随机CCP局部变量另一方面，无限速率的引入产生了一个“非常规”的连续时间马尔可夫链，经典的分析技术不能安全地使用。这一事实需要不同地处理正常和无限速率，使操作语义的定义复杂化。这就是EMPA所发生的情况[2]。4操作语义该语言的操作语义在结构操作中给出。系统管理由一个灵活的多任务系统组成。dingtoatouchedabedeled关系−→。 形式上，如果配置空间为C =P × C×V /不过，则−→是一个多元集，其元素属于C×[0，1]×R+×C。因此，这个关系被标记为两个实数，一个在0和1之间，另一个是正数。直观地说，第一个数字对应于与特定转换相关的概率，而第二项是转换发生的速率，两者都取决于商店的当前配置。具体地说，这两个数字是我们定义与程序执行相关的底层马尔可夫链的概率模型所需要的，无论是离散的还是连续的（参见。第5节）。72L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65转换定义见表3。首先，我们给出了函数速率的形式定义：P ×C→R，为每个代理分配其全局速率。 这个全局速率只不过是所考虑的代理的所有活动子代理的速率之和。定义4.1函数率：P × C →R定义为：(i) return（0）;(ii) rate（tellλ（c）.A，d）=λ（d）;(iii) rate（askλ（c）.A，d）=λ（d）ifd<$c;(iv) rate（askλ（c）.A，d）= 0 ifd/nc;(v) r在e（[p（→y）]λ，d）=λ（d）;(vi) rate（M1+M2，d）= rate（M1，d）+rate（M2，d）.(vii) rate（A1<$A2，d）= rate（A1，d）+rate（A2，d）;在这个定义中，我们清楚地看到，在系统的每一个状态下，速率函数都是用w.r.t.存储器的当前配置，保证转换系统实际上由实数标记。现在我们对表3的规则给出一些评论。第一个观察结果是，在每次跃迁之后，3.1节中定义的函数μ被应用于所获得的配置。这保证了准备在下一步中执行的代理已经解决了所有活动的隐藏。规则（SR 1）规定tell指令将其参数添加到约束存储器，并且这以概率1和速率λ发生，即tell指令本身中指定的速率。规则（SR2）对于询问指令类似地工作，相对于速率和概率，假设当前存储需要询问约束。规则（SR 3）通过使用简单的替换实现递归调用;第2节的定义保证变量正确连接（与Δ运算符相同，参见。[6]）。规则（SR4）和（SR5）是相似的，它们实现了竞争条件机制，或概率选择。他们指出，如果和或平行合成的单个项可以以一定的概率和速率演化，则整个构造可以以表3的表达式给出的新概率和新速率演化。注意，我们只需要左代理的规则，因为右代理的相应规则可以从+和的交换性导出。直观地说，发生的是当前配置可执行的tell、ask和过程调用指令之间的竞争。我们可以证明执行率是所有可执行代理的执行率之和，执行概率是被执行代理的执行率除以全局执行率。形式上，我们可以将给定配置的可执行代理定义为定义4.2令A，d，V∈C。由exec（xA，d，V）表示的xA，d，V的可执行指令集归纳地定义为：(i)exec（d，V）= 0;(ii) exec（tellλ（c）.A，d，V）={tellλ（c）};L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6573(iii) exec（askλ（c）.A，d，V）={askλ（c）}ifd<$c;(iv) exec（k_askλ（c）.A，d，V_ask）=k_ifd/k_c;（v）exec（<$[p（→y）]λ，d， V<$）={[p（→y）]λ};(vi) exec（M1+M2，d，V）=exec（M1，d，V）exec（M2，d，V）;(vii) exec（A1A2，d，V）=exec（A1，d，V）exec（A2，d，V）;有了这个定义，下面的命题就可以很容易地得到证明：命题4.3设A，d，V∈C为当前构形。然后，下一个转换执行属于集合exec（execA，d，V）的代理之一，调用它ΣA. 如果rate（exec（A，d，V））=A∈exec（A，d，V）rate（A），则transition是rate（A）/rate（exec（A，d，V）），与transition相关的rate是rate（exec（A，d，V））。Q将这个语义与[10，11]中提出的CCP的概率版本的语义进行比较，我们可以观察到两件事。首先，他们的平行和选择算子的定义是参数w.r.t.涉及的进程数。其次，他们将概率分布分配给这些运营商，而我们将费率分配给基本代理，并通过将这些费率组合在一起来获得概率分布。这种不同的方法允许保持总和和并行组合的关联性。此外，在我们的框架中出现的离散时间语义（见下一节）与[10]中的一个在执行规范化的点上不同在[10]中，必须在每个求和和并行结构中执行对活性剂的归一化，以便计算每个转换的概率。相反，在我们的框架中，通过考虑所有活动过程的速率，基本上应用于全局状态的水平。请注意，这种规范化实际上是通过转换步骤的导出树上的结构归纳来计算的，利用了组合性。5时间模型和可观测量表3中定义的操作语义是抽象的。时间的概念。事实上，在标签中，我们通过以两种不同的方式“具体化”过渡关系，携带了足够的信息来构建语言的离散时间和连续时间模型。这对应于速率的两种不同解释，或者是优先级，或者是每单位时间的执行频率。构建描述系统演化的概率模型的第一步，无论是离散时间马尔可夫链（DTMC）还是连续时间马尔可夫链（CTMC），都是将多转移系统折叠成一个简单的转移系统= N ×C×[0，1]×R+×C，最多有一条边连接图的两个不同节点。首先，考虑从一个stateσ∈C的两个跃迁，s ayσ−→（p1，λ1）和ndσ−→（p2，λ2）。Proposition4.3保证λ1=λ2，这是从状态σ的退出速率。若σi，σj∈C是多变迁系统的两个节点，则σi=<$（p，λ）σj为74L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）652Σ通过以下方式构建：通过对所有转换的概率求和来计算pσ−→JΣ因此，p=pJ，而退出率λ保持不变。i（p，λ）jσi−→J（p，λ）作为例子，考虑简单过程A = tell λ（c）+tell λ（c），其中λ是常数函数λ0。多变迁系统的图只有两个节点，σ0=（A，T）和σ1=（0，c）（局部变量的集合可以安全地忘记），以及两条边，都等于σ0−→（1，2 λ0）σ1。因此，由此产生的过渡制度在满足σ0=λ（1，2λ0）σ1的条件下，通过计算得到了一个最优解由于选择中的告知代理之间的竞争条件，从σ0到σ15.1离散时间首先，我们处理语言的离散时间具体化。基本上，我们丢弃所有与速率相关的信息，只保留与转换相关的概率，获得离散时间马尔可夫链（DTMC）。我们要强调的是，一个单一的代理人，一个告诉结构说，没有一个绝对的概率分配。它只有一个表示其被执行的倾向或优先级的比率，而被选择的实际概率取决于它被插入的上下文。背景越广，这种可能性就越小一个DTMC可以用它的随机矩阵来识别，由图的节点（在马尔可夫链上下文中称为状态在我们的框架中，矩阵σ j简单地定义为πij= p，其中σi= σ（p，λ）σj。第4.3章保证jπij= 1，因此随机矩阵k是定义好的。现在很简单为了将离散时间迹线定义为DTMC的迹线，让δ = σ1，p1，σ2，p2，σ3，.，pnσn+1. 这种迹线的长度是长度（δ）=n，而长度（δ）其概率为Prob（δ）=i=1pi.我们现在可以定义I/O观测量，对应于输入输出的可观测性（参见[10]）。首先，我们必须定义从状态σI到状态σO的概率，等于Prob（σI−→σO）：Σ概率（σI−→ σO）={p|p = Prob（δτ），δτ= σIp1σ2.σnpnσO}。其次，我们去掉了关于局部变量集的信息，因为我们只想观察约束存储的结果：Prob.A，d. AJ，dj= Σ∞|=零|=0Prob（A，d，μ−→. AJ，dJ， VΣμ）。注意，我们不区分相同基数的V集，因为它们都是等价的模重命名。定义5.1离散时间I/O可观测量是约束存储C上概率的（子）分布，由下式给出：Od（A，d）=.（dJ，p）|p=Prob。A，d0J，dj.σjL. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6575λ1+λ4λ1+λ4Fig. 1. 程序的执行树˙ ¸告诉λ1（c）询问λ2（c）。tellλ3（d）+tellλ4（e），T前面的分布一般是一个子概率，因为可以有无限次的非终止计算，我们不从它们中收集概率然而，存在可以避免这些问题的一般概率构造，参见。[25]但我们并没有遵循这个方向。事实上，我们对概率质量的损失解释为程序永远不会终止的概率感到例5.2现在我们举一个简单的例子，以阐明可观测量的作用。 我们考虑一个非常简单的程序，agent，即A = tell λ1（c）<$ask λ2（c）。tellλ3（d）+ tellλ4（e）。我们在这里想到的约束系统非常简单：c，d，e是基本的标记，所有的不同标记都是通过H的组合是不同的。由于在A中没有任何隐藏运算符，我们可以安全地忘记配置中的局部变量集。当计算从空的约束存储T开始时，执行树如图1所示。请注意，在树的边缘上，我们有两个数字作为标签：第一个是与该转移相关的概率，第二个是转移本身的速率。一开始，我们可以观察到两个tell进程（未启用ask）之间的竞争条件，一个速率为λ1，另一个速率为λ4。 所以把c加入商店的概率是λ1 ，而e将被添加概率为λ4。在任何一种情况下，跃迁的速率都是λ1+ λ4。其他过渡工作类似。从图1中的树可以清楚地看到，只有两个终端状态，也就是说，0，cHd和0，cHe。为了计算离散时间的可观测量，我们必须收集导致它们的所有迹的概率，给出：.Σλ1λ2λ−λ1λ2Od（A，T）=（cHd，），（cHe，），λ λ其中λ=（λ1+λ4）（λ2+λ4）。请注意，这是一个概率，因为所有的计算终止。76L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65JJc）（t）=（d，p）<$（t）.μ5.2连续时间在本节中，我们定义了操作语义的连续时间具体化。其思想是根据其无穷小生成元Q-矩阵来定义一个基础的连续时间马尔可夫链（CTMC）[18]，该矩阵简单地从转移系统中存在的信息中计算出来。考虑两个状态σi，σj∈C，其中σi=<$（p，λ）σj;矩阵的元素qij计算为qij=pλ：从σi到σj的转移率是λ的p分数，即从σi的全局退出率。请注意，转移中携带的信息对应于与CTMC相关的跳链和保持时间随机变量[18]，这是CTMC蒙特卡洛模拟算法的基础根据Q矩阵，我们可以通过求解以下微分方程组（如果状态空间是无限的，则可以是无限的）来重建在时间t内从状态i到状态j的概率分布，该微分方程组也称为CTMC的随机主方程[18]：(1)PJ（t）= QP（t），P（0）= Id。给定概率矩阵P（t），我们可以给出连续时间的概念。作为经过时间t的函数的可观测量。事实上，在时间t从σI到σO的概率是Prob（σI−→σO）（t）=P（t）σI，σO。从局部变量的信息中抽象出来，我们得到从a状态在时间t内，将状态A，d，j转换为状态A，J，d，J，j，Prob.A，d.A、dΣΣ（t）=Σ∞|=1个|=1Prob.A，d，. AJ，dJ，V（t）。定义5.3时间t处的连续时间I/O可观测量是约束存储上的子概率分布，定义为O（λA，dλ A ）J|p=Prob。 A，d−→。0，dj直观地说，这给出了一个进程在t个时间单位或更短的时间内以最终存储dJ终止的概率。这是一个子概率，因为通常不是所有的计算都在时间t之后停止。我们指出，这里定义的可观测的概念是经过时间的函数。实际上，它对应于矩阵P（t）的行P（t）的子向量<$A，d，<$A2P（t）的连续性意味着Oc（t）是连续的。一个有趣的问题是Oc（t）的长期行为，即在极限t→ ∞中发生了什么。从本质上讲，我们要问的是最终到达终端状态的概率是多少。但是这些状态是CTMC的吸收类[18]详细内容。这一事实使我们能够证明以下几点[2]更确切地说，它对应于该向量的线性函数，这是由于局部变量集合上的聚合。ΣμL. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6577⎜⎟⎟⎟⎟定理5.4lim Oc（A，d）（t）= Od（A，d）.Qt→∞因此，连续情况下的t依赖可观测分布收敛于离散时间模型定义的可观测分布这个定理将离散和连续时间具体化的长期行为联系在一起。基本上，它指出，在渐近极限中，连续时间模型引入的额外信息蒸发，导致离散时间模型引起的相同概率分布。这个定理是自然的陈述和证明在我们的框架内，这使得明确的关系之间的离散和连续的解释的语言。例5 - 5我们重新考虑例5 - 2。为了计算连续时间情况下的可观测量，我们必须计算基础链的Q矩阵。 首先，我们必须确定程序状态的顺序。 如果我们设置A3=λ1（c），e∈，A1=λ1（c）λ2（c）. tell λ3（d）+ tell λ4（e），T ≠，A4= tellλ3（d），c≠， A2= taskλ2（c）. tellλ3（d）+tellλ4（e），c，A5=0，cHd，A6=0，cHe，其中由索引引起的排序，我们有：⎛ ⎞⎜−λ1− λ4λ1λ400 0⎟⎜⎜⎜⎜⎜Q=0⎜⎜⎜⎜⎜⎝⎟0−λ2−λ40λ20λ4⎟⎟0 0−λ10 0λ1⎟⎟000 −λ3λ3 0⎟⎟0 0 0 0 00⎟⎠0 0 0 0 0 0给定矩阵Q，我们可以很容易地计算出在一定时间t内从一个状态到另一个状态的概率，从而计算出可观测量。 事实上，对于有限矩阵，方程（1）的解是，根据矩阵指数，P（t）=etQ。例如，如果λ1=λ2=λ3=λ4= 1，我们有Oc（A，T）（1）={（c H d，0. 0513），（c H e，0.{\fnSimHei\bord1\shad1\pos（200，288）}（2）={（c H d，0. 1467），（c H e，0. 6009）}，（100）={（c H d，0. 2500），（c H e，0. 7500）}。正如我们所看到的，观测值快速收敛到由下式给出的平稳分布：Od（λA，T λ）={（c H d，0. 2500），（c He，0. 7500）}。6sCCP中的生物系统建模随机过程代数已被证明是在不同抽象层次上对生物系统建模的有力工具[20]。这一申请源于78L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65观察生物实体之间的相互作用和过程之间的惊人的相似之处。第一个生物系统模拟了生物化学反应的网络在这个领域中最常用的过程代数是随机π-演算[19]，即使其他人也被使用过，比如PEPA [17]。CCP提供了一种与π演算不同的通信形式，通过存储器异步进行，存储器可以被看作是一种具有计算能力的存储器。这个特性反映在建模过程中，因为必须在商店级别描述交互的一部分。请注意，我们可以将约束存储视为环境的描述，由生物行为者填充，即通过询问和告诉指令与之交互的过程3在生化反应的情况下，我们可以将存储器的变量与每个分子和每个化合物相关联，存储系统中存在的这些分子的数量[4]与π演算不同的是，这里的主体与反应相关联，它们通过修改约束存储中变量的值来进行交互。在充分搅拌的混合物中，这些反应的动力学速度与基本速率乘以可用的相互作用分子的数量成比例。对于双分子反应，这意味着所涉及的两个分子的数量的乘积。这一观察结果是用于生化反应数值模拟的Gillespie算法[13]的基础，我们可以通过使用适当的速率函数来恢复它为了测试这种描述的可行性，我们在Prolog语言中实现了一个元解释器，能够运行sCCP程序的模拟在图2中，我们给出了sCCP代码和钠和氯离子化的简单可逆反应的时间演化：Na + ClNa+ + Cl−。正如我们所看到的，我们有两个过程，并行进行Na和Cl的电离和相应离子的去电离。观察速率函数的结构：速率被计算为基本速率乘以存储参与反应的两个分子的量的变量的乘积。的优点这描述w.r.t. 随机π演算主要是在悬挂物的变量中表示定量信息（分子数/浓度）的可能性和在动力学动力学模型中由非恒定速率给出的不稳定性。[4]关于这一点的进一步评论。7相关工作这个版本的CCP属于过程代数类，如PEPA [17]，随机π-演算[19]或EMPA [2]，仅举几例。然而，CCP和这些语言之间有一个重要的区别，即事实上，3注意，同步通信可以很容易地集成到CCP中，例如[3]。这一增加将进一步扩展建模能力。[4]CCP中的计算是单调进行的，因为我们只能添加新的信息，但不能删除它，因此要让变量改变值，我们必须将它们表示为不断增长的项列表。这些变量将被称为流变量。L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）6579我ioniz（Na，Cl，Na+， Cl−）：-（tellλNaCl（ion（Na，Cl，Na+， Cl−））+告诉+−（dei on（N a，Cl，N a+，C l −））λD Na Cl）.ioniz（Na，Cl，Na+， Cl−）FIG。 二、Na+Cl的CC P过程：N a++Cl−reaction（left）和s imulationout e（right）。CCP中的操作是异步的，而其他语言实现了代理之间的同步交互。事实上，从性能分析的角度来看，异步通信更容易处理，因为同步速率的定义很麻烦（参见。[5]）。在这种情况下，与异步随机语言（如pKLAIM [8]，特别是随机KLAIM [7]）有更强的相似性，其中速率被分配给通信指令。CCP在概率环境中以两种不同的方式扩展。在[14]中，通过在约束存储中添加随机变量来引入概率成分与我们的方法更相似的是[10]中提出的概率版本，其中概率分布既与求和算子相关联，又与并行合成相关联。这就产生了一种具有离散时间模型的概率语言，参见。第4节进一步评论。据我们所知，这是连续时间随机CCP的第一个建议。8结论和今后的工作我们提出了一个随机版本的CCP，其中每个与存储通信的指令都有一个实数，代表指令的优先级或其“速度”速率。操作语义以抽象形式给出，可以用特定的时间模型具体化，离散或连续。此外，对应于输入/输出行为的可观测量的概念被定义为离散时间和连续时间的版本，并且保留了求和和并行合成的通常代数性质。定理5.4给出了离散时间和连续时间之间的桥梁，说明了它们在长期行为中的等价性。在第6节中，我们认为sCCP可以用作建模生物系统的语言。 对这一目的的更详细分析将作为今后的工作推迟进行。此外，出于建模目的，sCCP的ad hoc概率模型检查过程[21]的开发可能很重要。致谢非常感谢Alessandra Di Pierro和Herbert Wiklicky的有益建议和讨论，并感谢Agostino Dovier的无与伦比的支持。80L. Bortolussi/Electronic Notes in Theoretical Computer Science 164（2006）65引用[1] K. Apt. 约束编程原理。剑桥大学出版社，2003年。[2] M. Bernardo和R. Gorrieri。Empa教程：具有非确定性、优先级、概率和时间的并发进程理论。技术报告96[3] F.S. de Boer，R.M. van Eijk，W. van der Hoek，and J-J.Ch. Meyer. 交换的失败语义多智能体系统中的信息。2000年CONCUR会议记录，1998年。[4] L. Bortolussi和A.警察系统生物学的过程代数与微分方程的连接。2006年提交CMSB。[5] J. Bradley和N. 戴维斯具有近似同步的可靠性能建模。在J. Hillston和M. Silva，编辑，Proceedings of the 7th workshop on process algebras and performancemodeling，第99-118页。萨拉戈萨大学，1999年9月。[6] F.S. de Boer，A. Di Pierro和C. Palamidessi。约束规划中的不确定性和无限计算。理论计算机科学，151（1），1995年。[7] R. De Nicola，D. Latella和M.马辛克基于klaim的移动系统形式化建模与定量分析。在SAC05会议记录中，2005年。[8] A.迪皮耶罗角Hankin和H.维基基连续时间概率klaim。 在2004年赛科会议记录中，2004年。[9] A. Di Pierro和H.维基基基于Banach空间的概率并发约束程序设计语义。在CATS'98的会议记录[10] A. Di Pierro 和 H. 维 基 基 概 率 并 发 约 束 程 序 设 计 的 操 作 语 义 。 IEEE Computer Society InternationalConference on