ISO 18629-13:2006

INTERNATIONAL ISO
STANDARD 18629-13
First edition
2006-08-15
Industrial automation systems and
integration — Process specification
language —
Part 13:
Duration and ordering theories
Systèmes d'automatisation industrielle et intégration — Langage de
spécification de procédé —
Partie 13: Théories de classement et de durée

Reference number
©
ISO 2006
PDF disclaimer
This PDF file may contain embedded typefaces. In accordance with Adobe's licensing policy, this file may be printed or viewed but
shall not be edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing. In
downloading this file, parties accept therein the responsibility of not infringing Adobe's licensing policy. The ISO Central Secretariat
accepts no liability in this area.
Adobe is a trademark of Adobe Systems Incorporated.
Details of the software products used to create this PDF file can be found in the General Info relative to the file; the PDF-creation
parameters were optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In
the unlikely event that a problem relating to it is found, please inform the Central Secretariat at the address given below.

©  ISO 2006
All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means,
electronic or mechanical, including photocopying and microfilm, without permission in writing from either ISO at the address below or
ISO's member body in the country of the requester.
ISO copyright office
Case postale 56 • CH-1211 Geneva 20
Tel. + 41 22 749 01 11
Fax + 41 22 749 09 47
E-mail copyright@iso.org
Web www.iso.org
Published in Switzerland
ii © ISO 2006 – All rights reserved

ISO 18629-13 : 2006 (E)
Contents        Page
1 Scope . 1
2 Normative references . 1
3 Terms, definitions, and abbreviations . 2
3.1 Terms and definitions. 2
3.2 Abbreviations . 6
4 General information on ISO 18629 . 6
5 Organization of this part of ISO 18629 . 7
6 Subactivity occurrence ordering core Theory . 7
6.1 Primitive Relations of the Subactivity occurrence ordering theory. 8
6.2 Defined Relations of the Subactivity occurrence ordering theory. 8
6.3 Relationship to other sets of axioms. 8
6.4 Informal Semantics of the Subactivity occurrence ordering theory . 8
6.4.1 soo . 8
6.4.2 soo_precedes . 9
6.4.3 soomap. 9
6.5 Definitions in the Subactivity occurrence ordering theory. 9
6.5.1 Definition 1 (related to root_soo). 9
6.5.2 Definition 2 (related to leaf_soo) . 9
6.5.3 Definition 3 (related to next_soo). 10
6.6 Axioms of the Subactivity occurrence ordering theory. 10
6.6.1 Axiom 1.10
6.6.2 Axiom 2.10
6.6.3 Axiom 3.10
6.6.4 Axiom 4.11
6.6.5 Axiom 5.11
6.6.6 Axiom 6.11
6.6.7 Axiom 7.11
6.6.8 Axiom 8.12
7 Duration theory . 12
7.1 Primitive relations in the Duration theory . 12
7.2 Primitive Functions and Constants. 12
7.3 Defined Relations of the Duration theory . 12
7.4 Relationship to other sets of axioms. 13
7.5 Informal Semantics of the Duration theory . 13
7.5.1 timeduration. 13
7.5.2 lesser. 13
7.5.3 duration. 13
7.5.4 time_add .13
7.5.5 add . 14
7.5.6 mult. 14
7.5.7 zero . 14
7.5.8 one . 14
ISO 18629-13 : 2006 (E)
7.5.9 max+. 14
7.5.10 max-. 14
7.6 Definitions of Duration theory . 14
7.6.1 Definition 1.14
7.7 Axioms for the Duration theory . 15
7.7.1 Axiom 1.15
7.7.2 Axiom 2.15
7.7.3 Axiom 3.15
7.7.4 Axiom 4.16
7.7.5 Axiom 5.16
7.7.6 Axiom 6.16
7.7.7 Axiom 7.16
7.7.8 Axiom 8.16
7.7.9 Axiom 9.17
7.7.10 Axiom 10. 17
7.7.11 Axiom 11. 17
7.7.12 Axiom 12. 17
7.7.13 Axiom 13. 17
7.7.14 Axiom 14. 18
7.7.15 Axiom 15. 18
7.7.16 Axiom 16. 18
7.7.17 Axiom 17. 18
7.7.18 Axiom 18. 19
7.7.19 Axiom 19. 19
7.7.20 Axiom 20. 19
7.7.21 Axiom 21. 19
7.7.22 Axiom 22. 20
8 Occurrence tree automorphisms. 20
8.1 Primitive Relations in the Occurrence tree automorphism theory. 20
8.2 Defined Relations in the Occurrence tree automorphism theory. 20
8.3 Relationship to other sets of axioms. 21
8.4 Informal semantics of the Occurrence tree automorphism theory. 21
8.4.1 ubiquitous .21
8.4.2 end_iso. 21
8.4.3 legal_map . 21
8.4.4 tree_map .22
8.5 Definitions in the Occurrence tree automorphism theory . 22
8.5.1 Definition 1.22
8.5.2 Definition 2.22
8.5.3 Definition 3.23
8.6 Axioms for the Occurrence tree automorphism theory . 23
8.6.1 Axiom 1.23
8.6.2 Axiom 2.24
8.6.3 Axiom 3.24
iv              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
9 Activity envelope theory . 25
9.1 Primitive Relations in the Activity envelope theory . 25
9.2 Defined relation in Activity envelope theory . 25
9.3 Relationship to other sets of axioms. 25
9.4 Informal semantics of the Activity envelope theory . 25
9.4.1 envelope. 25
9.4.2 umbra. 26
9.5 Definitions in activity envelop theory . 26
9.6 Axioms of the Activity envelope theory . 26
9.6.1 Axiom 1.26
9.6.2 Axiom 2.26
9.6.3 Axiom 3.27
9.6.4 Axiom 4.27
9.6.5 Axiom 5.27
9.6.6 Axiom 6.27
9.6.7 Axiom 7.27
9.6.8 Axiom 8.28

Annex A (normative) Use of ASN.1 Identifiers in SC4 standards. 29
Annex B (informative) Example of process description using ISO 18629-13. 30

Bibliography. 38
Index. 39

Figures
Figure B1: TOP level process for manufacturing a GT350 [8]. 31
Figure B.2: PROCESS for manufacturing the 350–Engine [8]. 33
Figure B.3: PROCESS for manufacturing the 350–Block [8]. 34
Figure B.4: PROCESS for manufacturing the 350–Harness [8] . 35
Figure B.5: PROCESS for manufacturing the harness wire [8]. 36
Figure B.6 : Process for manufacturing the 350-Wire [8]. 36
ISO 18629-13 : 2006 (E)
Foreword
ISO (the International Organization for Standardization) is a worldwide federation of national
standards bodies (ISO member bodies). The work of preparing International Standards is normally
carried out through ISO technical committees. Each member body interested in a subject for which a
technical committee has been established has the right to be represented on that committee.
International organizations, governmental and non-governmental, in liaison with ISO, also take part in
the work. ISO collaborates closely with the International Electrotechnical Commission (IEC) on all
matters of electrotechnical standardization.

International Standards are drafted in accordance with the rules given in the ISO/IEC Directives,
Part 2.
The main task of technical committees is to prepare International Standards. Draft International
Standards adopted by the technical committees are circulated to the member bodies for voting.
Publication as an International Standard requires approval by at least 75 % of the member bodies
casting a vote.
Attention is drawn to the possibility that some of the elements of this part of ISO 18629 may be the
subject of patent rights. ISO shall not be held responsible for identifying any or all such patent rights.

ISO 18629-13 was prepared by Technical Committee ISO/TC 184, Industrial automation systems and
integration, Subcommittee SC 4, Industrial data.

A complete list of parts of ISO 18629 is available from the Internet:

http://www.tc184-sc4.org/titles
vi              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
Introduction
ISO 18629 is an International Standard for the computer-interpretable exchange of information related
to manufacturing processes. Taken together, all the parts contained in the ISO 18629 Standard provide
a generic language for describing a manufacturing process throughout the entire production process
within the same industrial company or across several industrial sectors or companies, independently
from any particular representation model. The nature of this language makes it suitable for sharing
process information related to manufacturing during all the stages of a production process.

This part of ISO 18629 provides a description of the core elements of the language defined within ISO
18629.
All parts of ISO 18629 are independent of any specific process representation or model proposed in a
software application in the domain of manufacturing management. Collectively, they provide a
structural framework for improving the interoperability of these applications.

INTERNATIONAL STANDARD        ISO 18629-13: 2006 (E)

Industrial automation systems and integration — Process
specification language —
Part 13:
Duration and ordering theories

1 Scope
This part of ISO 18629 provides a representation of the primitive concepts related to ordering and
durations constraints for activities.

The following is within the scope of this part of ISO 18629:

⎯ subactivity occurrence orderings;
⎯ duration;
⎯ iterated occurrence orderings;
⎯ occurrence tree endomorphisms;
⎯ activity envelopes.
2 Normative references
The following referenced documents are indispensable for the application of this document. For dated
references, only the edition cited applies. For undated references, the latest edition of the referenced
document (including any amendments) applies.

ISO/IEC 8824-1: Information technology — Abstract Syntax Notation One (ASN.1) — Part 1:
Specification of basic notation.

ISO 15531-1: Industrial automation systems and integration — Industrial manufacturing management
data — Part 1: General overview.

ISO 18629-1: Industrial automation systems and integration — Process specification language —
Part 1: Overview and basic principles.

ISO 18629-11: 2005, Industrial automation systems and integration — Process specification language
— Part 11: PSL-core.
ISO 18629-13 : 2006 (E)
ISO 18629-12: Industrial automation systems and integration — Process specification language —
Part 12: Outer core.
3 Terms, definitions, and abbreviations

3.1 Terms and definitions
For the purposes of this document, the following terms and definitions apply:

3.1.1
automorphism
one-to-one mapping of elements on a set that preserves the relations and functions in some model
3.1.2
axiom
well-formed formula in a formal language that provides constraints on the interpretation of symbols in
the lexicon of a language
[ISO 18629-1]
3.1.3
commutative group
algebraic structure with an internal binary operation (OP) with respect to which : a OP b = b OP a

3.1.4
conservative definition
definition that specifies necessary and sufficient conditions that a term shall satisfy and that does not
allow new inferences to be drawn from the theory
[ISO 18629-1]
3.1.5
core theory
set of axioms for relation and function symbols that denote primitive concepts
[ISO 18629-1]
3.1.6
defined lexicon
set of symbols in the non-logical lexicon which denote defined concepts
NOTE Defined lexicon is divided into constant, function and relation symbols.
EXAMPLE  terms with conservative definitions.
[ISO 18629-1]
2              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
3.1.7
endomorphism
mapping from a set onto a subset that preserves the relations and functions in some model

3.1.8
extension
augmentation of PSL-Core containing additional axioms
NOTE 1  The PSL-Core is a relatively simple set of axioms that is adequate for expressing a wide range of basic
processes. However, more complex processes require expressive resources that exceed those of the PSL-Core.
Rather than clutter the PSL-Core itself with every conceivable concept that might prove useful in describing one
process or another, a variety of separate, modular extensions need to be developed and added to the PSL-Core as
necessary. In this way a user can tailor the language precisely to suit his or her expressive needs.
NOTE 2  All extensions are core theories or definitional extensions.
[ISO 18629-1]
3.1.9
grammar
specification of how logical symbols and lexical terms can be combined to make well-formed
formulae
[ISO 18629-1]
3.1.10
homomorphism
mapping between sets that preserves some relation on the elements of the set

3.1.11
interpretation
universe of discourse and assignment of truth values (TRUE or FALSE) to all sentences in a theory

NOTE  See annex B for an example of an interpretation.
[ISO 18629-11]
3.1.12
language
combination of a lexicon and a grammar
[ISO 18629-1]
3.1.13
lexicon
set of symbols and terms
ISO 18629-13 : 2006 (E)
NOTE The lexicon consists of logical symbols (such as Boolean connectives and quantifiers) and non-logical
symbols. For ISO 18629, the non logical part of the lexicon consists of expressions (constants, function symbols,
and relation symbols) chosen to represent the basic concepts of the ontology.
[ISO 18629-1]
3.1.14
model
combination of a set of elements and a truth assignment that satisfies all well-formed formulae in a
theory
NOTE 1 The word "model" is used, in logic, in a way that differs from the way it is used in most scientific and
everyday contexts: if a sentence is true in a certain interpretation, it is possible to say that the interpretation is a
model of the sentence. The kind of semantics presented here is often called model-theoretical semantics.
NOTE 2  A model is typically represented as a set with some additional structure (partial ordering, lattice, or
vector space). The model then defines meanings for the terminology and a notion of truth for sentences of the
language in terms of this model. Given a model, the underlying set of axioms of the mathematical structures used
in the set of axioms then becomes available as a basis for reasoning about the concepts intended by the terms of
the language and their logical relationships, so that the set of models constitutes the formal semantics of the
ontology.
[ISO 18629-1]
3.1.15
monomorphism
one to one mapping that preserves some relation on the elements of the set

3.1.16
ontology
lexicon of specialised terminology along with some specification of the meaning of terms in the
lexicon
NOTE 1: structured set of related terms given with a specification of the meaning of the terms in a formal
language. The specification of meaning explains why and how the terms are related and conditions how the set
is partitioned and structured.
NOTE 2:  The primary component of a process specification language such as ISO 18629 is an ontology. The
primitive concepts in the ontology according to ISO 18629 are adequate for describing basic manufacturing,
engineering, and business processes.

NOTE 3:  The focus of an ontology is not only on terms, but also on their meaning. An arbitrary set of terms is
included in the ontology, but these terms can only be shared if there is an agreement about their meaning. It is
the intended semantics of the terms that is being shared, not simply the terms.
NOTE 4:  Any term used without an explicit definition is a possible source of ambiguity and confusion. The
challenge for an ontology is that a framework is needed for making explicit the meaning of the terms within it.
For the ISO 18629 ontology, it is necessary to provide a rigorous mathematical characterisation of process
information as well as a precise expression of the basic logical properties of that information in the ISO 18629
language.
[ISO 18629-1]
4              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
3.1.17
Outer Core
set of core theories that are extensions of PSL-Core and that are so generic and pervasive in their
applicability that they have been put apart
NOTE  In practice, extensions incorporate the axioms of the Outer Core.
[ISO 18629-1]
3.1.18
primitive concept
lexical term that has no conservative definition
[ISO 18629-1]
3.1.19
primitive lexicon
set of symbols in the non-logical lexicon which denote primitive concepts
NOTE Primitive lexicon is divided into constant, function and relation symbols.
[ISO 18629-1]
3.1.20
process
structured set of activities involving various enterprise entities, that is designed and organised for a
given purpose
NOTE The definition provided here is very close to that given in ISO 10303-49. Nevertheless ISO 15531 needs
the notion of structured set of activities, without any predefined reference to the time or steps. In addition, from
the point of view of flow management, some empty processes may be needed for a synchronisation purpose
although they are not actually doing anything (ghost task).

[ISO 15531-1]
3.1.21
proof theory
set of theories and lexical elements necessary for the interpretation of the semantics of the language
NOTE  It consists of three components: the PSL-Core, the Outer Core and the extensions.
[ISO 18629-1]
3.1.22
PSL-Core
set of axioms for the concepts of activity, activity-occurrence, time-point, and object
ISO 18629-13 : 2006 (E)
NOTE  The motivation for PSL-Core is any two process-related applications shall share these axioms in
order to exchange process information, and hence is adequate for describing the fundamental concepts of
manufacturing processes. Consequently, this characterisation of basic processes makes few assumptions about
their nature beyond what is needed for describing those processes, and the PSL-Core is therefore rather weak in
terms of logical expressiveness. In particular, PSL-Core is not strong enough to provide definitions of the many
auxiliary notions that become necessary to describe all intuitions about manufacturing processes.
[ISO 18629-1]
3.1.23
theory
set of axioms and definitions that pertain to a given concept or set of concepts

NOTE this definition reflects the approach of artificial intelligence in which a theory is the set of assumptions on
which the meaning of the related concept is based.
[ISO 18629-1]
3.1.24
universe of discourse
the collection of concrete or abstract things that belong to an area of the real world, selected according
to its interest for the system to be modelled and for its corresponding environment

[ISO 15531-1]
3.2 Abbreviations
For the purpose of this part of ISO 18629, the following abbreviations apply:

⎯ FOL First-Order Logic:
⎯ BNF Backus-Naur form;
⎯ KIF Knowledge Interchange Format;
⎯ PSL Process Specification Language.

4 General information on ISO 18629

As stated in ISO 18629-1, ISO 18629 as a whole specifies a language for the representation of process
information, which is a process specification language named PSL. It is composed of a lexicon, an
ontology, and a grammar for process descriptions that are distributed in part 11 to 19 and part 41 to 49
of ISO 18629 .
Certain parts are under development
6              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
NOTE 1 PSL is a language for specifying manufacturing processes based on a mathematically well defined
vocabulary and grammar. As such, it is different from other languages such as EXPRESS (defined in ISO 10303-
11) and used for example in ISO 10303-41, ISO 10303-42, ISO 10303-49, ISO 13584, ISO 15531 and ISO
15926, that are modelling languages. In the context of an exchange of information between two processes, PSL
specifies each process independently of its behaviour. For example, an object viewed as a resource within one
process can be recognised as the same object even though it is viewed as a product within a second process. PSL
is based on Mathematical Set Theory and Situation Calculus (see ISO 18629-11: 2005, Annex D).
Part 11 to 19 of ISO 18629 specify core theories needed to give precise definitions and the
corresponding axioms of the primitive concepts of ISO 18629, thus enabling precise semantic
translations between different schemes.

According to that parts 11 to 19 of ISO 18629 provide:

⎯ the representation of the basic elements of the language;
⎯ standardized sets of axioms that correspond to intuitive semantic primitive concepts adequate to
describe basic processes;
⎯ the set of rules to develop, in compliance with PSL-Core, other core theories or extensions such as
the extensions that are provided in parts 41 to 49.

5 Organization of this part of ISO 18629

This clause specifies the fundamental theories from which this part of ISO 18629 is composed.

The core theories that constitute this part of ISO 18629 are:

⎯ Subactivity occurrence ordering theory (soo.th);
⎯ Duration theory (duration.th);
⎯ Occurrence tree automorphism theory (preserve.th);
⎯ Activity envelope theory (envelope.th);

All theories in this part of ISO 18629 are extensions of theories found within ISO 18629-12

6 Subactivity occurrence ordering core Theory

The Subactivity occurrence ordering theory introduces the concepts necessary to represent intuitions
about process flow and partial orderings over the subactivity occurrences within a complex activity.

ISO 18629-13 : 2006 (E)
6.1 Primitive Relations of the Subactivity occurrence ordering theory
The nonlogical lexicon of the Subactivity occurrence ordering theory contains two primitive relation
symbols:
⎯ soo;
⎯ soo_precedes.
The nonlogical lexicon of the Subactivity occurrence ordering theory contains one primitive function
symbol:
⎯ soomap.
6.2 Defined Relations of the Subactivity occurrence ordering theory
The nonlogical lexicon of the Subactivity Theory contains the following defined relation symbols:
⎯ root_soo;
⎯ leaf_soo;
⎯ next_subactivity.
6.3 Relationship to other sets of axioms
The Subactivity occurrence ordering theory requires the following core theories
⎯ psl_core.th;
⎯ occtree.th;
⎯ atomic.th;
⎯ complex.th;
⎯ actocc.th.
No definitional extensions are required by the Subactivity occurrence ordering theory.

6.4 Informal Semantics of the Subactivity occurrence ordering theory
6.4.1 soo
KIF notation for soo:
(soo ?s ?a)
Informal semantics for soo:
8              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
(soo ?s ?a) is TRUE in an interpretation of Subactivity occurrence ordering theory if and only if the
activity occurrence ?s is an element of the Subactivity occurrence ordering for activity ?a.
6.4.2 soo_precedes
KIF notation for primitive:
(soo_precedes ?s1 ?s2 ?a)
Informal semantics for soo_precedes:

(soo_precedes ?s1 ?s2 ?a) is TRUE in an interpretation of Subactivity occurrence ordering theory if
and only if the activity occurrence ?s1 precedes activity occurrence ?s2 in the subactivity occurrence
ordering for the activity ?a. This relation defines a partial ordering over the subactivity occurrences of
a complex activity.
6.4.3 soomap
KIF notation for soomap:
(soomap ?s)
Informal semantics for soomap:

(= ?s1 (soomap ?s)) is TRUE in an interpretation of Subactivity occurrence ordering theory if and only
if the activity occurrence ?s1 is the element of the subactivity occurrence ordering that corresponds to
?s.
6.5 Definitions in the Subactivity occurrence ordering theory
6.5.1 Definition 1 (related to root_soo)
An activity occurrence is a root of a subactivity occurrence ordering for an activity ?a if and only if it
is an element of the ordering and there does not exist an activity occurrence that precedes it in the
ordering.
(forall (?s ?a) (iff (root_soo ?s ?a)
(and (soo ?s ?a)
(not (exists (?s1)
(soo_precedes ?s1 ?s ?a)))))
6.5.2 Definition 2 (related to leaf_soo)
An activity occurrence is a leaf of a subactivity occurrence ordering for an activity ?a if and only if it
is an element of the ordering and there does not exist an activity occurrence that follows it in the
ordering
ISO 18629-13 : 2006 (E)
(forall (?s ?a) (iff (leaf_soo ?s ?a)
(and (soo ?s ?a)
(not (exists (?s1)
(soo_precedes ?s ?s1 ?a)))))
6.5.3 Definition 3 (related to next_soo)
An activity occurrence ?s2 is the next subactivity occurrence after ?s1 in a subactivity occurrence
ordering for ?a if and only if ?s1 precedes ?s2 in the ordering and there does not exist a subactivity
occurrence that is between them in the ordering.

(forall (?s1 ?s2 ?a) (iff (next_soo ?s1 ?s2 ?a)
(and  (soo_precedes ?s1 ?s2 ?a)
(not (exists (?s3)
(and  (soo_precedes ?s1 ?s3 ?a)
(soo_precedes ?s3 ?s2 ?a)))))))

6.6 Axioms of the Subactivity occurrence ordering theory
6.6.1 Axiom 1
The soo_precedes relation orders elements of the subactivity occurrence ordering.

(forall (?s1 ?s2 ?a)
(implies (soo_precedes ?s1 ?s2 ?a)
(and (soo ?s1 ?a)
(soo ?s2 ?a))))
6.6.2 Axiom 2
Elements of the subactivity occurrence ordering are elements of the activity tree.

(forall (?a ?s)
(implies (soo ?s ?a)
(or (root ?s ?a)
(exists (?s1)
(min_precedes ?s1 ?s ?a)))))
6.6.3 Axiom 3
The function soomap maps the activity tree to the subactivity occurrence ordering.

10              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
(forall (?s ?a)
(soo (soomap ?s) ?a))
6.6.4 Axiom 4
The elements of the subactivity occurrence ordering are fixed by soomap.

(forall (?s ?a)
(implies (soo ?s ?a)
(= ?s (soomap ?s))))
6.6.5 Axiom 5
The function soomap is a branch monomorphism.

(forall (?s ?a)
(or (mono (?s (soomap ?s) ?a)
(= ?s (soomap ?s))))
6.6.6 Axiom 6
The activity tree is order-homomorphic to the subactivity occurrence ordering.

(forall (?a ?s1 ?s2)
(implies (min_precedes ?s1 ?s2 ?a)
(iff (soo_precedes (soomap ?s1) (soomap ?s2) ?a)
(not (exists (?s3 ?s4)
(and (min_precedes ?s4 ?s3 ?a)
(= (soomap ?s3) (soomap ?s1))
(= (soomap ?s4) (soomap ?s2))))))))
6.6.7 Axiom 7
soo_precedes is not symmetric.

(forall (?a ?s1 ?s2)
(implies (soo_precedes ?s1 ?s2 ?a)
(not (soo_precedes ?s2 ?s1 ?a))))
ISO 18629-13 : 2006 (E)
6.6.8 Axiom 8
soo_precedes is transitive.
(forall (?a ?s1 ?s2 ?s3)
(implies (and (soo_precedes ?s1 ?s2 ?a)
(soo_precedes ?s2 ?s3 ?a))
(soo_precedes ?s1 ?s3 ?a)))
7 Duration theory
The Duration theory introduces the concept of duration. It adds a metric to the timeline by mapping
every pair of points to a new subclass of objects called timeduration that satisfy the axioms of vector
spaces.
7.1 Primitive relations in the Duration theory
The nonlogical lexicon of the Duration theory contains two primitive relation symbols:
— timeduration;
— lesser.
7.2 Primitive Functions and Constants
The nonlogical lexicon of the Duration theory contains three function symbols:;
— duration;
— add;
— mult.
The nonlogical lexicon of the Duration theory contains four constant symbols:
— zero;
— one;
— max+;
— max-.
7.3 Defined Relations of the Duration theory
The nonlogical lexicon of the Duration theory contains one defined relation symbol:
⎯ time_add.
12              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
7.4 Relationship to other sets of axioms
The Duration theory requires :
⎯ psl_core.th.
No definitional extensions are required by the Duration theory.

7.5 Informal Semantics of the Duration theory
7.5.1 timeduration
KIF notation for timeduration :
(timeduration ?d)
Informal semantics for timeduration :

(timeduration ?d) is TRUE in an interpretation of the Duration theory if and only if ?f is a member of
the set of timedurations in the universe of discourse of the interpretation. Timedurations are a
subcategory of object.
7.5.2 lesser
KIF notation for lesser :
(lesser ?d1 ?d2)
Informal semantics for lesser:

All timedurations are linearly ordered.
(lesser ?d1 ?d2) is TRUE in an interpretation of the Duration theory if and only if the value of the
timeduration ?d1 is less that the value of the timeduration ?d2.
7.5.3 duration
KIF notation for duration:
(duration ?t1 ?t2)
Informal semantics for duration:

(= (duration ?t1 ?t2) ?d) is TRUE in an interpretation of the Duration theory if and only if ?d denotes
the timeduration whose value is the distance between the timepoints ?t1 and ?t2 on the timeline.
7.5.4 time_add
KIF notation for time_add :
(time_add ?t ?d)
ISO 18629-13 : 2006 (E)
Informal semantics for time_add:

(= (time_add ?t ?d) ?t2) is TRUE in an interpretation of the Duration theory if and only if ?t2 denotes
the timepoint which is distance ?d from the timepoints ?t on the timeline.
7.5.5 add
KIF notation for add :
(add ?d1 ?d2)
Informal semantics for add:
(= (add ?d1 ?d2) ?d3) is TRUE in an interpretation of the Duration theory if and only if ?d3 denotes
the timeduration whose value is sum of the values of the timedurations ?d1 and ?d2.
7.5.6 mult
KIF notation for mult :
(mult ?x ?d)
Informal semantics for mult:
(= (mult ?x ?d) ?d2) is TRUE in an interpretation of the Duration theory if and only if ?d2 denotes
the timeduration whose value is product of the value of the timedurations ?d and ?x, where ?x is an
element of a commutative group.
7.5.7 zero
Informal semantics for zero:
zero denotes the timeduration constant that is the additive identity for the add function.
7.5.8 one
Informal semantics for one:
one denotes the constant that is the multiplicative identity for the mult function.
7.5.9 max+
Informal semantics for max+:
max+ is the maximum timeduration.
7.5.10 max-
Informal semantics for max-:
max- is the minimum timeduration.

7.6 Definitions of Duration theory
7.6.1 Definition 1
The time_add function maps a timepoint ?t1 and a timeduration ?d to the timepoint ?t2 such that the
duration between ?t1 and ?t2 is ?d.

14              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
(forall (?t1 ?t2 ?d)
(iff (= ?t2 (time_add ?t1 ?d))
(and (timepoint ?t1)
(timepoint ?t2)
(timeduration ?d)
(= ?d (duration ?t2 ?t1)))))
7.7 Axioms for the Duration theory
The set of axioms in the Duration theory is as follows:
7.7.1 Axiom 1
zero, max+, and max- are all timedurations.

(and (timeduration zero)
(timeduration max+)
(timeduration max-))
7.7.2 Axiom 2
The result of adding two timedurations is a timeduration.

(forall (?d1 ?d2)
(implies (and (timeduration ?d1)
(timeduration ?d2))
(timeduration (add ?d1 ?d2))))
7.7.3 Axiom 3
The add function is associative.

(forall (?d1 ?d2 ?d3)
(implies (and (timeduration ?d1)
(timeduration ?d2)
(timeduration ?d3))
(= (add (add ?d1 ?d2) ?d3) (add ?d1 (add ?d2 ?d3))))
ISO 18629-13 : 2006 (E)
7.7.4 Axiom 4
zero is the additive identity.

(forall (?d)
(implies (timeduration ?d)
(= (add ?d zero) ?d)))
7.7.5 Axiom 5
The opposite of a timeduration is a timeduration.

(forall (?d1)
(implies (timeduration ?d1)
(exists (?d2)
(and (timeduration ?d2)
(= (add ?d1 ?d2) zero))))
7.7.6 Axiom 6
The add function is commutative.

(forall (?d1 ?d2)
(implies (and (timeduration ?d1)
(timeduration ?d2))
(= (add ?d1 ?d2) (add ?d2 ?d1))))
7.7.7 Axiom 7
The result of multiplying a timeduration by a scalar value is a timeduration.

(forall (?d ?r)
(implies (timeduration ?d)
(timeduration (mult ?r ?d))))
7.7.8 Axiom 8
Timedurations can be multiplied by scalars:

(forall (?d1 ?d2 ?r)
(= (mult ?r (add ?d1 ?d2)) (add (mult ?r ?d1) (mult ?r ?d2))))
16              © ISO 2006 All rights reserved

ISO 18629-13 : 2006 (E)
7.7.9 Axiom 9
Multiplication of timedurations by scalars is distributive:

(forall (?d ?r ?s)
...