GBT 20719.12-2010 工业自动化系统与集成 过程规范语言 第12部分：外核.pdf

I C S2 5 0 4 0 4 0L6 7雷雪中华人民共和国国家标准G B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 52 0 11-0 1-1 4 发布工业自动化系统与集成过程规范语言第12 部分：外核I n d u s t r i a la u t o m a t i o ns y s t e m sa n di n t e g r a t i o n-P r o c e s ss p e c i f i c a t i o nl a n g u a g e-P a r t1 2：0 u t e rc o r e(I S 01 8 6 2 9-1 2：2 0 0 5，I D T)2 0 11-0 6 0 1 实施丰瞀鹳鬻瓣警糌瞥星发布中国国家标准化管理委员会仪1 9目次G B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 5前言-日l 言-”1 范围一12 规范性引用文件13 术语、定义及缩略语l3 1 术语和定义13 2 缩略语54G B T2 0 7 1 9 概j 蓬55G B T2 0 7 1 9 本部分的组织56 子活动核心理论67 发生树核心理论88 离散状态核心理论一1 19 原子活动核心理论1 41 0 复杂活动核心理论1 61 1 活动发生核心理论一2 0附录A(规范性附录)S C4 标准中A S N 1 标识符的应用附录B(资料性附录)与情景演算的关系”附录C(资料性附录)使用P S L 外核描述过程的实例附录N A(资料性附录)本部分英文黑体词的含义参考文献-索引2 72 82 93 53 6前言G B T2 0 7 1 9 1 2 2 0 1 0 i s o1 8 6 2 9 1 2：2 0 0 5G B T2 0 7 1 9 工业自动化系统与集成过程规范语言目前拟分为如下部分：第l 部分：概述与基本原理；第1 1 部分：P S L 核心；第1 2 部分：外核；第1 3 部分：时序理论；第1 4 部分：资源理论；第1 5 部分：活动性能理论；第2 1 部分：E X P R E S S；第2 2 部分：x M L；第2 3 部分：U M L；第4 1 部分：定义性扩展：活动扩展；第4 2 部分：时间和状态；第4 3 部分：定义性扩展：活动次序和持续时间扩展；第4 4 部分：定义性扩展：资源扩展；第4 5 部分：资源集的种类；第4 6 部分：加工活动；第4 7 部分：过程目的。本部分为G B T2 0 7 1 9 的第1 2 部分。本部分等同采用I S O1 8 6 2 9 1 2：2 0 0 5 C 1 1 业自动化系统与集成过程规范语言第1 2 部分：外核(英文版)。本部分的技术内容和组成结构与I S O1 8 6 2 9 1 2：2 0 0 5 相一致，在编写格式上符合G B T1 1 2 0 0 0标准化工作导则第1 部分：标准的结构和编写规则。只是根据我国国家标准的制定要求和为方便使用，做了如下编辑性的改动：将“I S O1 8 6 2 9”改为“G B T2 0 7 1 9”，把“I S O1 8 6 2 9-1 2”改成“G B T2 0 7 1 9 1 2”或“G B T2 0 7 1 9本部分”。删除了I S O1 8 6 2 9 1 2：2 0 0 5 的前言，并按照我国国家标准编制要求重新起草了前言。将I S O1 8 6 2 9 1 2：2 0 0 5 第2 章“规范性引用文件”中的引导语改为G B T1 1 2 0 0 0 中规定的引导语。I s O1 8 6 2 9 1 2：2 0 0 5 标准中i n d e x 的两个关键词“m a n u f a c t u r i n gf a c i l i t i e s”和“s a t i s f i a b l e”在原标准中没有找到，所以在中文索引中删除这两个关键词。将本部分中出现的已转化为国家标准的国际标准编号改为国家标准编号，便于使用和查阅。未转化的国际标准保留。为了使读者便于理解本部分黑体词的含义，增加了附录N A。删去了原文中不符合我国标准编写要求的字句。本部分附录A 为规范性附录；附录B、附录c、附录N A 为资料性附录。本部分由中国机械工业联合会提出。本部分由全国自动化系统与集成标准化技术委员会(s A c T c1 5 9)归口。本部分起草单位：北京机械工业自动化研究所、清华大学。本部分主要起草人：刘颖、黄双喜。G B T2 0 7 1 9 1 2 2 0 1 0 Z S O1 8 6 2 9 1 2：2 0 0 5引言G B T2 0 7 1 9 是为了进行与制造过程相关的计算机可解释的信息交换所使用的国家标准。G B T2 0 7 1 9 标准包含的所有部分结合在一起，为描述贯穿整个生产过程的制造活动提供了一类语言(该生产过程可能限于一个工业公司，也可能跨越几个工业部门或公司)，并独立于任何特定的表示模型。语言的本质使得它适用于在生产过程的各个阶段共享与制造相关的过程信息。G B T2 0 7 1 9 的本部分提供了国际标准中定义的语言的核心元素的描述。G B T2 0 7 1 9 中的所有部分与制造管理领域软件应用中采用的任何特定过程的表述或模型无关。本标准的所有部分一同为改善这些应用软件的协同性提供了一个结构框架。G B T2 0 7 1 9 1 2 2 0 1 0 I s 01 8 6 2 9-1 2：2 0 0 5工业自动化系统与集成过程规范语言第1 2 部分：外核1 范围G B T2 0 7 1 9 的本部分通过使用G B T2 0 7 1 9 的一组公理和定义提供了属于P S L 语言外核的概念表述。这些公理为G B T2 0 7 1 9 外核中的术语提供了语义的公理化。G B T2 0 7 1 9 本部分的范围包括：活动和子活动的集合；离散活动和状态；活动发生的约束；基本活动的并发；复杂活动；复杂活动的发生。2 规范性引用文件下列文件中的条款通过G B T2 0 7 1 9 的本部分的引用而成为本部分的条款。凡是注日期的引用文件，其随后所有的修改单(不包括勘误的内容)或修订版均不适用于本部分，然而，鼓励根据本部分达成协议的各方研究是否可使用这些文件的最新版本。凡是不注日期的引用文件，其最新版本适用于本部分。G B T1 6 2 6 2 1信息技术抽象语法记法一(A S N 1)第1 部分：基本记法规范(G B T1 6 2 6 2 12 0 0 6，I S O I E C8 8 2 4 1：2 0 0 2，I D T)G B T1 6 6 5 6 1工业自动化系统与集成产品数据表达与交换第1 部分：概述与基本原理(G B T1 6 6 5 6 1 2 0 0 8，I S O1 0 3 0 3 1：1 9 9 4，M O D)G B T1 9 1 1 4 1 工业自动化系统与集成工业制造管理数据第1 部分：综述(G B T1 9 1 1 4 1-2 0 0 3，I S O1 5 5 3 1 1：2 0 0 2，I D T)G B T2 0 7 1 9 1工业自动化系统与集成过程规范语言第1 部分：概述与基本原理(G B T2 0 7 1 9 1 2 0 0 6，I S 01 8 6 2 9 1：2 0 0 4，I D T)G B T2 0 7 1 9 1 1 工业自动化系统与集成过程规范语言第1 1 部分：P S L 核心(G B T2 0 7 1 9 1 l2 0 1 0，I S O1 8 6 2 9 1 1：2 0 0 5，I D T)3 术语、定义及缩略语3 1 术语和定义下列术语和定义适用于G B T2 0 7 1 9 的本部分。3 1 1公理a x i o m形式语言中的合式公式，用以对一门语言的词汇中的符号解释加以约束。-G B T2 0 7 1 9 1 33 1 2保守定义c o n s e r v a t i v ed e f i n i t i o n指明充要条件的定义，充要条件是指术语应该满足并且不允许从该理论作出新的推论的条件。I-G B T2 0 7 1 9 1 3】G B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 53 1 3核心理论c o r et h e o r y表示基本概念的关系符号和函数符号的公理集。F G B T2 0 7 1 9 1 的修改3 1 4数据d a t a定义适合于人或计算机通信、解释或处理的形式化方法的信息表示。G B T1 6 6 5 6 1 3 1 5定义的词汇d e f i n e dl e x i c o n非逻辑词汇的一系列符号，表示所定义概念。注：定义的词茫分为常量、函数和关系符号。示例；具有保守定义的术语。G B T2 0 7 1 9 1 3 1 6定义性扩展d e f i n i t i o n a le x t e n s i o n指P S L 核心的扩展，它引入了完全由P S L 核心定义的新的语言术语。注：定义性扩展为P s L 核心增加了新的表达能力，但它常常定义领域应用中的语义及术语。-G B T2 0 7 1 9 1 3 1 7扩展e x t e n s i o n包含附加公理的P S L 核心的扩充。注1：P S L 核心是一组相对简单的公理，足以表达较广范围内的基本过程。然而，更复杂的过程所需的表达性资源超出了P S L 核心的范围。相对于将每一个可能的概念(其对于描述一个或另一个过程可能有用)杂乱地添加到P S L 核心中去，更好的方式是开发各种独立的、模块化的扩展，并把它们添加进P S L 核心。采用这种方式，用户可以根据自己的表达需求精确地裁剪语言。注2：所有的扩展均为核心理论或定义性扩展。F G B T2 0 7 1 9 1 3 1 8语法g r a m m a r说明如何将逻辑符号和词汇术语组合为合式公式的规范。r G B T2 0 7 1 9 1 13 1 9幂等i d e m p o t e n t一个集合中的元素(a)在内部二元运算下(0 P)具有：aO Pa a。注：对于函数，当定义域中的每个元素都是幂等的，则函数是幂等的。示例：集合理论交集和并集是幂等的，因为SnS=S 以及SUS=S。3 1 1 0信息i n f o r m a t i o n事实、概念或指令。G B T1 6 6 5 6 1 3 1 1 1解释i n t e r p r e t a t i o n一个理论中所有命题的论域和真值(真或假)指派。注：请见附录C 中解释的示例。2G B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 53 1 1 2语言l a n g u a g e词汇和语法的结合。G B T2 0 7 1 9 1 3 1 1 3词汇l e x i c o n符号和术语的集合。注：词汇包括逻辑符号(例如布尔连接和量词)与非逻辑符号。对于G B T2 0 7 1 9 来说，词汇的非逻辑部分包括用于表达本体的基本概念的词语(常量，函数符号与关系符号)。r G B T2 0 7 1 9 1 3 1 1 4制造m a n u f a c t u r i n g将原材料或半成品转换成成品的功能或行为。G B T1 9 1 1 4 1 3 1 1 5制造过程m a n u f a c t u r i n gp r o c e s s一套结构化的行为或操作，它完成了将原材料或半成品向成品的转化。注：制造过程可被安排在程序规划、产品规划、单元规划或装配位置规划里。根据战略性应用和物资的分配，制造过程可被用于支持接库存生产、按订单生产、按订单装配。G B T1 9 1 1 4 1 3 1 1 6模型m o d e l满足一种理论中所有合式公式的一组元素和事实任务的合成。注1：“模型”这个词在逻辑中的用法不同于它在大多数科学及日常读物中的用法。如果一个命题在某种解释中为真，那么就可以说这种解释是该命题的模型。这里所说的语义常被称作模型理论语义。注2：模型一般表示为包含附加结构的集合(偏序，点阵，或向量空间)。模型定义了术语的含义以及本模型中所采用语言的命题的真值概念。给定一个模型，在公理集中使用的数学结构基本公理集就通过语言及它们的逻辑关系成为概念论证的基础，因此模型的集合构成了本体的形式语义。G B T2 0 7 1 9 1 3 1 1 7本体o n t o l o g y按照词汇中术语的含义的某些规范而定的专门术语的词汇。注1：与形式语言中术语台义的规范一同给出的相关术语的结构化集合。术语含义的规范说明了术语为什么相关，如何相关，以及集合划分和构造的条件。注2：p S I(比如G B T2 0 7 1 9)的主要部分就是一个本体。基本概念就是本体论。通过G B T2 0 7 1 9 可以描述基本制造工程及业务过程。注3：本体的核心不只是术语，也包括它们的含义。术语的任意集合包含在本体中，但只有在含义一致时这些术语才能被共享。共享的是术语的指定语义，而不是简单的术语共享。注4：没有显式定义的任何术语都可能成为含糊及混乱的来源。本体论的难点是：需要建立一个框架以使框架中术语的含义清晰明确。对于G B T2 0 7 1 9 这个本体，有必要提供一个过程信息的严格的数学特性描述以爱G B T2 0 7 1 9 语言中信息的基本逻辑特性的精确表达。G B T2 0 7 1 9 1 3 1 1 8外核o u t e rc o r e作为P S L 核心扩展的核心理论的集合，在适用性中它具有很高的普遍性，因此专门预留出来。3G B T2 0 7 1 9 1 2 20 1 0 t S O1 8 6 2 9-1 2：2 0 0 5注：事实上，扩展包含了外核的公理。F G B T2 0 7 1 9 1 3 1 1 9基本概念p r i m i t i v ec o n c e p t没有保守定义的词汇术语。G B T2 0 7 1 9 1 3 1 2 0基本词汇p r i m i t i v el e x i c o n表示基本概念的非逻辑词汇的符号集合。注：基本词汇分为常量、函数符号和关系符号。G B T2 0 7 1 9 1 3 1 2 1过程p r o c e s s涉及各种企业实体的一套结构化的活动，是为特定的目的设计和组织的。注：这里所提供的定义和G B T1 6 6 6 6 4 9 非常接近。然而G B T1 9 1 1 4 需要一套结构化行为的观念，对于时间和步骤段有任何预先确定，另外，从流程管理的观点来看，为同一目的需要一些空过程，尽管实际上它们不起任何作用。G B T1 9 1 1 4 1 3 1 2 2产品p r o d u c t由天然或人造而成的事物。G B T1 6 6 5 6 1 33 1 2 3证明论p r o o ft h e o r y解释某语言的语义所必需的理论与词汇元素的集合。注：它包含三部分：P S L 核心，外核及扩展。-G B T2 0 7 1 9 1 3 1 2 4P S L 核心P S L-c o r e对于活动、活动发生、时问点、对象这些概念的公理的集合。注：P S L 核心的动机是：任何两个过程相关的应用软件都需要共享这些公理，以交换过程信息，因此P S L 核心足可用于描述制造过程的基本概念。这样，基本过程的特性描述就几乎无需那些超出描述这些过程所需的本质的假设了，因此P S L 核心在逻辑表述方面比较薄弱。尤其是，P S L 核心并不够强大，它不能提供很多辅助概念的定义，而这些辅助概念是描述关于制造过程的所有感知事物所必需的。G B T2 0 7 1 9 1 3 1 2 5半格s e m i l a t t i c e在偏序中，每两个元素都具有一个唯一的最小上界。3 1 2 6理论t h e o r y属于给定概念和概念集的公理和定义的集合。注：这个定义反映了人工智能的方法，在此方法中理论是基于相关概念的含义的假设的集合。E O B T2 0 7 1 9 1 4G B T2 0 7 1 9 1 2 2 0 1 0 l I S O1 8 6 2 9-1 2：2 0 0 53 1 2 7讨论域u n i v e r s eo fd i s c o u r s e属于一个真实世界领域的具体或抽象的事务的集合，根据其在模块化的系统和相应环境上的重要性进行选择。E G B I T1 9 1 1 4 1 13 2 缩略语下列缩略语适用于G B T2 0 7 1 9 的本部分。F O L一阶逻辑F i r s t O r d e rL o g i c；B N F巴克斯范式B a e k u s-N a u rF o r m；K I F知识交换格式K n o w l e d g eI n t e r c h a n g eF o r m a t；P S L过程规范语言P r o c e s sS p e c i f i c a t i o nL a n g u a g e。4G B T2 0 7 1 9 概述G B T2 0 7 1 9 详细描述了一种用于表示过程信息的语言，即过程规范语言。它由用于过程描述的词汇、本体和语法组成。注1：P S L 是一种以数学定义良好的词表和语法为基础，用于详细描述制造过程的语言。这样，它不同于G B T1 6 6 5 6，G B T1 7 6 4 5，G B T1 9 1 1 4 和G B T1 8 9 7 5 标准中使用的其他语言。就两个过程的信息交换而言，P S L 确定了与其行为无关的每一个过程。例如，一个过程中被视为资源的对象可能与另一个过程中被视为产品的对象被识别为同一个对象。注2：P S L 是以数学集合核心理论和情景演算(见附录B)为基础的。这样，它采用的描述方法与使用G B T1 6 6 6 6标准中定义的现存语言的方法显著不同。与其说P S L 中这些概念的含义遵循定义术语的形式集合，不如说它们遵循公理与支持定义的集合。G B T2 0 7 1 9 给出了相应的注释及举例，以辅助对该语言的基本词汇的理解。G B T2 0 7 1 9 部分l x 系列详细说明了得到G B T2 0 7 1 9 的基本概念的精确定义和公理所需的核心理论，这些核心理论可以实现不同模式之间的精确语义翻译。以下各项属于G B T2 0 7 1 9 1 x 的范畴：语言的基本要素的表示法；提供与足以描述基本过程所需的直觉语义基本概念相符的标准化公理集；发展遵循P S L 核心的其他核心理论或扩展的规则集合。以下不属于G B T2 0 7 1 9 1 x 的范畴：涉及非核心理论概念的信息表示法。5G B T2 0 7 1 9 本部分的组织本条目详细说明了组成G B T2 0 7 1 9 中本部分的基本理论。5 1 外核的扩展构成G B T2 0 7 1 9 本部分的核心理论有：一子活动核心理论(s u b a e t i v i t y t h)；发生树核心理论(o e c t r e e t h)；一离散状态核心理论(d i s c _ s t a t e t h)；原子活动核心理论(a t o m i c t h)；一复杂活动核心理论(c o m p l e x t h)；一活动发生核心理论(a c t _ o c e t h)。图1 显示了外核中这些理论间的关系，图中的箭头表示这些理论间的从属关系。外核的所有理论都是P S L 核心的扩展。原子活动核心理论是子活动理论和发生树理论两个理论的扩展，而离散状态核5G B V2 0 7 1 9 1 2 2 0 I O I S O1 8 6 2 9 1 21 2 0 0 5心理论只是发生树核心理论的扩展。活动发生核心理论是复杂活动核心理论的扩展，反之，复杂括动核心理论又是原子活动核心理论的扩展。固1S L 外核公理集合闻的关系6 子活动核心理论子活动核心理论提供了流程组成的概念的公理。子活动发生次序理论的唯一强制约束是：子活动关系要与一个离散偏序同构。其他核心理论对其具有附加的强制约束。6 1子活动核心理论的基本关系子活动核心理论的非逻辑词汇包含一个基本关系符号：s u b a c t i v i t y。6 2 子活动核心理论的定义关系子活动核心理论的非逻辑词汇包含一个定义关系符号：p r i m i t i v e。6 3 与其他公理集的关系子活动核心理论需要G B T2 0 7 1 9 1 1(P S L 核心)中所详细说明的p s i c o r e t h。子活动核心理论不需要定义性扩展。6 4 子活动核心理论的非正式语义6 4 1s u b a c t i v i t y用于s u b a c t i v i t y 的K I F 符号是：(s u b a c t i v i t y?a l?a 2)用于s u b a c t i v i t y 的非正式语义是：当且仅当活动?a l 是活动?a 2 的子活动时，(s u b a c t i v i t y?a l?a 2)在子活动核心理论的解释中为真。子活动关系在活动的集合上形成一个离散偏序。6 4 2p r i m i t i v e用于p r i m i t i v e 的K I F 符号是：(p r i m i t i v e?a)用于p r i m i t i v e 的非正式语义是：当且仅当活动?a 除它本身之外没有任何子活动时，(p r i m i t i v e?a)在子活动核心理论的解释中为真。6 5 子活动核心理论中的定义当且仅当一个活动除它本身之外没有任何子活动时，该活动为基本。6G B T2 0 7 1 9 1 2 2 0 1 0 I I S O1 8 6 2 9 1 2：2 0 0 66 5 1 定义1(f o r a l l(?a)(i f f(p r i m i t i v e?a)(f o r a l l(?a 1)(i m p l i e s(s u b a c t i v i t y?a l?a)(=g a l?a)6 6 子活动核心理论的公理6 6 1 公理1子活动是活动上的一个关系。(f o r a l l(?a l?a 2)(i m p l i e s(s u b a e t i v i t y?a l?a 2)(a n d(a c t i v i t y?a 1)(a c t i v i t y?a 2)6 6 2 公理2子活动是自反的。(f o r a l l(?a)(i m p l i e s(a c t i v i t y?a)(s u b a c t i v i t y?a?a)6 6 3 公理3子活动是反对称的。(f e r a l l(?a l?a 2)(i m p l i e s(a n d(s u b a c t i v i t y?a l?a 2)(s u b a c t i v i t y?a 27 a 1)(=?a l?a 2)6 6 4 公理4子括动是传递的。(f o r a l l(?a l?a 27 a 3)(i m p l i e s(a n d(s u h a c t i v i t y?a l?a 2)(s u b a c t i v i t y?a 27 a 3)(s u b a c t i v i t y?a l?a 3)6 6 5 公理5子活动关系是一个离散排序，故在排序中每一个活动都有一个向下的后继。(f o r a l l(?a l?a 2)(i m p l i e s(s u b a c t i v i t y?a l?a 2)(e x i s t s(?a 3)(a n d(s u b a c t i v i t y?a l?a 3)(s u b a c t i v i t y?a 37 a 2)(f o r a l l(?a 4)(i m p l i e s(a n d(s u b a c t i v i t y?a l?a 4)(s u b a c t i v i t y?a 47 a 3)(o r(=?a 47 a 1)(=?a 47 a 3)6 6 6 公理6子活动关系是一个离散排序，故在排序中每一个活动都有一个向上的后继。7G B T2 0 7 1 9 1 2 2 0 1 0 I s o1 8 6 2 9-1 2：2 0 0 5(f o r a l l(?a l?a 2)(i m p l i e s(s u b a c t i v i t y?a l?a 2)(e x i s t s(?a 3)(a n d(s u b a c t i v i t y?a l?a 3)(s u h a c t i v i t y?a 37 a 2)(f o r a l l(?a 4)(i m p l i e s(a n d(s u b a c t i v i t y?a 37 a 4)(s u b a c t i v l t y?a 47 a 2)(o r(=?a 47 a 2)(=?a 47 a 3)7 发生树核心理论发生树是活动发生的所有离散序列的集合。发生树与情景演算中情景树的子结构是同构的(见附录c)，其主要区别是：每个发生树具有一个唯一的初始活动发生，而不是唯一的初始情景。就像在情景演算中，引人了p o s s 关系来实现对发生树中活动发生的约束的说明。因为发生树包含有域的建模者认为不可能发生的序列，所以p o s s 关系就修剪掉了发生树上与这些不可能的活动发生相对应的分枝。需要注意的是，发生树并不是一个表达一个活动的子活动发生的结构。发生树并不表示一个活动的特定发生，它表示的是域中所有活动的全部发生。7 1 基本关系发生树的非逻辑词汇包含三个基本关系符号：e a r l i e r i n i t i a l；l e g a l。7 2 基本函数发生树的非逻辑词汇包含一个基本函数符号：S U C C e S S o ro7 3 与其他公理集的关系发生树核心理论需要G B T2 0 7 1 9 1 1(P S L 核心)中所详细说明的p s L c o r e t h。发生树核心理论不需要定义性扩展。7 4 发生树核心理论的非正式语义7 4 1e a r l i e r用于e a r l i e r 的K I F 符号是：(e a r l i e r?o c c l?o c c 2)用于e a r l i e r 的非正式语义是：当且仅当两个活动发生?o c c l 和?o c c 2 位于树的同一个分枝上，并且?o c c l 比?o c c 2 更接近树的根时，(e a r l i e r?o c c l?o e e 2)在发生树核心理论的解释中为真。在发生树的解释中，活动发生的所有序列的集合形成一棵树；e a r l i e r(早于)关系详细说明了树中活动发生上的偏序。7 4 2i n i t i a l用于i n i t i a l 的K I F 符号是：(i n i t i a l?o c c)用于i n i t i a l 的非正式语义是：当且仅当活动发生?o c c 是发生树的根时，(i n i t i a l?o c c)在发生树核心理论的解释中为真。8G B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 57 4 3l e g a l用于l e g a l 的K I F 符号是：(1 e g a l?o c c)用于p o s s 的非正式语义是：当且仅当活动发生?o c c 是合法发生树的元素时，(1 e g a l?o c c)在发生树核心理论的解释中为真。7 4 4p o s s用于p o s s 的K I F 符号是：(p o s s?o c c l?o c c 2)用于p o s s 的非正式语义是：当且仅当活动?a 具有一个合法发生，并且该合法发生是发生树中活动发生?o c c 的后继时，(p o s s?a?o c c 2)在发生树核心理论的解释中为真。7 4 5p r e c e d e s用于p r e c e d e s 的K I F 符号是：(p r e c e d e s?o c c l?o c c 2)用于p r e c e d e s 的非正式语义是：当且仅当在发生树中，活动发生?o c c l 早于活动发生?o c c 2，并且这两个活动发生之间的所有活动发生都对应于可能的活动时，(p r e c e d e s?o c c l?o c c 2)在发生树核心理论的解释中为真。该关系详细说明了发生树的子树，其中每个活动发生都是可能的活动的发生。7 4 6s u c c e s s o r用于s u c c e s s o r 的K I F 符号是；(s u c c e s s o r?a?o c c)用于s u c c e s s o r 的非正式语义是：当且仅当?o c c 2 表示紧接在发生树中活动发生?o c c 之后的?a 的发生时，(=(s u c c e s s o r?a?o c c)?o c e 2)在发生树核心理论的解释中为真。7 5 发生树核心理论的公理以下为发生树核心理论中的公理集。7 5 1 公理1e a r l i e r(早于)关系受活动发生的约束。(f o r a l l(?o c c l?o c c 2)(i m p l i e s(e a r l i e r?o c c l?o c c 2)(m a d(a c t l v i t y _ o c c u r r e n c e?o c c l)(a c t i v i t y _ o c c u r r e n c e?o c c 2)7 5 2 公理2发生上的e a r l i e r(早于)关系是反自反的。(f o r a l l(?o c c l?o c c 2)(i m p l i e s(e a r l i e r?o c c l?O C C 2)(n o t(e a r l i e r?o c c 27 0 c c l)7 5 3 公理3发生上的e a r l i e r(早于)关系是传递的。(f o r a l l(?o c c l?o c c 27 0 c c 3)(i m p l i e s(a n d(e a r l i e r?o c c l?o c c 2)(e a r l i e r?o c c 27 0 c c 3)(e a r l i e r?o c c l?o c c 3)gG B T2 0 7 1 9 1 2 2 0 1 0 I S O1 8 6 2 9-1 2：2 0 0 57 5 4 公理4发生树中的一个分枝是活动发生的一个全序集。(f o r a l l(?o c c l?o c c 27 0 c c 3)(i m p l i e s(a n d(e a r l i e r?o c c l?o c c 2)(e a r l i e r?O C C 37 0 c c 2)(o r(e a r l i e r?o c c l?o c c 3)(e a r l i e r?o c c 37 0 c c l)(=?o c c 37 0 c c l)7 5 5 公理5没有早于初始发生的发生。(f o r a l l(?c c c l?o c c 2)(i m p l i e s(i n i t i a l?o c c l)(n o t(e x i s t s(?O C C 2)(e a r l i e r?o c t 27 0 c c l)7 5 6 公理6发生树的每个分枝都有一个初始发生。(f o r a l l(?o c c l?o c c 2)(i m p l i e s(e a r l i e r?o c c l?o c c 2)(e x i s t s(?o c c p)(a n d(i n i t i a l?o c c p)(o r(e a r l i e r?o c c p?o c c l)(=9 0 c c p?o c c l)7 5 7 公理7每个活动都有一个初始发生。(f o r a l l(?a)(i m p l i e s(a c t i v i t y?a)(e x i s t s(?s)(a n d(o c c u r r e n c eo f?s?a)(i n i t i a l?s)7 5 8 公理8在发生树中，同一活动没有两个初始活动发生。(f o r a l l(?o c c l?o c c 27 a)(i m p l i e s(a n d(i n i t i a l?o c c l)(i n i t i a l?o c c 2)(o c c u r r e n c e _ o f?o c c l?a)(o c c u r r e n c e _ o f?o c c 27 a)(=?o c c l?o c c 2)7 5 9 公理9一个活动发生的后继是该活动的一个发生。(f o r a l l(?a?o c c)(i m p l i e s(a n d(a c t i v i t y _ o c c u r r e n c e?o c c)(a c t i v i t y?a)(o c c u r r a n c e _ o f(s u c c e s s o r?a?o c c)?a)1 0G B T2 0 7 1 9 1 2 2 0 1 0 l S O1 8 6 2 9-1 2：2 0 0 57 5 1 0 公理1 0每一个非初始发生都是另一个发生的后继。(f o r a l l(?o c c)(i m p l i e s(n o t(i n i t i a l?o c c)(e x i s t s(?a?o c c p)(=?o c c(S U C C e S S O r?a?o c c p)7 5 1 1 公理1 1当且仅当发生?o c c 2 晚于?o c c l 时，发生?o c e l 先于?o c c 2 的后继发生。(f o r a l l(?a?o c c l?o c c 2)(i f f(e a r l i e r?o c c l(S U C C E S S O r?a?o c c 2)(o r(e a r l i e r?o c c l?o c c 2)(=?o c c l?o c c 2)7 5 1 2 公理1 2活动发生受l e g a l(合法)关系的约束。(f o r a l l(?o c c)(i m p l i e s(1 e g a l?o c c)(a c t i v i t y _ o c c u r r e n c e?o c c)7 5 1 3 公理1 3如果一个活动发生是合法的，那么在发生树中所有早于它的活动发生也是合法的。(f o r a l l(?o c c l?o c c 2)(i m p l i e s(a n d(1 e g a l?o c c l)(e a r l i e r?o c c 27 0 c c l)(1 e g a l?o c c 2)7 5 1 4 公理1 4一个活动发生的结束在其后继的起始之前。(f o r a l l(?o c c l?o c c 2)(i m p l i e s(e a r l i e r?o c c l?o c c 2)(b e f o r e(e n d o f?o c c l)(b e g i n o f?o c c 2)7 5 1 5 定义1p o s s 关系介于活动和活动发生之间。(f o r a l l(?a?o c c)(i f f(p o s s?a?o c c)(1 e g a l(s u c c e s s o r?a?o c t)7 5 1 6 定义2当且仅当在排序关系中活动发生?o c c l 早