嵌套结构的软件性能建模：分层自动机模型与流体近似 在线获取

可在www.sciencedirect.com在线获取理论计算机科学电子笔记310（2015）27-47www.elsevier.com/locate/entcs嵌套自动机模型的流体性能分析卢卡·博尔托卢西的里雅斯特大学数学与地球科学系，比萨，luca@dmi.units.it简·希尔斯顿爱丁堡大学信息学院，jane. ed.ac.uk米尔科·特里巴斯通电子和计算机科学，南安普敦大学，m. soton.ac.uk摘要在本文中，我们提出了一类嵌套自动机的建模的性能，可用性和可靠性的软件系统的层次结构，我们称之为系统的系统。定量建模提供了宝贵的洞察软件系统的动态行为，允许非功能属性，如性能，可靠性和可用性进行评估。然而，许多系统的复杂性对这种方法的可行性提出了挑战，因为所需的数学模型变得太大而无法获得高阶计算效率的解决方案。近年来，人们发现，在某些情况下，一个近似的平均场，可以提供非常好的估计，同时大大降低了计算成本。我们提出的系统的系统是分层排列的自动机，其中，在兄弟姐妹之间，父母和孩子之间，甚至从孩子到父母之间，都可以发挥作用，从而可以捕捉到广泛的复杂动态。 我们表明，在温和的条件下，系统的系统可以配备有比显式状态表示更有效运行几个数量级的EQUIPUID近似模型，同时提供对可执行性措施的出色估计。这是一个显着的扩展，以前的流体近似结果，软件性能建模的有价值的应用。保留字：系统的系统，流体近似，软件性能建模。1介绍嵌套（或分层）结构的建模和分析经常发生在许多领域，包括例如软件系统和生物过程。例如，在软件上下文中，云环境可以被认为是许多计算机的集合，每个计算机都包含其他组件，例如处理器和线程[10]。因此，有三个层次：进程和线程，计算机和云本身，以及在每个层次上的个人行为http://dx.doi.org/10.1016/j.entcs.2014.12.0111571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-SA许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-sa/3.0/）。28L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27实体可以用自动机来描述。请注意，这些系统中的层次嵌套是真正的结构化的，而不是像UML状态机那样用来隐藏细节的抽象。这些系统的组织复杂性意味着很难预测它们的行为，因此在部署之前必须调查性能和可靠性特征当正式推理这些系统进行反应模型的基础上离散状态空间表示，问题的规模增长非常迅速的人口的组件，使分析在实践中不可行在本文中，我们提出了一个马尔可夫模型的嵌套自动机，我们称之为系统的系统。自动机按层次结构组织在一棵树中（图1 a））;自动机的行为可以由其兄弟的状态来判断（水平交互;图1 c））。每个自动机都包含其他自动机，父自动机的动态可能会影响其子自动机的动态，反之亦然（垂直交互;图1 d））。树的每个节点都被分配了一个多重性，这表明在其父自动机的每个副本中，系统的系统中存在多少个随机自动机的副本（图1b）。嵌套马尔可夫模型先前已被提出作为一个很好的模型，以结构化组织的软件系统，但有限的进展已经取得了沉重的计算成本，由于分层和大的多重性。以前提出的技术试图利用对称性，但仍然产生马尔可夫链。例如，Buchholz利用Kronecker代数的分层模型，可以表达某些类别的随机Petri网和随机网络，但他的工作仅限于两级嵌套[4，5]。Lanus和Trivedi考虑了一类分层马尔可夫模型，其中任意大小的自动机的状态可以以这样一种方式进行划分，即可以构建一个简化模型，该模型保留了可用性和性能的稳态奖励措施[11]。然而，CTMC的状态空间大小仍然是相关的（在最坏情况下呈指数关系） 减少自动机的数量在本文中，我们介绍了一个平均场近似的基础上的一个系统的普通微分方程（ODE），最初关联的方程与每个元素的CTMC状态描述符，估计的期望。不幸的是，状态描述符的增长与级别的数量呈指数增长，多项式与类树中的分支级别，每个类中的自动机的数量，每个自动机类的状态数。这显然阻碍了甚至适用性的嵌套系统的适度规模的EQUUID模型。为了解决这个问题，我们利用这种方程之间的对称性，非正式地表明，对于任何两个相同类型的自动机副本（即，属于树中的相同节点）产生相同的ODE解。因此，通过考虑树中每个节点的代表性方程组，可以显著减少ODE系统的大小，而与所有涉及的多重性无关。ODE对称性的基本结果类似于[15]，它在马尔可夫过程代数PEPA [9]的背景下建立了ODE集总性的一种在这方面，本文件由于其一般性，代表了一个重大的改进L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2729和更广泛的适用范围。具体来说，在[15]中，水平交互仅限于PEPA的语义。例如，这排除了研究具有更一般形式的相互作用的嵌套系统的可能性，例如某些网络模型中使用的质量作用定律[16]。相反，我们的结果不依赖于实际的相互作用的法律，提供他们产生一个ODE系统的唯一的解决方案。对于垂直交互，本文放宽了进程代数中选择特定同步算子所施加的限制。例如，在PEPA中（以及通常基于CSP的演算中），垂直交互可以通过考虑父进程P和其子进程C1，... .，Cn，在复合过程中：P<${α}（C1<$L... Cn）。在这种情况下，如果α∈L，那么语义强制只有当所有进程都可以执行时才能看到α动作。 另一方面，如果α/∈ L，则只有一个进程Ci将与其父进程同步执行动作。在CCS和其他基于互补动作的进程演算中，即使引入了二进制交互的事务，情况也更加严格。在我们的建模形式主义，垂直相互作用是通过引入因果映射的概念。使用因果映射，建模者可以指定，例如，哪些状态的子自动机容易受到父母执行的动作，以及当该动作被目睹时，子自动机改变其易受影响状态的概率可以表明，这种表达水平不能通过使用PEPA或其他可用的马尔可夫过程代数（例如，[1，8]）。论文概述第2节介绍了我们的系统的马尔可夫模型，并通过一个简单的运行示例来说明主要定义。第三节讨论了椭圆流体近似，并给出了常微分方程对称约化的结果。第4节使用了一个分层分布式计算系统的可执行性模型的案例研究，广泛的数值验证的目的，考虑的准确性的EQUUID近似及其计算优势，随机分析。最后，第五部分对本文进行了总结。2嵌套自动机系统的系统是由马尔可夫自动机组成的层次模型，其中包含其他自动机，具有任意嵌套级别。在这里，我们感兴趣的系统中，在任何层次的组织由一个人口的相互作用的代理。这类系统的例子无处不在：在生物学中，组织由许多细胞组成，每个细胞包含许多不同的生化分子相互作用。服务器群包含许多计算机，每个计算机都可能运行大量的进程。在后一种情况下，更高级别的马尔可夫自动机可以表示服务器群，它们将包含对群内计算机进行建模的马尔可夫自动机，每个群都包含表示运行过程的自动机种群。通过图1中的一个示例说明了这种分层包容的概念，30L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27n 1>=2n 2>=1n 1，1>=2一TT<第1章><二><1、1>a)b）、不不Fα=λa1c）、1 d）、Fig. 1. a）系统的系统; b）系统的系统的实例; c）水平相互作用; d）垂直相互作用。在本节剩余部分中将介绍的符号现在我们来描述系统模型的系统结构。我们的想法是，我们将在层次结构的每一级描述一个原型代理填充该级别的每种类型的代理。这在代理类的概念中得到了体现。然后，这些类将被实例化，指定系统中每个类2.1结构设A是模型的所有自动机类的集合我们可以将每个类看作系统中的一种元素或代理。因此，例如，在服务器群中，群，计算机和作业都可能是系统描述中的不同自动机类一个系统的系统由一棵树来具体化，树的节点A描述了这些类的分层组织因此，在服务器群示例中，一台计算机将是一个群的子计算机，并且是多个作业的父计算机为了讨论树中不同的代理类，我们需要一些坐标符号。为此，我们假设一个固定且定义良好的访问策略（例如，深度优先），并用D表示树的深度。我们让i1，i2，. il<$∈ A表示到达树的第l层的自动机类通过从根下面的第i个自动机类开始导航树，然后取它的第i个孩子，等等。注意，我们不需要平衡树，因此，例如，101，1，102可能属于树，但102，1，103可能不属于树。 在记法中，我们有时将i1，i2，.，il到il，其中il是长度为l的索引向量，或者类似地，到il−1，il。我们用cil来表示i l的孩子的数量。这些将被索引为101，102，103，203，.，你好，我很好。在建立了自动机类的层次组织之后，我们现在转向描述自动机类本身。从本质上讲，每个自动机将是一个有限状态机，它将以概率方式（随机时间）改变状态L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2731LL由于与系统级规则指定的其他自动机的交互。我们首先提供自动机结构的描述：自动机类il由元组定义哪里你好我好。Σ⟨il⟩,−→⟨il⟩,n⟨il⟩Σ,• 是自动机dil，其中dil =|拉吉勒|.• −→ilil×il是两个状态之间的跃迁集合。 当文字清晰时，我们使用缩写−→ilby−→。首先，我们使用典型的符号il 如果. il•n<$il <$∈N是种群大小，即它指定有多少个不同的副本，自动机i1，i2，...，在其父自动机的每个副本内存在多个副本，i1，i2，. il−1。如果l= 1，它只是表示在系统的系统中有多少个拷贝后一点需要更多的解释。假设我们有一个简单的系统，只有一条从101到101，1的路径。在这里，有n个<$1<$1 <$类型的自动机，但每个都包含n个<$1，1 <$1类型的自动机。因此有在这个系统的系统中总共有n<$1<$+ n<$1 <$·n<$1，1 <$自动机。例如，一个服务器群的系统表示，由10台服务器组成的单个群，每台服务器托管20个作业，将有211个自动机。为了描述系统的系统的状态，我们将使用以下形式的布尔向量：b：=。bj<$il<$[kl]<$，<$il<$：<$il<$∈A，1≤j≤d<$il<$，（1）其中k1=（k1，...，kl）使得1≤km≤n∈i1，.，im，对于所有1≤m≤l。每个元素ntbjil[kl]等于1或0。 S p eci call y，bjil[kl]=1当且仅当j是通过获取i 1的第k1个副本、i 1的第k 2个副本、i 2的第k 2个副本等而到达的i l类型自动机的当前局部状态。因此，对于自动机的每个副本和il类型自动机的每个局部状态，我们记录这个实例是否处于该状态。需要向量b的双索引il和[kl]，因为我们需要识别特定自动机类的特定自动机。因此，kll标识系统树系统中的自动机类，而kl指定总体的实际元素为了做到这一点，我们还需要知道哪些是包含给定代理的实际自动机，因此需要另一个坐标向量。示例1我们使用下面的运行示例来说明本节中给出的定义。 让我们考虑图1中所示的系统的系统，具有三个自动机类，101、102、103和102，每个自动机类具有两个局部状态和转换12101，101→ 101，102，101，102→101，101。32L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27Σ让我们设n= 2，n= 1，且n = 2;也就是说，在自动机的两个副本中的每一个副本中都有自动机的两个副本。因此，状态描述符具有以下形式：b=.b11[1]，b21[1]，b11，1[1，1]，b21，1[1，1]，b11，1[1，2]，b21，1[1，2]，b11 [2]，b21 [2]，b11，1 [2，1]，b21，1 [2， 1]，b11，1 [2， 2]，b21，1 [2， 2]，b12[1]，b22 [1]，（二）其中，第一行的元素表示自动机的局部状态，这些状态可以从第一个副本中获得;第二行的最后两个元素描述了自动机的局部状态，这些状态可以从第二个副本中获得;最后两个元素表示唯一的自动机的状态，它没有孩子。2.2语义一个系统的动力学受其组成部分之间的两种相互作用的影响：水平相互作用和垂直相互作用。横向互动是通过同一层级实体的动态相互影响而产生的。例如，在服务器群模型中，这可以是单个计算机内的进程和作业然而，这些动态并不独立于上下文，而是可以由包含节点的状态和包含在交互节点中的自动机的状态来确定这被称为垂直互动。再次，在服务器群示例中，计算机中的进程的速度可以取决于其能量状态，例如，其是否处于功率节省模式。此外，服务器群中的两台计算机可以交换作业，如果其中一台有许多作业等待处理，而另一台空闲。另一种形式的垂直交互是由于树可以将其影响传播到它的后代节点：想想计算机断电会对其中运行的进程产生的我们将通过事件来描述第一种相互作用，这些事件由系统级别的规则来指定，而第二种动态将通过因果图来描述。系统的系统的动力学的主要来源是事件E，其引起状态描述符（1）的变化。每个事件η∈ E将水平交互定义为系统树系统中兄弟自动机之间的同步形式。它的特征是一个同步集Sη，指定哪一类自动机和多少实例参与事件，并通过函数Fη给出相互作用的速率。与[12]类似，这是一个功能速率，以便完整地描述整体行为。我们选择这样的比率只取决于人口水平。这种选择是基于这样的假设，即同一自动机的副本在统计上彼此相等，但每个个体的状态可以被观察到。然而，一个自动机的行为可能依赖于它的父级、兄弟级和子级的当前状态。在这里，这种关系表现为这样一个事实，即功能率可能取决于儿童和兄弟姐妹的总人口从形式上讲，L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2733LS2LLΣLF η。一个100万， . ，aisη，ail−1，Xsil−1，Xci1，. ，Xcisη，Ls = 1，...，sη;LLLLLLLLLL用下面的形式定义事件E定义2.1[事件]事件η∈ E是一对η=（Sη，Fη），其中：◦Sη是包含自动机转换的同步集，记为y i sj−→issn，使得对于每个s1，s2 = 1，.，Sη（Thell−1l −1事件中涉及的自动机具有相同的父级），其中sη是事件中的自动机 为简单起见，我们还要求，即L同步中涉及的自动机都是不同的。1◦函数Fη给出了一个特定的自动机元组在状态i1isη 该函数具有参数：llll哪里• ais：=. 一个1000美元的硬币， . ，adi sis• ail-1是i 1，.的父节点的状态空间的描述符，isη• Xsil−1是i 1，.的兄弟种群的状态描述符， 如果你不介意，LlXsil−1：=（Xil−1，1，.，Xil−1，cil−1），哪里Xml：=.X1ml，. ， Xdml，对于所有ml：∈A并且Xjml是在状态j中的ml的实例的数目的计数;• Xcis：=（Xis，1，.，Xis，cis）是种群的子节点，对于s= 1，...， sη。实施例1（续）再次考虑图1中所示和前面所述的实施例。 令α表示一个顶层的动作，涉及状态为<$1 <$1和<$2 <$2的自动机。我们会写Sα={<$1<$1 → <$1<$2，<$2 <$1→ <$2 <$2}。关联函数Fα具有形式参数F α。a11，a21，a12，a22，X11，X21，X12，X22，X1<$1，1 <$，X2<$1，1 <$}，1这个条件可以很容易地放弃，代价是强制每个类的自动机数量最少。 并使Sη成为多重集。L34L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2712其中，第一行与两个类型为1的自动机的局部状态有关，第二行描述了对兄弟姐妹的局部状态的依赖性，最后一行显示了对孩子的局部状态的依赖性。设置Fα=λαa1，当λα> 0时，表示每当两个自动机处于其局部状态1时发生同步;当这种情况发生时，自动机在2中改变其局部状态，如在同步集合Sα中所表达的。同步速率由λα给出。在上面的例子中，为了简单起见，我们考虑了一个函数Fα，它不依赖于父自动机或子自动机的种群。第4节将研究一个更详细的案例研究，其中存在这种依赖关系。此外，让我们注意到，我们故意使用由字母a表示的形式参数（例如， 11和1 2），以指示这是一个模板函数，可以应用于区分（2）中的布尔状态描述符向量b。虽然这将在后面的定义2.3中得到更精确的定义，但在这里我们预计这个函数将引起b的两个不同的转变。更具体地说，这两个转换都涉及自动机的同一个副本，但是，第一个转换将涉及它与自动机的第一个副本的交互，而第二个转换将描述与自动机的第二个副本的交互。一个事件指定了哪些自动机被同步所影响，以及这发生的速度有多快。然而，它并没有说明它们的子节点实际上发生了什么。让我们回想一下，描述这种行为对于建模系统中的事件影响其内部组件的行为的情况是有用的计算机的断电将中止其所有软件进程。相反，这种垂直交互形式被因果映射的概念所捕获，它定义了父自动机的转换如何影响其子自动机。定义2.2[因果图]因果图C是一组规则，其形式如下：il. ;il，rmjm−→il，rmkm：：pm其中pi是（0， 1]中的一个数，或者是特殊符号！在因果映射的规则右侧，每个自动机事件的值pj指定更新发生的概率（当p∈（0， 1]）或恰好一个子自动机改变状态的概率（如果p=！）。一个因果映射是良构的，如果左边的每个转换在C中最多出现一次，并且右边的同一状态中永远不会有两个事件规则的手侧，即 il，rs 对于s1/= s2。 在下文中，我们假设所有的因果映射都是rewell-formed的，并且we将表示为yrule（i li−→ilj），即C中规则的右手边，如果y为n，则将y rul e（il i−→ilj）表示为左手边。示例1（续）对于前面考虑的示例，我们可以定义L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27351sηL.- 是的ΣLL1LM因果映射⟨1⟩ →⟨1⟩100万美元，1万美元→100，1升- -！（三）这个因果映射表示，每当一个自动机的局部状态从1变为2时，那么正好有一个子自动机从状态1变为状态2。正如所讨论的，事件的具体化是在自动机类的层次上给出的然而，回想一下，系统的系统由每个自动机类的许多实例组成。因此，我们可以想到一个人口对应于每一类自动机。在实践中，每个事件都将涉及给定自动机类的一些元素。因此，我们需要一种机制来确定所涉及的实际因素或代理人此外，我们需要考虑自动机的所有可能选择，每个选择都提供了事件的实例更具体地说，考虑一个事件η ∈ E，涉及到类i 1，.， ⟨i sη ⟩.我们通过实例函数Fη [k1，...， ksη]（b）. 当事件η同步时Ll在l级自动机中，我们需要识别它运行的父自动机这用iη- 是的坐标k，…， k指定实际au-l−1Llj j j jJTomata参与了此次活动。 每个k =（k，...，k）使得1≤km≤n≠i，其中1 ≤m≤l且j = 1. sη。 此外，由于所涉及的自动机需要包含在同一个父节点中，则它保持ki=kj. 一个元组（k1，...，ksη），l−1l−1ll满足这些约束的事件称为事件η的实例，表示一个事件可以通过选择特定实例来参与事件并经历更新而在系统的系统内显现的方式。对于系统的系统的任何给定事件和给定状态，可以存在可以实例化事件的η的实例集表示为：Kη。每个函数都与一个跳转或更新向量相关联，根据同步集合Sn，状态描述符，即b中的每个条目将递增或递减1，以反映进入和退出每个自动机的每个实例内的局部状态示例1（续）回想一下，α是图1所示示例的顶层操作，涉及状态为<$1 <$1和<$2 <$2的自动机。的元组1、 1和2、 1形成事件α的实例集合。它们表示自动机的两个副本中的任何一个副本与自动机的唯一副本2002年。在我们定义与系统系统相关的CTMC动力学之前，引入一些额外的符号将是有用的。在系统的系统中捕捉到的丰富的动态特性意味着，转换的速率，甚至转换的存在，不仅取决于发生转换的自动机的状态，而且还可能取决于同一级别的其他自动机（兄弟）的状态，它的封闭自动机（父）和其中的自动机（子）。但我们确实限制了这种依赖性只取决于兄弟姐妹，122136L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27LJii. Σl−1Σb1 [2]=.b11[2]，b21[2]，.Σ吉勒LLLLLLη儿童通过他们的人口计数，基于假设的情况是不可区分的。我们用bj[kj]状态e的向量n尝试等式（1）中的形式吉勒勒勒对应于实例kj：b[kj]：=.b1ij[kj]， . ，bdi jij[kj]，j=1. S.（四）如上所述，CTMC中的转换将取决于事件中所涉及的实例的这种详细的当前状态，但也可以由兄弟和子自动机通过它们的聚集状态（就它们的种群而言）来确定我们引入符号来表示这些粒子，其中Sil−1<$[kl−1]是对应于所有兄弟的计数向量。本质上，对于父自动机类的实例k l −1中包含的每个自动机类，我们计算每个本地状态有多少个自动机实例SJil−1[kl-1]，特别是，自动机类的状态计数的向量l-1，j-1。Sil−1[kl−1]：=。S1[kl−1]， . ，Sc<$il−1<$[kl−1]<$，（5）SJil−1 [kl−1]：=nil−1，jr=1B1il−1，jnil−1，j[kl−1，r]， . 、r=1bd<$il−1，j<$[k，r]il−1，j（6）类似地，我们考虑子自动机中的种群Cj，[kj]，其中包含自动机kj中包含的自动机的状态：吉勒勒勒LCj[kj]：=Sj[kj]（7）il例1（续）对于事件α，我们有：b1[1]=.b11[1]，b21[1]，b<$2 <$[1] = b1<$2 <$[1]，b2<$2 <$[1]。兄弟姐妹群体的向量由下式给出：.b1<$1<$[1]+b1 <$1 <$[2]，b2<$1<$[1]+b2<$1<$[2]，b1<$2<$[1]，b2<$2<$[1]<$。同样，儿童人口的矢量是.b1<$1，1 <$[1，1]+b1<$1，1 <$[1，2]，b2<$1，1 <$[1，1]+b2<$1，1 <$[1，L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27372]<$。我们现在准备提供CTMC实际动态的定义。我们需要做的是为每个事件η的每个实例指定速率（由实例函数给出，其中我们替换兄弟姐妹38L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27sηJ.伊什LLLLLrsηr1蓬塔尼山bL吉勒L阿吉勒 ⟩Lil−1il−1吉勒L阿吉勒 ⟩LLLηL1LMMLLLLLLLLL+1个LLLLLLRlt=1D阿吉河阿吉尔山[kr，t]L如果r，s，d→−我的天啊！∈R，+1个LLL.LLηLL和子节点）和更新向量，指定CTMC状态描述符中的净变化。此外，每个事件在自动机层次结构中向下游传播其效应，根据与过渡中涉及的自动机中的状态变化相关联的因果规则。因此，我们还需要指定子自动机以多大的速率感知发生在其父级的事件，以及它们的状态如何修改。定义2.3[CTMC动力学]设A是具有事件E的系统的系统。 让（1）定义CTMC状态描述符。然后，从事件η∈ E导出CTMC的转移函数如下：Fη [k1，.，ksη]（b）：=LlF ηb1[k1]， . ，bsη [k]，b[kl−1]，1S[kl−1]，C1[k]， . 得双曲余切值.sη[ksη]，（8）对于所有（k1，...，ksη）∈K，其中kj=（kj，.，kj），使得1≤hj≤ni，与1≤m≤l且j= 1... sη。由y∈n[k1， .. . ，kη]：=ejij[hl]，ij使得<$iJl<$∈ A，其中1≤j≤d<$iJl<$， 1≤h≤n<$iJl <$，定义如下：如果<$ir<$r1→−<$ir<$r2∈Sη，iJ=ir，hl=kr， j=r2，ejiJl[hl]=<$ir<$r2∈Sη，iJ=ir，hl=kr，j=r1−1ifirr1→−000年，或l l l然后，对于eachirr1， →−irr2 ∈Sη，则C，say中有它的规则LR=rule（irr1→−L在图2中，我们为每个副本定义一个转换函数，自动机子m的类型为ir，rJ，包含在可由kl到达的自动机≤m≤nir，rJ，如下所示：Fi，s[k，m|k，...，K]（b）：⎧⎪F η[k1,. . . ，ksη]（b）·bdr[kr，m]Lη1sηdrrdrf[kl， . ，kl]·p·bir，s[kl，m]ifil，s⎩⎪−→il，s：：p∈R，和相应的跳跃向量eηir，s[kl， m|k1， . ，ksη]：=.ejij[hl]，FL⎪⎨（九）0否则，L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2739L−1if<$ir，s<$d−→<$ir，s<$f∈R，j=f，iJ=<$ir，s<$，hl=<$kr，m<$⎧⎪⎨+1if⟨ir,s⟩d−→⟨ir,s⟩f∈R,j=d,iJ=⟨ir,s⟩,hl=⟨kr,m⟩LLLLL与组分000年，或l l l等式（8）表示转换函数的实例，以描述参与事件的自动机的特定元组的行为。这取决 关于所涉及的自动机的局部状态，参见。（4），并在其父母的状态，这是通过删除位置向量kl的最后一个元素达到的;速率也可能取决于自动机的兄弟姐妹，参见。（五）、注意，根据定义，兄弟是那些可以在自动机的父系统中找到的，即， 在自动机所在的特定副本中。如前所述，对兄弟状态的依赖是通过给定局部状态下自动机的总种群，参见（六）、最后，速率可以以类似的方式依赖于自动机的子。等式（9）考虑了对孩子的影响。如果在一个给定的状态中只有一个孩子被移动，那么速率通过将其除以孩子的总数来调整。因此，我们假设一个孩子被随机均匀地选择来更新（这是由不可分割性假设所证明的）。如果每个孩子被选择以概率p移动，那么每个孩子看到的是总速率的一个分数p示例1（续）让我们将上述定义应用于我们的运行示例。它认为Fα[1，1]（b）=λαb1[1]b1[1]，Fα[2， 1]（b）=λαb1[2]b1[1]，这反映了自动机的唯一副本102与自动机的两个副本101中的任何一个交互的可能性。对于状态描述符使用与（2）中相同的排序，这两个函数产生等于. −1，+1，0，0，0，0，0，0，0，0，0，0，− 1，+1和分别.0，0，0，0，0，0，−1，+1，0，0，0，0，−1，+1，由于因果映射（3），α对子自动机有影响。例如，函数α1 1b11，1 [1，1]和F+11，1 [1，1 |1，1]（b）= λαb<$1 <$[1]b<$2 <$[1]b1<$1，1 <$[1，1] +b1<$1，1 <$[1，2]α1 1b11，1 [1，2]F+11，1 [1，2 |1，1]（b）= λαb <$1 <$[1]b <$2 <$[1]b1<$1，1 <$[1，1]+b1<$1，2 <$[1，2]ejiJl[hl]=L40L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27.Σrsη1r rsη1拉克里尔布里尔+e η i，c|k，...，[k]Fη i，c|k，...，k]（b）给出在自动机的第一个副本中的每个副本中的α 1，1 α看到α事件的速率。 类似的函数定义在第二个副本中。然后，相应的跳跃向量为和.0，0，−1，+1，0，0，0，0，0，0，0，0，0，0.0，0，0，0，−1，+1，0，0，0，0，0，0，0，0。3流体方程我们现在构造一组微分方程，提供CTMC平均演化的一阶近似。我们将定义这组常微分方程，近似于状态变量b=bjil[kl]. 事实上，这些变量根据（6）确定总体变量随着国家变量b取{0， 1}中的值，近似期望对应于ap。近似（随机）自动机处于给定状态的概率。这类似于[6]中考虑的马尔可夫主体的空间平均场，尽管在这里我们提供了一个不同的推导。更具体地说，按照惯例[3]，使用漂移向量构造了一组离散常微分方程，漂移向量描述了给定状态下系统变量的瞬时平均变化对于一个任意的系统，漂移定义为：F（b）：=100% 。en[k1， . ，ksη]F η[k1， . ，ksη]（b）η∈E（k1，.，ksη）∈Kηl lllLlsηcirnir，cr=1c =1m=1+1个Lll+1l llL（十）漂移方程中的求和考虑了每个变迁η在交互自动机水平上的所有可能实例及其对其子级的所有可能影响。然后，该流体ODE方程简单地为db（t）=F（b（t））。（十一）DT该方程可被视为CTMC平均值的近似方程实际上，从Dynkin公式（参见，例如，[13]）获得的平均值的真实方程为：dE[b（t）]= E [F（b（t））]。DT因此，可以通过将期望值（通常为非线性）函数F。该操作对应于实方程[2，7]的一阶近似。可执行性的近似估计L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）2741测量可以被表示为适当的确定性函数（即，（11）的解的奖励），例如在[14]中讨论的我们在这里强调，由于在前一节中仔细介绍的符号，漂移和流体方程的这种简单定义是可能的示例1（续）对于运行示例，让我们假设α是唯一定义的事件。 然后，与示例相对应的常微分方程系统（以分量表示）为：2bstec1[1]=−λαb1[1]b1[1]bstec2[1]=+λαb1[1]b1[1]˙1 11b11，1 [1，1]b<$1， 1 <$[1， 1] = −λαb <$1 <$[1]b<$2 <$[1]b1<$1，1 <$[1，1] +b1<$1，1<$[1，2]˙211b11，1 [1，1]b<$1，1 <$[1，1] = +λαb<$1 <$[1]b<$2 <$[1]b1<$1，1 <$[1，1] +b1<$1，1<$[1，2]˙1 11b11，1 [1，2]b<$1， 1 <$[1， 2] = −λαb <$1 <$[1]b<$2 <$[1]b1<$1，1 <$[1，1] +b1<$1，1<$[1，2]˙211b11，1 [1，2]b<$1，1 <$[1，2]=+λαb<$1 <$[1]b<$2 <$[1]b1<$1，1 <$[1，1]+b1<$1，1<$[1，2]bstec1[2]=−λαb1[2]b1[1]bstec2[2]=+λαb1[2]b1[1]˙1 11b11，1 [2，1]b<$1，1 <$[2，1]= −λαb<$1 <$[2]b<$2 <$[1]b1<$1，1 <$[2，1]+b1<$1，1<$[2，2]˙211b11，1 [2，1]b<$1，1 <$[2，1]=+λαb<$1 <$[2]b<$2 <$[1]b1<$1，1 <$[2，1]+b1<$1，1<$[2，2]˙1 11b11，1 [2，2]b<$1，1 <$[2，2]=−λαb<$1 <$[2]b<$2 <$[1]b1<$1，1 <$[2，1]+b1<$1，1<$[2，2]˙211b11，1 [2，2]b<$1，1 <$[2，2]=+λαb<$1 <$[2]b<$2 <$[1]b1<$1，1 <$[2，1]+b1<$1，1<$[2，2]bstec1<$2<$[1]=−λαb1 <$1 <$[1]b1<$2<$[1]−λαb1<$1<$[2]b1<$2 <$[1]bstec2<$2<$[1]=+λαb1<$1<$[1]b1<$2<$[1]+λα b1 <$1<$[2]b1<$2<$[1]为了说明如何获得一个大小（即方程的数量）与自动机实例的数量无关的微分方程模型，让我们比较一下，例如，方程bstec11[1]和bstec11[2]。假设初始条件为b1<$1<$1 <$[1]（0）=b1<$1 <$1 <$[1]（0），则在所有未来时间点的导数都相等。通过解的唯一性，这意味着两个解也是平等的。因此，可以去掉两个方程中的一个。此外，这可以通过检查漂移的定义来系统地完成以及实例函数Fη和Fη。我们可以很容易地看到，从语法上讲，+1个1sη对于每个元组（k1，...， kl）∈ Kη. 这意味着2其中，对于紧性，我们使用符号bstec表示导数。42L. Bortolussi et al. /Electronic Notes in Theoretical Computer Science 310（2015）27J.sηΣn⟨i⟩ n的实例。漂移的方程在任何代理排列下都是不变的，与阶级结构相一致。特别是，相同类的两个代理的代理的代理方程（即导出的ODE）在语法上是相同的。这一观察结果可以很容易地转化为以下内容。定理3.1假设对所有的kil，bil <$[kl]（0）=bil <$[kJl]（0）对任意两个kJl且kl，且（11）的解在[0，T]中存在且唯一.然后，它认为，对于所有的t∈ [0，T]bil[kl]（t）= bil[k Sl]（t）。证据[草图]通过在同类代理的置换下的不变性，可以得出，如果b是类不变的，即bil[kl]=bil[kJl]，对于任何kil，kl，kJl，则F<$il<$[kl]（b）=F<$il<$[k′l]（b），即向量场也是类不变的。因此，如果b是类不变的，那么b+hF（b）也是类不变的 。 固 定 h >0 ， 设x （ 0 ） =b（ 0 ） ， 且 x（ （ k+1 ） h ） =x（ kh ） +F （ x（kh））。通过一个简单的归纳，我们可以建立x（kh）对任何k都是类不变的。因此，类不变性是由欧拉积分方案保持因此，通过让h→0，它也被ODE解保持。QQ简化后的方程可以通过修改模板表达式，观察到Sj吉勒河[hl−1]=Sj=nbj：F ηij（b）：=nir<$F η.ˆb⟨i1⟩,. . . ，bikη，bil−1，Sil−1，Si1，. ，Sisη.ll llr/=j，r=1Ll（十二）这个新的模板方程是通过对一个代理的所有可能的兄弟节点求和得到的，使用的假设是，L都属于不同的阶级。述倍增因子. sη尼日勒河是η1sηr j，r=1lη1sη由于F[kl，.，KL ]（b（t））=F[kl，.，KL ]（b（t））为所有（k1，.， ksη ）1sη你好，有LSηr=/lj，r=1=（kl，...， kl）在Kη中，对于每个固定的I类主体，Rl4数值验证在这一节中，我们将对上一节中提出4.1模型描述为了说明我们的框架，让我们考虑一个系统的可执行性模型，该系统具有如下排列的四个自动机类。有两个顶级的两态自动机，分别表示一台计算机和一台L