GB/T 20719.41-2010 工业自动化系统与集成 过程规范语言 第41部分：定义性扩展：活动扩展

ICS25．040．40

L67

a雪

中华人民共和国国家标准

GB／T20719．41—2010／ISO

工业自动化系统与集成

过程规范语言

第41部分：定义性扩展：活动扩展

Industrialautomationand

systemintegration--

Process

specificationlanguage

Part41：Definitionalextensions

extension：Activity

(ISO18629—41：2006，IDT)

201

1-01-14发布

中华人民共和国国家质量监督检验检疫总局考寿

中国国家标准化管理委员会仅111

GB／T18629-41：2006

20719．41—2010／ISO

目次

前言………………I

引言………………Ⅲ

1范围…………·1

2规范性引用文件1

3术语、定义和缩略语…··……………·1

4GB／T20719的第41部分～第49部分的常规组织

5GB／T

20719本部分的组织……………·………“

6菲确定性活动：置换分支结构………

7非确定性活动：折叠分支结构…·…”

8非确定性活动：分支结构和排序…-．10

9非确定性活动：重复的分支结构…“14

10活动谱：置换活动树……………·…………………·…·16

11括动谱：压实分支结构…………···……18

12活动谱：活动树和重新排序………····……·……·……………………20

13谱和子树遏制…………·……·………··……………………··………22

14活动的嵌入约束…·………··……··……·………………·…………··24

15梗概活动树……………26

16原子活动：向上并发………·……·………………·……29

17原子活动：向下并发…·……···………·-30

18原子活动谱·…………··………·……“32

19活动的前提………………·………………………··…34

附录A(规范性附录)GB／T

附录B(资料性附录)使用GB／T

附录NA(资料性附录)本部分英文黑体词的含义……………………45

参考文献……………………48

GB／T20719．41--2010／150

前言

GB／T20719《工业自动化系统与集成过程规范语言》目前拟分为以下部分：

——第1部分：概述与基本原理；

——第11部分：PSL核心；

——第12部分：外核；

——第13部分：时序理论；

——第14部分：资源理论；

——第15部分：活动性能理论；

——第21部分：EXPRESS；

——第22部分：xML；

——第23部分：UML；

——第41部分：定义性扩展：活动扩展；

——第42部分：时间和状态；

——第43部分：定义性扩展：活动次序和持续时间扩展；

——第44部分：定义性扩展：资源扩展；

——第45部分：资源集的种类；

——第46部分：加工活动；

——第47部分：过程目的。

本部分为GB／T20719的第41部分。

本部分等同采用ISO

扩展活动扩展》(英文版)。

本部分的技术内容和组成结构与ISO

《标准化工作导则第1部分：标准的结构和编写规则》。只根据我国国家标准的制定要求和为方便使

用，做了如下编辑性的改动：

20719

——将“ISO18629”改为“GB／T20719”，把。IsO18629—41”改成“GB／T20719．41”或“GB／T

20719．1”；“ISO18629—11”改成“GB／T20719．11”；

本部分”；“ISO18629-1”改成“GB／T

“ISO20719．12”。

18629—12”改成“GB／T

——将6．6的“注：GB／T20719．1—2004，3．3．8，4．2．4和5．1中阐明了GB／T20719中的语法句

20719．1

子的功能和重要性。”改成“注：GB／T2004，4．3．4中阐明了GB／T20719中的语法

句子的功能和重要性。”

——删除了IsO18629—41：2006的前言，并按照我国国家标准编制要求重新起草了前言。

1．12000中规定的

——将ISO18629—41：2006第2章“规范性引用文件”中的引导语改为GB／T

引导语。

——将本部分中出现的已转化为国家标准的国际标准编号改为国家标准编号，便于使用和查阅。

未转化的国际标准保留。

——为了使读者便于理解本部分黑体词的含义，增加了附录NA。

——删去了原文中不符合我国标准编写的字句。

I

GB／T

20719．41--2010／IS018629-41：2006

本部分的附录A为规范性附录，附录B、附录NA为资料性附录。

本部分由中国机械工业联合会提出。

本部分由全国自动化系统与集成标准化技术委员会(sAc／Tc159)]E1口。

本部分主要起草单位：北京机械工业自动化研究所，清华大学。

主要起草人：王思斯、黄双喜。

Ⅱ

GB／T

20719．41--2010／ISO

引言

GB／T20719是为了进行与制造过程相关的计算机可解释的信息交换所使用的国家标准。

GB／T20719包含的所有部分结合在一起，为描述贯穿整个生产过程的制造过程提供了一类语言(该生

产过程可能位于一个工业公司，也可能跨越几个工业部门或公司)，并独立于任何特定的表示模型。语

言的本质使得它适用于在生产过程的各个阶段共享与制造相关的过程规范和性质。

本部分提供了与在GB／T20719中定义的活动扩展相关的语言的定义性扩展的描述。

GB／T20719中的所有部分与给定的应用软件中使用的任何特定过程的表述模型无关。它们一同

为改善这些应用软件的协同性提供了一个结构框架。

Ⅲ

GB／T20719．41—2010／ISo

工业自动化系统与集成

过程规范语言

第41部分：定义性扩展：活动扩展

1范围

本部分通过使用GB／T20719语言中编写的一组定义来提供这种语言的非基本概念的规范。这些

定义为本部分中的术语提供了语义的公理化。

以下包括在本部分的范围中：

——使用GB／T20719．11—2010和GB／T

系无关的、但与例如第5章中列出的那些活动类别相关的概念的定义。

以下不包括在本部分的范围中：

——使用GB／T20719．11—2010和GB／T

关的概念的定义。

2规范性引用文件

下列文件中的条款通过GB／T20719的本部分的引用而成为本部分的条款。凡是注日期的引用文

件，其随后所有的修改单(不包括勘误的内容)或修订版均不适用于本部分，然而，鼓励根据本部分达成

协议的各方研究是否可使用这些文件的最新版本。凡是不注日期的引用文件，其最新版本适用于本

部分。

16262．1--

GB／T16262．1信息技术抽象语法记法一(ASN．1)第1部分：基本记法规范(GB／T

2006。ISC}／IEC8824—1：2002，IDT)

GB／T16656．1工业自动化系统与集成产品数据表示与交换第1部分：概述与基本原理

16656．12008，ISO10303—1：1994，MOD)

(GB／T

19114．1--

GB／T19114．1工业自动化系统与集成工业制造管理数据第1部分：综述(GB／T

2003，ISO15531-1：2002，IDT)

20719．1—2006

GB／T工业自动化系统与集成过程规范语言第1部分：概述与基本原理

(ISO18629．1：2004，IDT)

20719．11—20lO

GB／T工业自动化系统与集成过程规范语言第11部分：PSL核心

(ISO18629—11：2005，IDT)

20719．12—201018629—

GB／T工业自动化系统与集成过程规范语言第12部分：外核(ISO

12：2005，IDT)

3术语、定义和缩略语

3．1术语和定义

下列术语和定义适用于GB／T20719的本部分。

3．1．1

公理axiom

形式语言中的合式公式，用以对一门语言的词汇中的符号解释加以约束。

18629-41：2006

GB／T20719．41—2010／LSO

FGB／T

20719．1—2006]

3．1．2

数据data

一种形式化的信息表达，它适合于人或计算机进行通信、解释或处理。

EGB／T

16656．1—2008]

3．1．3

lexicon

定义的词汇defined

非逻辑词汇的一系列符号，表示所定义概念。

注：定义词汇划分为常数符号、函数符号和关系符号。

例：具有保守定义的术语。

[GB／T20719．1—2006]

3．1．4

extension

定义性扩展definitional

指PSL核心的扩展，它引入了完全由PSL核心定义的新的语言术语。

注：定义性扩展没有为PSL核心增加新的表达能力，但它常常定义领域应用中的语义及术语。

[-GB／T20719．1—2006，定义3．1．6]

3．1．5

离散制造discretemanufacturing

离散项目的生产。

例：汽车，装置或计算机。

[-GB／T19114．1—2003]

3．1．6

扩展extension

包含附加公理的PSL核心的扩充。

注1：PSL核心是一组相对简单的公理，足以表达较广范围内的基本过程。然而，更复杂的过程所需的表达性资源

超出了PSL核心的范围。相对于将每一个可能的概念(其对于描述一个或另一个过程可能有用)杂乱地添加

到PSL核心中去，更好的方式是开发各种独立的、模块化的扩展，并把它们添加进PSL核心。采用这种方式，

用户可以根据自己的表达需求精确地裁剪语言。

注2：所有的扩展均为核心理论或定义性扩展。

[GB／T20719．1—2006]

3．1．7

语法gral∞lfflar

说明如何将逻辑符号和词汇术语组合为合式公式的规范。

20719．1—2006]

[-GB／T

3．1．8

信息information

事实、概念或指令。

[-GB／T

16656．1—2008]

3．1．9

语言language

词汇和语法的结合。

[-GB／T

20719．1—2006]

3．1．10

制造manufacturing

将原材料或半成品转换成成品的功能或行为。

2

GB／T20719．41--2010／mo

注：定义采自APICS字典，第八版。

19114．1—2003]

[GB／T

3．1．11

制造过程manufacturingprocess

一套结构化的行为或操作，它完成了将原材料或半成品向成品的转化。

注：制造过程可被安排在程序规划、产品规划、单元规划或装配位置规划里。根据战略性应用和物质的分配，制造

过程可被用于支持按库存生产，按订单生产，按订单装配。

19114．1—2003]

[GB／T

3．1．12

模型model

满足一种理论中所有合式公式的一组元素和事实任务的组合。

注1：。模型”这个词在逻辑中的用法不同于它在大多数科学及日常读物中的用法：如果一个命题在某种解释中为

真。那么就可以说这种解释是该命题的模型。这里所说的语义常被称作模型理论语义。

注2：模型一般表示为包含附加结构的集合(半定序，点阵，或向量空间)。模型定义了术语的古义以及本模型中所

采用语言的命题的事实概念。给定一个模型，在公理集中使用的数学结构基本公理集就通过语言及它们的逻

辑关系成为概念论证的基础，因此模型的集合构成了本体的形式语义。

GB／T20719．1—2006|

3．1．13

本体ontology

按照词汇中术语的含义的某些规范而定的专门术语的词汇。

注1：与形式语言中术语含义的规范一同给出的相关术语的结构化集合。术语含义的规范说明了术语为什么相关、

如何相关，以及集合划分和构造的条件。

20719．可以描述基本

注2：PSL(比如GB／T20719)的主要部分就是一个本体。基本概念就是本体论。通过GB／T

的制造过程及业务过程。

注3：本体的核心不只是术语，也包括它们的含义。术语的任意集合包含在本体中，但只有在含义一致时这些术语

才能被共享。共享的是术语的指定语义，而不是简单的术语共享。

注4：没有显式定义的任何术语都可能成为含糊及混乱的来源。本体论的难点是：需要建立一个框架以使框架中术

语的含义更为清晰明确。对于GB／T20719这个本体，有必要提供一个过程信息的严格的数学特性描述以及

GB／T20719语言中信息的基本逻辑特性的精确表达。

注5：实际上，扩展合并了外核的公理。

20719．1—2006]

[GB／T

3．1．14

基本概念primitiveconcept

没有保守定义的词汇术语。

20719．1—2006]

[-GB／T

3．1．15

lexicon

基本词汇primitive

表示基本概念的非逻辑词汇的符号集合。

注：基本词汇分为常量、函数符号和关系符号。

20719．1—2006]

[GB／T

3．1．16

过程process

涉及各种企业实体的一套结构化的活动，是为特定的目的设计和组织的。

间和步骤没有任何预先确定。另外，从流程管理的观点来看，为同一目的需要一些空过程，尽管实际上它们不

3

GB／T20719．41--2010／iso18629-41：2006

起任何作用。

[GB／T19114．1—2003]

3．1．17

产品product

由天然或人造而成的事物。

[-GB／T16656．1—2008]

3．1．18

资源resource

在企业生产产品或服务中装置的任何设备、工具和手段。

注1：这里所定义的资源包括人力资源，作为一种具有给定才能和能力的特定的手段。这些工具通过指派任务而被

认为涉及制造过程。除了它们在制造过程中完成给定的任务(即原材料或组件的变换，后勤服务保证)的能力

外，不包括人力资源的个体或通用人类行为建模。作为包括人力手段的其他资源，仅从他们的功能、能力、状

态(即空闲的、忙)，它不包括任何方面的个体或共同的社会行为建模或表述。

20719．44的原材料和消耗品的定义

注2：此定义包括GB／T16656．49的定义。而适用于GB／T20719．14和GB／T

包括GB／T16656．49定义。

[-GB／T19114．1—2003]

3．1．19

理论theory

关于某个指定概念或概念集的公理和定义的集合。

注：该定义反映了人工智能方法，在该方法中。理论是一组假设，以这些假设为基础得到相关概念的含义。

20719．1—2006]

[GB／T

3．2缩略语

本部分使用了以下缩略语。

KIFFormat知识交换格式

KnowledgeInterchange

4GB／T20719的第41部分～第49部分的常规组织”

GB／T20719的第41部分～第49部分详细描述了给出GB／T20719的非基本概念的精确定义和

一组公理所需的定义性扩展。定义性扩展是引入了有关词汇的新项目的GB／T

20719．11

GB／T20719．12—2010的扩展。在定义性扩展中存在的这些项目可以用GB／T2010和

GB／T

件类型的规范中所使用的元素提供精确的语义定义。定义性扩展存在于以下范畴中：

——活动扩展；

——时间和状态扩展；

——活动次序和周期扩展；

——资源角色；

——资源集合；

——处理器活动扩展。

20719

GB／T20719的单个用户或用户团体可能需要扩展GB／T20719来详细描述目前在GB／T

的第41部分～第49部分中缺少的概念。它们应该采用GB／T20719中存在的元素来这样做。自定义

扩展及其定义组成定义性扩展，但不应成为GB／T20719的第41部分～第49部分中的一部分。

注：自定义扩展应像在GB／T20719．1—2006的5．1和5．2中所定义的那样符合GB／T20719。

以下包括在GB／T20719的第41部分～第49部分的范围内：

1)某些部分正在开发中。

4

GB／T20719．41--2010／ISO

——使用GB／T20719．11—20lo和GB／T

概念的元素的语义定义；

——约束定义性扩展中元素的使用的一组公理。

以下不包括在GB／T20719的第41部分～第49部分的范围内：

20719．11—2010和GB／T20719．12—2010中一部分的概念的定义和公理；

——作为GB／T

20719．11—2010和GB／T

——没有使用GB／T20719．12—2010中的元素来定义的元素；

——自定义扩展。

5GB／T20719本部分的组织

组成本部分的基本理论是：

——非确定性活动：置换分支结构；

——非确定性活动：折叠分支结构；

——非确定性活动：分支结构和排序；

——非确定性活动：重复的分支结构；

——活动谱：置换活动树；

——活动谱：压实分支结构；

——活动谱：活动树和重新排序；

——谱和子树遏制；

——活动的嵌入约束；

——梗概活动树；

——原子活动：向上并发；

——原子活动：向下并发；

——原子活动谱；

——活动的前提。

图l显示这些扩展与GB／T

GB／T20719本部分中的定义性扩展。箭头显示本部分中的扩展和GB／T

性。本部分中的全部理论均为GB／T207192．12—2010的扩展，GB／T

GB／T20719．11—2010的扩展。

注：GB／T20719．12—2010中的扩展之间相关性的完整图表存在于GB／T20719．12—2010的5．1中。

图1GB／T20719的定义性扩展

5

18629-41：2006

GB／T20719．41--2010／LSO

6非确定性活动：置换分支结构

本条款表征了关于非确定性活动：置换分支结构的全部定义。

6．1置换分支结构的基本词汇

置换分支结构的词典不需要基本关系。

6．2置换分支结构的概念的定义词汇

本条款中定义了以下关系：

(branch_monomorphic?a?occl?occ2)；

(branch_automorphic?a?occl?occ2)；

(permuted?a)；

(nondet_permuted?a)；

(partial_permuted?a)；

(simple?a)。

每一个概念由非正式语义和一个KIF公理来描述。

6．3置换分支结构所需的核心理论

此扩展需要：

——act—OCC．th；

——comDlex．th；

——atomic．th；

——subactivitv．th：

——occtree．th；

Sl—core．th。

——p

6．4置换分支结构所需的定义性扩展

置换分支结构不需要定义性扩展。

6．5置换分支结构的概念的定义

对于置换分支结构定义以下概念。

6．5．1Branch_monomorpbic

当且仅当最小活动树的一个分支中的原子活动发生的集合能被嵌入到另一分支上的原子活动发生

的集合中时，此一个分支对于另一分支是branch-monomorphic。

(forall(?sl?a)

(implies(and(occurrence_of?occl?a)

(subactivity_occurrence?sl?occl))

(exists(?s2)

70cc2)

(and(subactivity_occurrence?s2

7a))))))))

(mono?sl?s2

6．5．2Branch_automorphic

当且仅当最小活动树的一个分支上的原子活动发生的集合是该最小活动树的另一分支上的原子活

动发生的集合的置换时，这两个分支是branchautomorphic。

(forall(?occl?occ2)(iff(branchautomorphic?occl?occ2)

(and(branch_monomorphic?occl?occ2)

70ccl))))

(branch_monomorphic?occ2

6

GB／T20719．41—2010／ISO

6．5．3Pernmted

当且仅当最小活动树的每一个分支上的原子子活动发生的集合都是每一个其他分支上的原子子活

动发生的置换时，一个活动发生是permuted。

(forall(：?occ)(ill(permuted?occ)

(forall(?occl70cc2)

(implies(and(same_grove?occl?occ)

(same70cc))

grove?occ2

(branch_automorphic?occl?occ2))))))

6．5．4Nondet_permuted

当且仅当最小活动树的每一个分支上的原子子活动发生的集合是其他一些分支上的原子子活动发

生的置换时，一个活动发生是nondet—permuted。

(forall(?occ)(iff(nondet—permuted?occ)

(forall(?occl)

(implies(same—groVe?occl?occ)

(exists(?occ2)

(and(same_grove?occl?occ2)

(not(=?occl?occ2))

(branch_automorphic?occl?occ2)))))))

6．5．5Partial_permuted

当且仅当存在一个分支使得原子子活动发生的集合是在其他一些分支上的原子子活动发生的置

换，且存在不是任何其他分支的置换的一个分支时，一个活动发生是partial_permuted。

(forall(?occ)(iff(partialpermuted?occ)

70cc3)

(exist(?occl?0CC2

(and(same_grove?occl?occ)

70cc)

(same_grove?occ2

(not(=?occl?0CC2))

(branch_automorphic?occl?occ2)

(same_grove?occ370cc)

(forall(?0CC4)

70cc47a)

(implies(and(same—grove?occ3

(branch70cc4))

automorphic?occ3

(=?occ3

70cc4))))))))

6．5．6Simple

当且仅当一个活动树的所有分支都不是分支自同构时，一个活动发生是simple。

(forall(?occ)(iff(simple?occ)

(forall(?occl?occ2)

(implies(and(same_grove?occl?occ)

(same_grove?occ270cc)

(branch_automorphic?occl?occ2))

(=?occl?occ2)))))

6．6置换分支结构关系的语法

下列语法句子描述了用于置换分支结构的KIF中详细说明的过程描述和辅助规则。

20719．12006的4．3．4中阐明了GB／T20719中的语法句子的功能和重要性。

注：在GB／T

7

GB／T20719．41—2010／ISO18629-41：2006

(permuted_spen)：：=(forall((variable))

(implies(sametree(variable)?occ)

(occurrence_sentence)))

(nondet

permute,d-spec>：：=(forall((variable)*)

(implies(same_tree(variable)?occ)

(or(occurrencesentence>*)))

(simple_spec>)

(simple_spec)：：=(exists((variable>*)

(end(occurrence_formula>

(branch_spec)))

<occurrence

iiteral>：：=(occurrence(variable>(term>)

<occurrence_formula>：：=(occurrence_literal>l

(and(occurrence1iteral)*)

<occurrence_sentence>：=(exists((variable)*)

(occurrenceformula>)

(branclh_spec>：：=(and(same_tree(variable>?occ)十

(not(=(variable>?occ))+)

7非确定性活动：折叠分支结构

本条款表征了有关非确定性活动：折叠分支结构的全部定义。

7．1折叠分支结构的基本词汇

折叠分支结构的词典不需要基本关系。

7．2折叠分支结构概念的定义词汇

本条款中定义了以下关系：

——(branch—homomorphic?occl?occ2)；

——(f01ded?a)l

——(nondet—folded?a)；

——(parti．dfolded?a)；

——(rigid?a)。

每一个概念由非正式语义和一个KIF公理来描述。

7．3折叠分支结构所需的理论

本理论需要：

——act—occ．th；

——complex．th；

——atomic．th：

——subactivity．th；

——occtree．th；

——psd_core．th。

7．4折叠分支结构所需的定义性扩展

折叠分支结构不需要定义性扩展。

8

GB／T20719．41—2010／ISO

7．5折叠分支结构的定义

对于折叠分支结构定义以下概念。

7．5．1Branch_homomorphic

当且仅当存在从一个最小活动树的一个分支的原子活动发生的集合到此最小活动树的另一个分支

的原子活动发生的集合的映射时，此一个分支对于另一个分支是branch—homomorphic。

(forall(?occl?occ2)(iff

branch_homomorphic?occl?occ2)

(and(sanegrove?occl?occ2)

(forall(?sl?a)

(implies(and(occurrence_of．90cci?a)

(subactivity_occurrence?sl?occl))

(exists(?s2)

70cc2)

(suhactivity_occurrence?s2

7a)))))))

(hom?sl?s2

7．5．2Folded

当且仅当存在一个单独的分支，使得最小活动树的每一个分支上的原子子活动发生的集合是这个

单独的分支上的原子子活动发生的置换时，一个活动是folded。

(forall(?occ)(iff(folded?occ)

(exists(?occl)

(and(same—grove?oocl?ooc)

(forall(?occ2)

70cc)

(implies(sane_grove?occ2

(branch_homomorphic?occl?occ2)))))))

7．5．3Nondet_folded

当且仅当存在一个分支，使得最小活动树的每一个分支上的原子子活动发生的集合是第一个分支

上的原子子活动发生的置换时，一个活动是nondet—folded。

(forall(?occ)(iff(nondet—folded?occ)

(forall(?occl)

(implies(same_grove?occl?oce)

(exists(?occ2)

(and(sanegrove?occ270cc)

(not(。?occl?OOC2))

(branch

homomorphic?occl?occ2)))))))

7．5．4Partial—．folded

当且仅当存在一个分支，使得最小活动树的每一个分支上的原子子活动发生的集合是第一个分支

上的原子子活动发生的置换时，一个活动是partial_folded。

(forall(?occ)(iff(partial—folded?occ)

(exists(?occl?occ270cc3)

(and(same_grove?occl?occ)

(same_grove?occ270cc)

(not(=?occl?occ2))

(branch_homomorphic?occl?occ2)

70cc)

(sane_grove?occ3

(forall(?0CC4)

9

20719．41—2010／lSo16629-41：2006

GB／T

grove?occ470cc)

(implies(and(same

(not(=?occ370CC4)))

70cc4))))))))

(not(branch_homomorphic?occ3

7．5．5Rigid

当且仅当一个活动树中所有分支都不是分支同态，则称一个活动是rigid。

(forall(?occ)(iff(rigid?occ)

(forall(?occl?occ2)

(implies(and(same—grove?occl?occ)

(same70cc)

grove?ccc2

(not(=?occl?occ2)))

7．6折叠分支结构的过程描述语法

下列语法句子描述了用于折叠分支结构的KIF中详细说明的过程描述和辅助规则。

(folded_spec>：：=(exists((variable>)

(and(same_tree<variable>?occ)

(occurrence_axiom>))

<nondet_foldedspec>：：=(exists(<variable>)

(and(same_tree<variable>?occ)

(or(OCCurrence—axiom>*)))

folded

spec>

<partial—folded_spec>：：=(or<nondet

(rigid_spec>)

<rigidspat)t：=(exists(<variable)*)

(and(occurrence_formula>

<hranch_spec>))

(Occurrence—disjunct>：：=(occurrence_literal>J

(or(occurrence—literal)*)

(occurrence_axiom)：：=(exists(<variable>*)

<occurrence—disjunct>)

8非确定性活动：分支结构和排序

本条款表征了有关非确定性活动：分支结构和排序的全部定义。

8．1分支结构和排序的基本词汇

分支结构和排序的词典不需要基本关系。

8．2分支结构和排序的定义词汇

本条款中定义了以下关系：

——(mono—tree?sl?s27a)；

7a)；

——(order—tree?sl?s2

——(root—automorphic?occl?occ2)；

——(ordered?occ)：

——(nondet—ordered?occ)；

——(broken_ordered?occ)；

——(unordered?occ)。

每一个概念由非正式语义和一个KIF公理来描述。

10

GB／T20719．41—2010／ISo

8．3分支结构和排序所需的理论

本理论需要：

——act—OCC．th；

——complex．th；

——atomic．th：

——subactivity．th；

——occtree．th；

——psl—core．th。

8．4分支结构和排序所需的定义性扩展

分支结构和排序不需要定义性扩展。

8．5分支结构和排序的定义

对于为分支结构和排序定义以下概念。

8．5．1Mono_tree

生根于?sl的子树能被单一同态地嵌入到生根于?s2的子树中。

(forall(?sl?s27a)(iff(mono—tree?sl?s27a)

7S47s5)

(forall(?s3

(impldes(and(min_precedes?sl?s37a)

7s47a)

(min_preeedes?s2

(mono?s37a)