CARMA：高级定量建模语言的目标和资源约束在www.sciencedirect.com在线获取.

可在www.sciencedirect.com在线获取理论计算机科学电子笔记337（2018）155-172www.elsevier.com/locate/entcsCARMA中的目标和资源约束保罗·皮霍1 Anastasis Georgoulas2 简·希尔斯顿3英国爱丁堡大学信息学院摘要CARMA是一种最近开发的高级定量建模语言，用于设计和分析集体自适应系统。 在当前的CARMA语言中，系统中的代理由行为（作为过程捕获）和知识（表示为属性存储）组成。 本文我们提出了在目标和指标方面为智能体规范配备更复杂形式的知识的第一步，并演示了如何将这些知识集成到建模和分析中。过程我们说明了一个简单的例子，从域的群机器人的想法关键词：随机建模，集体自适应系统，目标，控制1引言集体适应系统（CAS）的例子在自然界中广泛存在，从昆虫的群集行为到人类的流行病传播模式。这些系统的特点是由大量的简单实体或代理人的感知仅限于自己的位置，但仍然与他们的邻居互动。通过这些相互作用，复杂的涌现行为可能在系统层面上形成，通常是一种很难从单个代理的简单行为中预测的这些系统的高度分布式和鲁棒性意味着它们已经成为设计高度分布式的基于计算机的系统的范例，这些系统旨在在没有人为干预的情况下操作。在一般情况下，它是难以预测的紧急行为，更难知道先验如何设计的行为，以实现系统级的目标，个别代理1电子邮件：paul. ed.ac.uk2电子邮件：anastasis. ed.ac.uk3电子邮件：jane. ed.ac.ukhttps://doi.org/10.1016/j.entcs.2018.03.0391571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。156P. Piho等人/理论计算机科学电子笔记337（2018）155因此，建模成为设计集体自适应系统的一个有价值的工具，允许相对于全局目标评估代理的可能配置。此外，这种系统的高度分布式特性意味着它们通常是资源受限的。例如，个体实体可能仅具有有限的电池寿命。因此，模型必须能够考虑非功能性需求以及功能性需求。集体自适应资源共享马尔可夫代理（Collective Adaptive Resource-sharingMarkovian Agents）是最近定义的基于代数的高级随机过程建模语言。预处理已有的工作集中在使用卡玛来探索潜在的行为，通过马尔可夫模拟的系统。当考虑非功能需求和行为目标时，它们必须被外部表达，例如作为合适的时序逻辑中的公式[2，13，6]。然而，从长远来看，我们希望能够在模型本身中表达目标，并探索在模型环境中使用控制算法。这将允许个体代理的行为被调整以实现系统目标，同时尊重适用于个体代理的资源约束作为实现这一长期目标的第一步，在本文中，我们提出了一个扩展的CARMA建模语言，它支持资源约束和系统级功能目标的指定。此扩展为CARMA提供了基本的监控功能，随后可用于推理控制策略。在模拟过程中，违反资源约束的代理在系统层面上，目标的具体化支持状态的识别，这些状态可以被视为系统行为轨迹内的理想目标。本文其余部分的结构如下。在第二节中，我们提出了CARMA进程代数。在第3节中给出了用于指定个人级资源约束和全局目标的拟议扩展的描述。在第4节中，通过群机器人模型说明了扩展。在第5节中，我们介绍了用于试验拟议变更的已开发软件工具。最后，我们在第6节结束本文。2 CARMACAMA是一种新的随机过程代数，用于表示CAS范式中开发的系统[10]。该语言提供了一组丰富的通信原语，并利用在与每个组件相关联的存储中捕获的属性，以实现基于属性的通信。例如，对于许多CAS系统，位置可能是属性之一。因此，它是直接的模型系统，其中，例如，有有限的范围内的通信，或相互作用被限制到共同定位的组件，或有空间heterogeneity在代理的行为一个集体系统由一个在环境中运行的集体组成。集合是一个多组组件，用于模拟系统的行为;它是P. Piho等人/理论计算机科学电子笔记337（2018）155157.我们让公司简介是由该语法生成的组件C的集合。一用于描述一组相互作用的代理，它们合作完成一组给定的任务。环境对代理操作的上下文所固有的所有方面进行建模，即环境介导代理交互。这是CARMA的关键特征之一。环境不是一个集中的控制器，而是更普遍和多样性的东西-真实系统的物理具体来说，环境负责设置执行操作的速率，以及接收给定消息的概率。例如，在智能交通系统的模型中，环境将决定实体（公共汽车、自行车、出租车等）在城市中移动的速率，这也可能取决于当前时间。这是导致拥堵的其他车辆的存在的抽象，其可能在一天中的不同环境的作用也与CAS的空间分布性质有关-我们期望代理的位置将对代理可以做什么产生CARMA组件捕获在系统中操作的代理。 组成一个过程，描述代理存储是一个将属性名映射到基本值的函数。位于CARMA组件内的进程通过定义的通信原语与其他组件交互。具体来说，CARMA支持单播和广播通信，并允许本地同步，但全局异步通信。与变量和潜在接收者相关的不同谓词（属性上的布尔表达式）用于过滤可能的交互。因此，组件只有在其存储满足目标谓词时才能接收消息。类似地，接收者也使用谓词来标识接受的源。只有当发送者满足接收者使用的谓词，并且接收者满足发送者使用的谓词时，才会发生交互。通信行为的执行需要时间，时间是一个指数分布的随机变量，其参数由环境决定。更正式地说，我们让SYS是由以下语法定义的CARMA系统S的集合S：：=E中的N其中N是集合，E是环境。 我们让Col作为集合N，由以下语法生成：N：：=CN N一个集合N要么是一个成分C，要么是集合的平行组合N1N2.组件的精确语法是：C：：= 0 . （P，γ）分量C可以是由0表示的非活性分量，或者是由0表示的非活性分量的项。158P. Piho等人/理论计算机科学电子笔记337（2018）155form（P，γ），其中P是一个过程，γ是一个存储。存储是一个函数，属性名称为基本值。我们让：• ATTR是属性名称a，AJ，a1，.. .，b，BJ，b1，.. . ;• VA l是基本值v，vJ，v1，.. . ;• r是存储器的集合γ，γ1，γJ，. . ，即， 从A TTR到V A l的函数。组件的行为通过过程P指定。设PR oc是CARMA过程P，Q，. . .由以下语法定义：P，Q：：=零| 行为P|P+Q|P|Q| [π] P| 杀| A（A=ΔP）act：：=α<$[πs]<$−→e<$σ| α[πr]<$−→e<$σ| α<$[πs]（−→x）σ| α[πr]（−→x）σe：：= a|my.a|X|v|现在|·· ·πs，πr，π：：= T| ⊥ |e1da e2|¬π|π∧π| · ··过程规范是相当标准的，前缀，选择和并行组合都具有通常的含义。谓词π用于指示进程仅在谓词为真时才有效。区分进程kill从集合中删除封闭组件。在操作描述中，使用了以下符号：• α是集合AcT TTYPE中的动作类型;• πs和 πr是定义可接受通信伙伴的谓词• x是变量集合VAR中的变量;• e是表达式集合EXP4中的表达式;• -→·表示元素的序列• σ是更新，即更新集合中从Γ到Dist（Γ）的函数;其中Dist（Γ）是Γ上的概率分布的集合形式上，环境由两个元素组成：全局存储γg，其对系统的整体状态进行建模，以及演化规则ρ，其是一个函数，取决于全局存储和集体的当前状态（即， 在集合中每个组件的配置上），返回一个函数元组ε=μp，μw，μr，μu：[4]为简洁起见，省略了表达式e 我们只假设表达式是使用值、属性（有时以my为前缀）、变量和特殊项的适当组合构建。后者用于表示当前时间。P. Piho等人/理论计算机科学电子笔记337（2018）155159• μp：Γ×Γ×ACT→[0，1]，μp（ γs，γr，α）表示当 α被执行时，具有存储γr的组件可以从具有存储γs• μw：Γ×Γ×AcT→[0，1]， μw（ γs，γr，α）产生权重，该权重将用于计算当 α被执行时具有存储γr的组件可以从具有存储 γs• μr：Γ×ACT→R≥0， μr（ γs，α）计算动作 α在存储有 γs的组件上的执行速率;• μ u：Γ×Ac T→λ×Col，μ u（γ s，α）决定了在具有存储γ s的组件上执行动作α所引起的环境（全局存储和集体）的更新。为了从模型中提取观测值，CARMA规范还包含一组度量。每一个度量都被定义为：measurem name [var1 = range1，.，varn= rangen] = expr;表达式expr可用于统计或计算有关系统中运行的组件的属性值的统计信息。这些表达式用于计算在所有表达式的存储中计算的表达式expr分别满足布尔表达式保护的分量CARMA的形式语义产生了一个连续时间马尔可夫链（CTMC）。系统的状态空间被表示为有限的离散状态集，状态转换的时间由模型描述给出的速率决定 由CARMA模型生成的状态空间通常太大，分析上易于处理，因此通过模拟各个时间轨迹来分析模型。Eclipse支持CARMA模型的规范和分析插 件 [1] 和 模 型 模 拟 器 。 该 插 件 实 现 了 一 种 适 当 的 高 级 语 言 ， 名 为CARMASpecification Language，通过提供受主流编程语言启发的丰富语法结构，简化了CARMA3捕获要求在我们目前的工作中，我们考虑两种不同形式的要求或约束条件下，CAS可能会受到。首先，CAS的高度分布式特性意味着系统中的各个组件在访问它们完成任务所需的资源时可能受到限制即使在一个需要组件协同工作的系统中，它们也可能竞争资源。我们可以将其视为单个组件在给定资源范围或约束内运行的要求。相反，在全局级别，系统需求通常是根据全局状态空间上必须满足的目标或条件来表述的，可能在给定的时间范围内。在本节中，我们将考虑如何扩展CARMA建模语言，160P. Piho等人/理论计算机科学电子笔记337（2018）155为了以自然的方式捕捉这两种形式的需求。3.1个体限制我们将注意力限制在基于个人的资源使用限制上，特别是，我们指出，在某些情况下，这些是硬约束，当违反导致个别组件失败。在其他情况下，我们可能需要考虑当违反时使组件无法对当前任务做出贡献的约束-例如，与集体的其余部分的连接丢失。此外，这样的个体级约束也可以用来模拟超时行为或诱导组件故障，由于缓冲器超过流。我们选择这种观点，因为它似乎最符合CARMA模型中组件的半自治性质我们的目标是支持监测各个组件，资源限制。例如，这将使我们能够轻松地跟踪故障组件的定义，并通过允许通过约束隐式定义组件故障来因此，我们扩展的CARMA 语言，以便为各个组件指定约束导致定义：C：：= 0|（P，γ，c（γ））其中，如前所述，C要么是空进程，要么定义为P和本地存储γ，c（γ）表示存储属性上的一组约束。集合c（γ）由定义由以下语法给出的存储变量的约束的表达式组成：c（γ）：：= e|埃雷e：：=xoxo∈ {<，>，≥，≤，=，/=}x：：= k |γ（a）k是一个常数，γ（a）是存储γ中属性a的值也就是说，组件约束被定义为对商店属性的评估的线性不等式和等式的合取因此，我们假设资源使用被记录为组件中的一个属性CARMA规范语言[1]的实现允许定义接受数值的属性。由于底层模型是一个有限状态CTMC，并且属性编码在组件的状态中，因此我们需要一组可能的属性值是可数的-例如，实数或整数的有限子集。此外，可以通过指定枚举类型（如颜色）来定义分类属性，作为一组命名值，例如红色，蓝色和绿色。在建模工具的当前实现中，枚举类型的值是不有序的，因此在这里我们限制自己考虑数值属性，其中可以以上面给出的形式规定约束P. Piho等人/理论计算机科学电子笔记337（2018）155161约束规范需要被纳入语言的形式语义中。考虑以下CARMA过程：[π1]α<$[π2]<$x <$σCARMA模型的模拟器如下进行：（i）评估谓词π1以检查动作是否可能（ii）评估过滤谓词π2以获得消息x的所有可能接收者（iii）在系统中所有动作的上下文中评估演化规则（iv）从可以执行的动作集中采样动作。假设执行了动作α，我们根据σ更新本地存储。检查约束的两个自然位置是在检查谓词π1时或在计算存储更新之后。我们选择前一种方法，因为它允许我们将约束包含在动作的守卫集中，并使用现有的实现，只需最少的修改。换句话说，在上面的例子中，如果我们考虑一个约束c（γ），那么结果中的过程变为：[π1<$c（γ）]α<$[π2]<$x <$σ采用这种方法并不能确保在组件的演化过程中不会违反约束。 例如，考虑商店属性b= 2并且约束b≥0。假设执行的操作将以以下方式减少约束：b←b−3这意味着只有在动作触发之后才违反约束-这可以通过动作触发来解释，尽管缺乏资源。可以通过检查在执行动作之后不会违反约束来阻止触发这样的这导致了一些技术困难，因为一般来说，更新σ是概率性的，并且返回可能更新的商店值的概率分布。选项之一是为组件规定附加的约束集合c（σ（b）），使得b上的更新σ的可能结果也必须满足b上的约束。在目前的工作中，我们选择了一种替代方案，让建模者以最合适的方式显式处理这种边界情况。因此，为了将各个约束集成到CARMA模型的操作中，我们根据守卫对约束定义进行语义化在给定的CARMA模型中的过程及其操作。我们定义了从扩展了约束的语法定义的C ARMA分量集（记为Com Pc）到C ARMA分量集COMp的平移，如第2节所示。例如，动作前缀的翻译如下：.法P，γ，c（γ）−t−ra−n−s−la−ti−o→n.[c（γ）]act. [c（γ）]P+[<$c（γ）]停止。nil，γ这意味着由过程动作P、存储γ和约束集c（γ）定义的组件c被转换为组件。 特别地，约束被包括作为对过程act.P的保护，使得如果约束被违反，则组件将无法执行其通常的动作。相反地，162P. Piho等人/理论计算机科学电子笔记337（2018）155−−−−−−−→−−−−−−−→−−−−−−−→如果不满足约束，组件将只能执行特殊的操作stop，将组件转换为nil进程定义的非活动组件。我们将动作停止定义为一个没有接收者和消息的广播动作stop：= stop[]{}同样，我们给翻译的过程语法，处理选择，并行组成和警卫的过程中的其余元素。.P，γ，c（γ）翻译.[c（γ）] P +[<$c（γ）]停止。nil，γ. P+ Q，γ，c（γ）−t−ra−n−s−la−ti−o→n. （[c（γ）]P+[c（γ）]Q） +[<$c（γ）]停止。nil，γ. P<$Q，γ，c（γ）.[π]P，γ，c（γ）翻译. （[c（γ）] P <$[c（γ）] Q）+[<$c（γ）]停止。nil，γ.[π <$c（γ）] P +[<$c（γ）]停止。nil，γ因此，使用这种方法，可以在现有的CARMA框架中编码个人级别的约束。在CARMA规范语言中实现约束提供了一种清晰而紧凑的方式来捕获组件依赖于某个有限的资源。上述翻译由建模工具自动执行。这使得建模者可以专注于行为和约束，而不必显式地处理违反约束的组件的后果。建议的实现允许为每个组件类型定义不同的约束集，并允许在具有单个约束或约束集的系统中初始化组件的限制。这提高了CARMA模型的可重用性，因为可以很容易地考虑不同个体约束图1展示了CARMA规范语言的扩展语法。我们的目标是给出模型结构的概念，因此我们没有给出 特定约束的定义或代理人或其机构的完整定义。特别是，组件- 遗漏用“.”表示。. “.图1中Agent的组件块扩展为约束块，其中定义了约束，在本例中为约束1和约束2。在系统System中初始化Agent类型的组件时，关键字following用于指示Agent正在使用的约束。3.2全球目标在本节中，我们将重点转移到系统的全球目标。全局目标可以表示系统的期望功能行为或全局属性。前者的一个例子是指定我们希望组件导航到的目标位置。所需全局属性的一个示例是故障组件的数量小于给定的界限。显然，这些目标必须与限制因素区别对待，因为预计系统不会启动P. Piho等人/理论计算机科学电子笔记337（2018）155163组件代理{...约束{ 1}约束_1{... } 的情况;约束_2{...};}}system系统{collective{newAgent（.. . ）@（x，y）遵循约束_1;n∈Agent（.. . ） @（x}环境{ ... 个 文件夹}.Fig. 1.实例化具有不同约束的零部件。在一个满足既定目标的状态下。因此，当单个约束确定要避免的状态时，目标确定要瞄准的状态我们限制自己考虑基于国家的目标。这意味着目标隐含地定义了模型的一组状态，在这些状态中实现了期望的行为。上面提到的目标位置和故障组件示例都是基于状态的目标的实例。具体地说，通过规定目标位置，我们说我们对系统的那些状态感兴趣，在这些状态中，组件已经到达目标。相比之下，基于轨迹的目标将根据轨迹来描述目标，即轨迹或带时间戳的状态序列。这将是必要的，以考虑建模系统的定时特性。例如，说目标位置必须在T个时间单位内到达，这将导致我们考虑系统到时间T的轨迹。然而，在本文中，我们专注于基于状态的目标，和基于概率的目标留下进一步的工作。一般来说，基于状态的目标可以很容易地被监控：在系统遇到的每个状态，我们都可以决定目标是否满足。因此，给定一个模拟轨迹，我们可以基于这样的目标对其进行注释。这可以在线或离线完成。请注意，这不会改变系统的行为，因此模型的语义保持不变。在未来的工作中，我们希望引入更复杂的控制思想，通过模型环境中使用的进化规则，将全局目标用于然而，在本文中，我们使用基于全球目标的基本在线监测作为起点。全球目标的具体内容如下。 首先，我们将兴趣度量定义为从状态到R的函数，如第2节所述。这些目标以类似于基于个人的约束的形式被具体化。特别是，每个目标都被表达为在定义的度量上的不平等和平等的结合语法164P. Piho等人/理论计算机科学电子笔记337（2018）155这些目标定义如下：g：：= u|乌鲁u：：=yoyo∈ {<，>，≥，≤，=，/=}y：：= k |m（s）k是常数，m（s）是状态s中的度量m的值在实施过程中，我们利用了CARMA工具的现有部分特别是，CARMA规范语言已经支持定义的措施，以提取观察和研究模型的行为。例如，定义为测量停止=#{机器人[停止] | true};将返回一个时间轨迹的数量命名为机器人的组件是在状态停止。 对于监控目标是否满足，我们感兴趣在布尔测度中。假设我们有一个目标，即处于停止状态的机器人组件的数量小于5。这可以用以下方式表示测量停止小于5= 2016年02月03日02：00 - 01：00（#{机器人[停止] |true}<（5））;其中bool2int是一个帮助函数，它将布尔值转换为整数，以便测量仍然是所实现的模型模拟器所需的数值。我们简单的初始实现相当于将定义的目标映射到上面给出的StoppedLessThan5示例中的度量。然而，由于当前语言及其实现的限制，无法在环境中访问度量值，因此无法在演化规则中使用它们。为了能够直接使用的措施，在作出控制决策的CARMA语言将需要修改在未来的工作。4案例分析在本节中，我们给出了一个简单的例子，说明如何将所提出的个人级资源约束和全局目标的思想用于分析来自群体机器人领域特别是，我们考虑一个模型的一群10个机器人在4 × 4网格上导航。机器人可以选择向北或向东移动。向北的动作对应于在平面的y同样，东递增x坐标。通过禁用将机器人带出网格的操作，机器人被约束到4 × 4网格。这是通过在动作上设置一个保护来完成的，该保护检查增加的位置是否仍然在网格内通过构建模型，每个机器人从位置（0，0）开始，并通过采取可能的路径之一来移动到（3，3）。 如果我们设定动作的速率在这种情况下，r= 1，那么每个路径都是同样可能的，P. Piho等人/理论计算机科学电子笔记337（2018）155165额外的限制。这个基本模型的结构如图2a所示。请注意，在此模型中，组件之间没有交互。这样的模型足以展示个体约束和全局目标，同时模拟速度非常快。以后的工作将考虑更复杂的系统，包括组件之间的通信。我们在这个模型中考虑的资源是机器人的电池寿命。 机器人被赋予一个本地存储属性，表示为b，用于跟踪其电池电量。特别地，我们让属性值10表示满电池，并将系统中的每个机器人实例化为b=10。我们通过为移动机器人的动作设置概率存储更新来模拟电池耗尽也就是说，我们定义了两组位置。第一组对应于机器人在正常能量消耗下运行的位置，图2中为灰色，而第二组对应于机器人必须花费更多能量的位置具体地，在灰色位置处执行的每个动作以相等的概率将电池电平降低0或1。另一方面，在红色位置，电池电量以相等的概率降低4或5。然后，我们为每个机器人设置资源约束b >0。这个约束可以用一种显而易见的方式来解释：为了使机器人正常工作，它的电池必须不为空。每个机器人需要执行6个动作才能从（0，0）移动到（3，3）。然而，由于电池寿命是一个考虑因素，一些可能的路径可能会消耗太多的电池，导致机器人在到达（3， 3）之前失败。例如，假设一个机器人已经走了一条包含两个红色位置的路径，那么它在（3，3）处的电池指示器的预期状态是10 −（4 × 0）。5 + 2 × 4。5）=− 1。 因此，我们期望通过两个红色节点的机器人违反约束。图3、图4和图5的左侧绘制了（3， 3）处的机器人预期数量和停止机器人的预期数量与时间的关系。通过对所创建的CARMA模型进行5000次模拟来获得轨迹，每个轨迹由100个样本组成以95%置信区间绘制轨迹平均值。由于大量的模拟运行，平均值周围的这些间隔非常窄。在红色和灰色位置的场景中，在到达（3， 3）之前耗尽电池的机器人的预期数量在所有情况下都很高-通过采取随机路径，许多机器人将访问两个红色位置。因此，我们在个人层面的约束下建立了一个简单的系统模型-在这种情况下，电池寿命。下一步是推广使用全球目标。 如上所述，全局目标可以是系统的功能目标，也可以是某些期望的全局属性。在这种情况下，我们感兴趣的是机器人群到达位置（3， 3）。我们可以指定需要到达目标的机器人数量，以便系统成功完成其预期功能。假设在这种情况下，我们需要五个或更多的机器人到达位置（3， 3）以满足目标。相反，我们也可以规定不超过5个机器人不能达到（3，3），这是等价的，因为所有没有失败的机器人都会达到（3，3）。166P. Piho等人/理论计算机科学电子笔记337（2018）155（0，3）（1，3）（二、三）（三，三）津西路北北北北（0，2）（一、二）（二，二）（三，二）津西路北北北北（0，1）（1，1）（2，1）（3，1）津西路北北北北（0，0）（1，0）（2，0）（3，0）津西路（0，3）（1，3）（二、三）（三，三）津西路北北北北（0，2）（一、二）（二，二）（三，二）津西路北北北北（0，1）（1，1）（2，1）（3，1）津西路北北北北（0，0）（1，0）（2，0）（3，0）津西路(a) 无约束机器人群体模型的空间结构。(b) 第一次实验的空间配置（0，3）（1，3）（二、三）（三，三）津西路北北北北（0，2）（一、二）（二，二）（三，二）津西路北北北北（0，1）（1，1）（2，1）（3，1）津西路北北北北（0，0）（1，0）（2，0）（3，0）津西路（0，3）（1，3）（二、三）（三，三）津西路北北北北（0，2）（一、二）（二，二）（三，二）津西路北北北北（0，1）（1，1）（2，1）（3，1）津西路北北北北（0，0）（1，0）（2，0）（3，0）津西路(c) 第二个实验的空间配置 （d）第三次实验的空间配置图二.机器人群体模型的空间结构。红色节点表示动作需要更多能量的位置。通过建设。 因此，全球利益衡量标准是测量停止=#{ Robot[nil] | true}给出已经违反了它们各自的约束并且最终处于它们不能执行附加动作的状态的机器人组件的数量，或者可替换地，测量RobotsAtTarget=#{Robot[ReadyToMovee]|我是。loc==[3，3]}其给出了处于位置（3，3）并且处于ReadyToMove状态的Robot组件的数量，该状态指示它们准备好执行另一个移动动作的状态因此，全局目标可以定义为Stopped≤5。第3.2节中描述了导出一个度量来记录系统是否满足该目标。 注意P. Piho等人/理论计算机科学电子笔记337（2018）155167Occupational at（3， 3）停止机器人在（3，3）OTS铜顶罗布奥克街Occupational at（3， 3）停止机器人E（停止次数≤5）E（停止次数≤5）E（停止次数≤5）E（停止次数≤5）预计机器人预计机器人10 108 86 64 42 200 2 4 6 8 10 12 14时间00 2 4 6 8 10 12 14时间1 .一、00。80。60。40。21 .一、00。80。60。40。20。00 2 4 6 8 10 12 14时间0。00 2 4 6 8 10 12 14时间图三. 具有空间配置的非受控（左）和受控（右）系统的仿真结果 由图2b表示。10 108 86 64 42 200 2 4 6 8 10 12 14时间00 2 4 6 8 10 12 14时间1 .一、00。80。60。40。21 .一、00。80。60。40。20。00 2 4 6 8 10 12 14时间0。00 2 4 6 8 10 12 14时间见图4。 具有空间配置的非受控（左）和受控（右）系统的仿真结果 图2C。对于单个模拟运行，结果将是时间的二元函数。另一方面，对于5000次模拟运行，CARMA模拟工具的输出是对应于以下情况的轨迹比例的聚合度量：预计机器人预计机器人奥克街铜顶罗布在（3，3）OTS168P. Piho等人/理论计算机科学电子笔记337（2018）155Occupational at（3， 3）停止机器人Occupational at（3， 3）停止机器人E（停止次数≤5）预计机器人E（停止次数≤5）10 108 86 64 42 200 2 4 6 8 10 12 14时间00 2 4 6 8 10 12 14时间1 .一、00。80。60。40。20。00 2 4 6 8 10 12 14时间1 .一、00。80。60。40。20。00 2 4 6 8 10 12 14时间图五. 具有空间配置的非受控（左）和受控（右）系统的仿真结果 由图2D所示。所拥有的财产。我们可以将其解释为系统满足目标的期望概率。图3、图4和图5的左侧给出了三种不同网格配置下与目标相对应的测度的时间演化。正如预期的那样，在不受控系统的情况下，满足目标的概率很低。在图3的例子中，我们指出预期目标满意度最终远离极端1和0。这意味着系统的随机行为产生了足够的方差，导致目标满意度的高度不确定性请注意，在图3中，与位置（3，3）处的机器人数量相对应的度量与预期相矛盾，因为它不是单调增加的。这是一个与第3.1节中的讨论相关的建模伪影，是由于在执行操作后检查约束。特别地，一些机器人将到达目标位置（3，3），但立即进入故障状态。在这个例子中，我们选择将它们视为失败的机器人。现在我们可以研究当应用简单的控制策略时，满足目标的期望是如何变化的。特别是，假设机器人可以感知它是否正在移动到红色或灰色位置。有了这些信息，我们可以给出一个控制策略：如果机器人可以在红色位置和灰色位置之间选择，它会选择灰色。同样，在图3、图4和图5的右侧给出了针对三种不同空间配置模拟受控系统所产生的测量轨迹。 我们已经画出了机器人的预期数量在（3，3），停止机器人和目标被满足的期望概率在图2b和2c中给出的空间配置的情况下，预计机器人P. Piho等人/理论计算机科学电子笔记337（2018）15516922. Σ. Σ在图3和图4中的响应仿真结果中，我们看到所有机器人都被期望以高概率到达位置（3， 3）。这由位置（3，3）处的预期占用度量增长到10并且停止的机器人的预期请注意，在这些情况下，简单的控制策略足以使机器人采取最多一个红色位置的路径。因此，机器人到达位置（3，3）的最坏情况场景电池电量为0时，16空间配置在图2b中，概率为1.5，在图2c中，这使得任何单个机器人都不太可能停止，因此我们期望目标以非常高的概率得到满足在图2d中给出的空间配置和图5中的模拟轨迹的情况下，我们看到，尽管改进非常轻微，但即使在给定的控制策略下，大多数机器人也无法达到（3，3）这是由红色位置的放置来解释的。所有的机器人首先被引导到位置（1， 0），从那里位置（1， 1）和（2， 0）是同样可能的。所有选择到（2，0）的机器人很可能无法到达（3，3），因为从（2，0）开始的所有路径都需要经过另一个红色位置。从（1， 1）出发，机器人又有两个同样可能的目的地--特别是（1， 2）和（2， 1）。采取通过（2，1）的路径的机器人再次可能失败，而只有通过（1，2）的机器人将以高概率到达目的地5翻译工具我们已经开发了一个软件工具来实验对CARMA语言的拟议更改。该实现包括对解析机制的扩展，以支持新的语法，但不改变模拟框架。相反，它转换模型，使其仅使用标准的CARMA语法， 因此可以用现有的软件进行分析和模拟在CARMA规范语言中，模型包括一个或多个称为scenarios的变体（在图1中用system关键字表示），它们描述了模型和环境的不同初始化。在扩展的语法中，每个场景还指定了应该考虑哪些单独的约束和全局目标。这允许通过从定义的全套约束和目标中进行选择来轻松创建不同的变量。该工具将CARMA模型和场景名称作为输入，通过检查解析器生成的语法树，构建一个新的CARMA模型，该模型反映了指定的约束和目标。结果模型在三个方面与原始模型不同。首先，它只包括所选择的场景，其余的被丢弃。其次，按照3.1节中的映射，通过添加新的守卫和进程来适当修改组件定义。第三，每个目标都被一个度量所取代，如果目标被满足，则该度量在任何给定时间的值为1，如果目标不被满足，则该度量为0。在算法1中以伪代码描述了变换过程。这个原型实现允许使用新的170P. Piho等人/理论计算机科学电子笔记337（2018）155语言特色虽然简单，但这是整合此处提出的更改的第一步。我们设想，未来发布的CARMA工具不仅将支持语法，还将修改模拟器，以完全和原生地考虑目标和约束的存在，从而允许基于目标的执行控制。算法1实现所执行的转换的草图排除给定方案对于每个组件，创建所有约束的连接，如第3.1节所述添加防护并停止进程端对于每个全球目标，创建一个度量，表示目标是否满足，如第3.2节所述端从场景定义中删除目标和约束从模型中删除其他场景六、结论随机过程代数已被证明是CAS中涌现现象分析的有用建模范式[3，12，11，5]。本文中的工作是通过研究高度分布式的基于计算机的系统（如机器人群和无线传感器网络）中的涌现行为来推动的。特别是，我们感兴趣的是应用过程代数框架来指导这样的系统的控制策略的设计。Winfield等人[14]是应用形式化方法研究CAS，特别是机器人群的早期工作的一个例子。本文提出了一种机器人群体模型，其中个体的行为以线性时序逻辑公式的形式给出。其目的是使用自动定理证明方法来证明或反驳是否给定的紧急性质，也表示在线性时序逻辑，持有。Brambilla等人采用了一种更密切相关的方法，将形式化方法和建模应用于CAS的设计，特别是群体机器人。 [4]和Konur et al. [8]的一项建议。这两篇论文都讨论了基于种群的群体模型的模型检验特性最后，最近的工作是使用机器人群的正式模型，结合基于逻辑的期望属性规范，用于控制策略的自动合成[7，9]。在本文中，我们提出了一个扩展的CARMA过程代数及其相应的建模工具。首先，我们注意到CAS通常具有资源受限的代理-例如，受电池寿命限制。我们扩展了CARMA语言，以适应规定的个人级别的约束，当违反时，导致给定的组件失败。第二个扩展的动机是注意到CAS的期望行为通常是用系统级行为而不是单个组件的行为来表示的提出了一种P. Piho等人/理论计算机科学电子笔记337（2018）155171CARMA建模语言的扩展，用于指定所需的系统属性和功能目标，以系统的全局度量。该扩展提供了基本的监控功能，为以后推理和设计控制策略提供了一个有价值的平台。从群体机器人领域的一个例子，展示了使用资源约束和全局目标的分析CAS。特别是，一个机器人群体的模型，给出了一个简单的控制策略，并与不受控制的情况下进行了比较。在这两种情况下，系统的模拟轨迹进行监测，以满足规定的全球目标。作为进一步的工作，我们将考虑目标监控可以用来适应组件的方式，通过在环境中的进化规则的操作，以引导系统朝着满足规定的目标。确认这项工作得到了EPSRC为爱丁堡大学信息学院普适并行计算博士培训中心（http：//pervasivepallelism.inf.ed.ac.uk/）提供的EP/L01503 X/1资助。引用[1] CARMA Eclipse Plugin -用于分析集体自适应系统的QUANTICOL工具集。URLhttp://quanticol.sourceforge.net/?第27页[2] Aziz，A.，K. 桑瓦尔河谷Singhal和R.连续时间马尔可夫链的模型检验，ACM Trans.Comput. 逻辑1（2000），pp.162-170。URLhttp://doi.acm.org/10.1145/343369.343402[3] 博尔托卢西湖D. Latella和M. Massink，Stochastic process algebra and stability analysis of collectivesystems ， in ： Coordination Models and Languages ，15th International Conference ， COordination2013 ， Held as Part of the 8th International Federated Conference on Distributed ComputingTechniques，DisCoTec 2013，Florence，Italy，June 3-5，2013. 2013，pp. 1-15.URLhttps://doi.org/10.1007/978-3-642-38493-6_1[4] Brambilla，M.，A. Brutschy，M. Dorigo和M. Birattari，机器人群的属性驱动设计：基于规定建模和模型检查的设计方法，ACM Trans.奥顿适应。系统9（2014），pp. 17：1-17：28。网址http://doi.acm.org/10.1145/2700318[5] Coronato，A.，V. D. Florio，M. Bakhouya和G. D. M. Serugendo，Formal modeling of socio-technicalcollective adaptive systems ， in ： Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops，SASOW 2012，Lyon，France，September 10-14，2012，pp. 187-192.网址https://doi.org/10.1109/SASOW.2012.40[6] 哈格海吉岛A. Jones，Z.孔氏E.巴尔托奇河Grosu和C. Belta，Spatel：a novel spatial-temporal logicand its