第一章

介绍

1.1 介绍

MCMAS是多智体系统（MAS）的模型检查器。MCMAS接受输入MAS规格说明和一组要验证的公式，并使用基于有序二元决策图（OBDD [1]）的算法评估这些公式的真值。只要有可能，MCMAS就会给出值为假的公式的反例和值为真的公式的证明。MCMAS允许验证多种模态，包括CTL操作符，认知操作符，这些操作符能在有或没有公平条件的情况下推理正确的行为和策略。

MCMAS还可用于运行交互式的，逐步的模拟。此外，一个图形界面作为Eclipse插件提供，其包含用于语法识别的图形编辑器，图形模拟器和用于反例的图形分析器。

多智体系统在MCMAS中使用源自解释系统[5]形式的专用编程语言进行描述。这种称为ISPL（解释系统编程语言）的语言类似于SMV语言，因为它通过变量表征代理，并使用布尔表达式表示它们的演化。

本文件的其余部分安排如下：

2.1节是一个简单的教程，简要介绍了解释系统的形式，ISPL和基本的MCMAS命令。
3.1节描述了MCMAS可执行文件的命令行选项。
3.2节包含完整的ISPL语法。
3.3节介绍了图形界面。
3.4节详细描述了MCMAS的理论背景。

1.2 安装要点概览

系统需求：

经测试的平台：x86兼容32位或64位处理器；ppc和MacIntel。
操作系统：Linux，Mac OS X，使用Cygwin的Windows；
编译器：flex 2.5.4或更高版本， GNU bison 2.3或更高版本，GNU g++ 4.0.1或者更高版本；
Eclipse 3.2和Java 1.7或者更高的版本（可选的）。
如果您想在不同的架构/配置上运行MCMAS，请随时通过mcmas@imperial.ac.uk与我们联系。

安装步骤

（仅Windows平台）在Windows XP/Vista/7操作系统上安装cygwin和g++，flex，bison这些包。详细说明可以从http://www.cygwin.com/¹ 中找到。
用tar解压MCMAS资源，输入make，你可以获取到可执行的mcmas。
（可选）通过将文件org.mcmas.ui_1.0.0.jar文件复制到Eclipse安装的插件/目录，来安装Eclipse图形编辑器插件。安装Graphviz（http://www.graphviz.org/）。然后第一次使用选项“-clean”运行Eclipse，并在MCMAS首选项中指定包含mcmas和dot（Graphviz中的程序）的目录的路径，以及Cygwin中的bin目录（如果使用Windows）。

运行mcmas

命令行中输入，请参阅example目录中的示例。
./mcmas -h
图形界面：启动Eclipse；如果插件已被识别，您应该能够创建一个新的ISPL项目并创建一个新的ISPL文件。

1.2.1 更简单的安装

我们或许可以为您的系统提供预编译的二进制版本，请通过mcmas@imperial.ac.uk与我们联系。

第二章

教程

2.1 教程

2.1.1 如何描述智体系统？

存在各种技术和语言来描述智体系统。MCMAS采用并扩展了解释系统的形式[5]，使用专用的ISPL语言。我们将智体区分为两类：“标准”智体和环境智体。环境智体用于描述“标准”智体们共享的边界条件和基础结构，其模型与“标准”智体类似（见下文）。并非所有模型都需要环境智体，因此在ISPL中是可选的。

简而言之，在MCMAS中，每个智体（包括环境智体）的特征有：

一组本地状态（例如接收方的状态“就绪”或“忙”）。
一组动作（例如“发出消息”或“打开信道”）。
描述在给定本地状态下，智体可以执行哪个动作的规则。我们将此规则称为协议（不要与网络中的协议概念混淆）。
一个演化函数，描述智体的本地状态如何根据其当前的本地状态和其他代理的动作而演变。

本地状态。本地状态通过本地变量来定义：例如，参考一个具有两个传感器的打印机，一个传感器用于调色剂（其变量可以是高或低），以及一个用于纸的传感器（其变量可以是满或空）。在这种情况下，打印机智体具有四种可能的本地状态，其对应于调色剂和纸张变量的所有可能值的组合。本地状态是私有的，即每个智体只能观察其自身的本地状态，下面讨论的所有其他参数（协议和演化函数）不能引用其他智体的本地变量。唯一的例外是所有“标准”智体都可以“窥视”某些环境变量。智体 i 可以查看的环境中的这些变量称为智体 i 的本地可观察变量。它们可以在智体 i 的协议和演化函数中被引用，因此是智体扩展的本地状态的一部分。但是，它们的值只能由环境改变，即“标准”智体只允许读取它们的值。此外，智体的认知可访问性关系（参见第3.4节）基于代理的扩展本地状态。直观地，如果一个智体的扩展本地状态保持不变，且在这个系统的所有状态下某些东西都是真的，则智体在系统的一个状态下“知道”这些东西。在本手册的其余部分，我们使用“本地状态”一词来表示“扩展的本地状态”。

动作。每个智体（包括环境）都被允许执行某些动作，例如发送消息。并假设所有其他智体都可以看到该智体所执行的所有动作。

协议。协议描述了可以在给定的本地状态中执行哪些动作。由于本地状态是根据变量定义的，因此智体的协议表示为从变量映射到动作的函数。在ISPL中，协议并不要求详尽无遗：仅指定与某些动作的执行相关的变量赋值就足够了，并通过关键字Others表示一个包含全部的赋值（见下文）。协议不需要是确定的：可以将一组动作与给定的变量赋值相关联。在这种情况下，在该集合中非确定性地选择要执行的动作。

演化函数。一个智体的演化函数描述了变量的赋值如何随其他所有智体执行动作的结果而变化。例如，一个打印机的演化函数可以规定为，如果当前本地状态（或组成本地状态的变量）是“就绪”，并且一个智体执行“发送打印作业”动作，那么打印机的下一个本地状态是“忙”。形式上，演化函数是一个函数，它返回智体本地变量的“下一个”赋值，即是关于本地变量的“当前”赋值集，环境的可观察变量以及智体已执行的动作的函数。通过联合所有智体的演化函数来计算全局演化函数。

使用ISPL的MAS描述是通过声明本地变量赋值的一组初始状态来完成的。如果多于一个状态满足分配，则随机选择初始状态。系统根据协议和演化函数从这组初始状态演变，并且该过程用于计算用户指定的公式的真值。公平条件也可以在ISPL中指定，以排除不需要的行为（例如，通信信道持续噪声或打印机被单个代理永远锁定）

在下一节中，我们将提供两个具体示例及其ISPL编码。我们参考3.4节来获得更正式的ISPL定义及其语义。

2.1.2 一个具体的例子：比特传输问题及其ISPL形式的编码

在比特传输问题[5]中，发送方S希望通过使用不可靠的通信信道将比特值传送给接收方R（见图2.1）。在此示例中，通道可能会丢弃消息，但不能篡改消息；此外，在任何给定时间，信道只能在一个方向上发送消息而在另一个方向上不发送消息。

实现通信的一种机制如下：S立即开始将比特值发送到R，并继续这样做直到它从R收到确认。R在收到比特之前什么都不做；从那时起，它将确认收据的消息发送给S。当S从R接收到第一个确认时，S停止将该比特发送到R，并且协议在此处终止。

为了以解释系统的形式编码这个例子，我们首先介绍一个Environment智体，其ISPL代码如下：

Agent Environment
  Vars:
    state : {S,R,SR,none};
  end Vars
  Actions = {S,SR,R,none};
  Protocol:
    state=S: {S,SR,R,none};
    state=R: {S,SR,R,none};
    state=SR: {S,SR,R,none};
    state=none: {S,SR,R,none};
  end Protocol
  Evolution:
    state=S if (Action=S);
    state=R if (Action=R);
    state=SR if (Action=SR);
    state=none if (Action=none);
  end Evolution
end Agent

在这种情况下，Environment没有可观察的变量（因此，此部分未出现在代码中），且它只有一个表示通信信道可用性的可变状态（例如，SR表示两个方向都可以进行通信）。因此，Environment智体有4种可能的本地状态。Environment可以执行四个动作（在这个例子中，我们对本地状态和动作使用相同的名称）：仅从发送方传输消息，从发送方和接受方传输消息，仅从接收方传输消息，不传输任何消息。在这个例子中，协议简单地规定在每个状态中Environment智体可以选择（非确定性地）任何动作。演化函数定义如下：在Evolution:下面的第一行，读作“如果Environment的（当前）动作是S，则下一个状态将是S”。从本质上讲，演化函数只是在环境的本地状态中记录最后执行的动作。通常，当关键字if右侧的布尔条件变为真时，会触发演化函数中的一条。

我们通过以下ISPL代码对智体Sender进行编码：

Agent Sender
  Vars:
    bit : { b0, b1}; -- The bit can be either zero or one
    ack : boolean;  -- This is true when the ack has been received
  end Vars
  Actions = { sb0,sb1,nothing };
  Protocol:
    bit=b0 and ack=false : {sb0};
    bit=b1 and ack=false : {sb1};
    ack=true : {nothing};
  end Protocol
  Evolution:
    (ack=true) if (ack=false) and
       ( ( (Receiver.Action=sendack) and (Environment.Action=SR) )
        or
       ( (Receiver.Action=sendack) and (Environment.Action=R) )
       );
  end Evolution
end Agent

请注意，这是一个“标准”智体，并且不存在可观察的变量。Vars部分声明了两个变量：枚举类型bit编码了发件方想要发送的比特值，和一个布尔变量ack编码是否已收到确认（可以通过使用前缀--和注释文本来添加注释）。因此，发送方具有四个可能的本地状态，其对应于bit和ack的所有可能值的组合。发送方声明了三个动作：发送比特值0，发送比特值1，什么都不做。发送方的“协议”部分定义了如何执行这些动作。通常，协议的每一行都以变量值的布尔条件开始，后跟冒号，后跟布尔条件为真时允许的动作列表。协议的行不需要是详尽的：如果不是，则需要使用特殊关键字Other来指定当布尔条件都不为真时要执行的动作（例如，在这种情况下引入“什么都不做”动作）。在这种情况下，演化函数很简单：发送者仅在变量ack的值为false并且从接收方收到确认时才更改它的值（并且变量bit不会改变其值）；请注意其他智体的动作通过使用含有作用域的语法AgentName.Action指定。如果未添加作用域前缀，则该值旨在引用本智体的变量。与协议的情况一样，布尔条件列表不需要涵盖所有可能的情况：MCMAS假定，如果没有布尔条件为真，则智体的本地状态不会更改。

我们通过以下ISPL代码对智体Receiver进行编码：

Agent Receiver
  Vars:
    state : { empty, r0, r1 };
  end Vars
  Actions = { nothing,sendack };
  Protocol:
    state=empty : {nothing};
    (state=r0 or state=r1): {sendack};
  end Protocol
  Evolution:
    state=r0 if ( ( (Sender.Action=sb0) and (state=empty) and
                    (Environment.Action=SR) ) or
                  ( (Sender.Action=sb0) and (state=empty) and
                    (Environment.Action=S) ) );
    state=r1 if ( ( (Sender.Action=sb1) and (state=empty) and
                    (Environment.Action=SR) ) or
                  ( (Sender.Action=sb1) and (state=empty) and
                    (Environment.Action=S) ) );
  end Evolution
end Agent

仅为此智体声明一个枚举变量，表示是否已接收该比特及其值。智体Receiver可以执行两个动作：不执行任何动作（如果状态为空），或者如果已接收到比特，则发送确认消息。如果Receiver处于状态为空并且Sender正在执行发送位0的操作，此时环境正在双向启用传输（Environment.Action=SR）或者至少从发送方启用传输（Environment.Action=S），则Receiver演变为状态r0。状态r1的演变是类似的。

在声明Environment和agents之后，还需要五个部分来完成MCMAS的ISPL：Evaluation，InitStates，Groups，Fairness，和待验证的公式列表：

Evaluation
  recbit if ( (Receiver.state=r0) or (Receiver.state=r1) );
  recack if ( ( Sender.ack = true ) );
  bit0 if ( (Sender.bit=b0));
  bit1 if ( (Sender.bit=b1) );
  envworks if ( Environment.state=SR );
end Evaluation

InitStates
  ( (Sender.bit=b0) or (Sender.bit=b1) ) and
  ( Receiver.state=empty ) and ( Sender.ack=false) and
  ( Environment.state=none );
end InitStates

Groups
  g1 = {Sender,Receiver};
end Groups

Fairness
  envworks;
end Fairness

Formulae
  AF(K(Sender,K(Receiver,bit0) or K(Receiver,bit1)));
  AG(recack -> K(Sender,(K(Receiver,bit0) or K(Receiver,bit1))));
end Formulae

Evaluation部分介绍了在公平条件和待验证的公式中使用的布尔变量。这些布尔变量由关于智体的本地状态的布尔表达式定义。例如，如果Receiver的本地状态是r0或r1，则布尔变量recbit为真。

InitStates部分通过本地状态的布尔表达式声明了一组初始状态。

Groups部分允许定义智体组，可用于验证Formulae部分中的组模态。

Fairness部分包含一个布尔表达式列表：直观地说，要求这部分列出的所有公式必须在所有动作中永远为真。例如，在上面的例子中，要求命题envworks永远为真，这意味着环境不能永远地避开状态SR。

注意。如果任何公式都不需要组模态，则Groups部分可以保留为空，或者可以从ISPL代码中删除整个部分。这同样适用于Fairness部分。

Formulae部分包含待验证的公式列表。使用CTL时间运算符，认知算子，运算符来构建公式以推理正确的行为和策略。在上面列出的示例中，第一个公式读作“沿着所有路径，在将来的某个时刻，发送方将知道接收方知道比特值是0或者1”。在这种特殊情况下（见下文），这个公式是正确的，因为公平条件envworks。如果这个公平条件被注释掉，则公式变为假（因为环境可以无限期地禁止通信）。第二个公式声明了“总是如此，如果收到确认，则发送方知道接收方知道该比特的值”。即使公平条件被删除，该公式也是如此。本节中提供的示例和其他公式可以在MCMAS发布的源代码中的文本文件examples/bit_transmission_protocol.ispl中找到。

2.1.3 验证和模拟

在本节中，我们将介绍如何在命令行运行MCMAS，以执行上一节中介绍的例子的验证和模拟。

最小的MCMAS执行包括调用可执行文件，后跟要验证的ispl文件的名称：
$ ./mcmas examples/bit_transmission_protocol.ispl

�************************************************************************
MCMAS v1.2.2
 This software comes with ABSOLUTELY NO WARRANTY, to the extent
 permited by applicable law.
 Please check http://vas.doc.ic.ac.uk/software/mcmas/ for the latest release.
 Report bugs to <mcmas@imperial.ac.uk>
************************************************************************
examples/bit_transmission_protocol.ispl has been parsed successfully.
Global syntax checking...
Done
Encoding BDD parameters...
Building partial transition relation...
Building OBDD for initial states...
Building reachable state space...
Checking formulae...
Building set of fair states...
Verifying properties...
  Formula number 1: (AF K(Sender, (K(Receiver, bit0) || K(Receiver, bit1)))), is TRUE in the model
  Formula number 2: (AG (recack -> K(Sender, (K(Receiver, bit0) || K(Receiver, bit1))))), is TRUE in the model
done, 2 formulae successfully read and checked
execution time = 0
number of reachable states = 18
BDD memory in use = 9018016

在这种情况下，如果语法正确，MCMAS只输出在ISPL文件的Formulae部分中找到的公式的计算结果。MCMAS对输入文件执行详细的语法检查，如果存在语法错误，则不会调用验证进程。如果出现错误，MCMAS将终止并显示错误警告和详细信息。例如，如果Environment智体中state的定义中分号被删除，则MCMAS将终止，并显示以下错误：
$ ./mcmas examples/bit_transmission_protocol.ispl

************************************************************************
MCMAS v1.2.2
 This software comes with ABSOLUTELY NO WARRANTY, to the extent
 permited by applicable law.
 Please check http://vas.doc.ic.ac.uk/software/mcmas/ for the latest release.
 Report bugs to <mcmas@imperial.ac.uk>
************************************************************************
examples/bit_transmission_protocol.ispl:9.16: syntax error, unexpected LCB, expecting COLON
examples/bit_transmission_protocol.ispl has syntax error(s).

有许多选项可用于计算反例、增加详细程度等。这些选项在3.1节中有详细说明。

MCMAS的一个重要特征是运行模拟的可能性。使用命令行中的-s选项启动模拟环境：
$ ./mcmas -s examples/bit_transmission_protocol-2.ispl

************************************************************************
MCMAS v1.2.2
 This software comes with ABSOLUTELY NO WARRANTY, to the extent
 permited by applicable law.
 Please check http://vas.doc.ic.ac.uk/software/mcmas/ for the latest release.
 Report bugs to <mcmas@imperial.ac.uk>
************************************************************************
examples/bit_transmission_protocol-2.ispl has been parsed successfully.
Gloabl syntax checking...
Done
Encoding BDD parameters...
--------- Initial state ---------
Agent Environment
  state = S
Agent Sender
ack = false
  bit = b0
Agent Receiver
  state = empty
----------------------------
Is this the initial state? [Y(es), N(ext), E(xit)]:

MCMAS此时停止等待来自用户的输入。使用键N（下一个）和P（上一个）可以浏览所有可能的初始状态。使用Y选择一个初始状态：

--------- Initial state ---------
Agent Environment
state = S
Agent Sender
  ack = false
  bit = b0
Agent Receiver
  state = empty
----------------------------
Is this the initial state? [Y(es), N(ext), E(xit)]: Y
Enabled transtions:
1 : Environment : none; Sender : sb0; Receiver : nothing
2 : Environment : SR; Sender : sb0; Receiver : nothing
3 : Environment : R; Sender : sb0; Receiver : nothing
4 : Environment : S; Sender : sb0; Receiver : nothing
Please choose one, or type 0 to backtrack or -1 to quit:

选择状态时，MCMAS会输出该状态可能的转换。可以通过键入相应的数字来选择转换（在下面的示例中，选择了转换2）：

Please choose one, or type 0 to backtrack or -1 to quit:
2
--------- Current state ---------
Agent Environment
  state = SR
Agent Sender
ack = false
  bit = b0
Agent Receiver
  state = r0
----------------------------
Enabled transtions:
1 : Environment : S; Sender : sb0; Receiver : sendack
2 : Environment : R; Sender : sb0; Receiver : sendack
3 : Environment : SR; Sender : sb0; Receiver : sendack
4 : Environment : none; Sender : sb0; Receiver : sendack
Please choose one, or type 0 to backtrack or -1 to quit:

选择转换后，MCMAS将显示新状态和新状态下可用的转换。请注意，始终可以使用0原路返回，或使用-1退出。

B、使用手册