Chapter 7. Semantics

7.1. A Standard Model-Theoretic Semantics of Simple KerML Models

KerML's official semantics departs from the standard model-theoretic semantics for logic-based modeling languages (such as OWL and Alloy), as well as from formalizations of UML class models and ER models in the following way:

1. Since KerML allows features to have features, features cannot be interpreted (like classical properties or binary predicates) as binary relations over the universe U (or subsets of U × U).
2. Due to KerML's peculiar Feature Typing concept, the interpretation/extent of a classifier C includes the interpretations/extents of all features having C as their range, implying that classifiers can no longer be interpreted as subsets of U.
3. Since KerML allows features to have non-unique and ordered collections (multisets and sequences) as values, the interpretations of a KerML model also include a marking set and the set of all sequences formed with elements of U and of the marking set.

As a consequence, KerML's official semantics has lost much of the intuitive and philosophical appeal of standard model-theoretic semantics.

We present a standard model-theoretic semantics of a fragment of KerML, called Simple KerML Models, which do neither allow features to have features nor non-unique/ordered value collections.

For readability, we prefer using the terms object type instead of "structure", action type instead of "behavior", and action instead of "performance". We also call a structural feature a property, a data-valued property an attribute, and a behavioral feature an action step.

While the classical model-theoretic semantics of predicate logic does not make any ontological distinctions among the elements of the universe, the model-theoretic semantics of OWL partitions the universe into data values and objects, whereas the model-theoretic semantics of KerML partitions the universe into data values, objects and actions.

We define a Simple KerML model as a KerML model that only defines

1. data types, object types and action types as classifiers;
2. features for classifiers, but not for features;
3. features with plain value sets.

The following is an example of a Simple KerML model defining the action types BookRoom, CheckIn, Charge, CheckOut and RentHotelRoom, as well as the object types Room and Hotel, such that the action type RentHotelRoom has four action steps, the object type Room has one attribute and the object type Hotel has two attributes and one action step:

behavior BookRoom;
behavior CheckIn;
behavior Charge;
behavior CheckOut;
behavior RentHotelRoom {
  step bookRoom[1] : BookRoom;
  step checkIn[0..1] : CheckIn;
  step charge[1] : Charge;
  step checkOut[0..1] : CheckOut;
}
struct Room {
  feature roomNumber: Natural;
}
struct Hotel {
  feature name: String;
  feature rooms[1..*]: Room;
  step rentHotelRoom[*] : RentHotelRoom;
}

An action step (as an action-valued feature) defined for an object type, such as Hotel::rentHotelRoom, may express the fact that objects of that type can perform actions of the type defined for the step, such as hotels performing rentHotelRoom actions.

In the following section, we define a more concise mathematical representation of Simple KerML models as 11-tuples.

Simple KerML Models

A Simple KerML model defines a vocabulary consisting of the names of classifiers (data types, object types or action types) and classifier features, corresponding to the vocabulary of a predicate logical language consisting of names of constants, functions and predicates. Data literals correspond to constants, classifiers correspond to unary predicates, and classifier features correspond to unary functions (or binary predicates).

For Simple KerML models, we simplify the representation of the start and end times of occurrences by including two corresponding attributes in the definition of the predefined classifier Occurrence. In KerML, all occurrences have a startShot and an endShot, which are special zero-duration suboccurrences, whose occurrence time can be obtained by invoking the library function TimeOf. Consequently, the start time of an occurrence o is TimeOf( o.startShot ), and its end time is TimeOf( o.endShot ).

According to the KerML spec, all occurrences have an endShot, which raises the question, if KerML does not support ongoing occurrences with a moving time horizon?

A Simple KerML model, based on a set of predefined classifiers, is a 11-tuple

⟨ DT, OT, AT, Cl, ownF, feat, rng, mul, sup, CInv, GInv ⟩

specifying:

1. The pairwise disjoint finite sets of names of (predefined and user-defined) data types DT, object types OT and action types AT, which merged together form the set of classifier names Cl, such that, by definition, each of them contains the predefined name of a most general type/classifier: DataValue ∈ DT, Object ∈ OT, Action ∈ AT and { Occurrence, Anything } ⊆ Cl.
2. A function ownF for assigning a set of local names of its owned features to a classifier name C. The function feat is obtained by extending ownF such that subclassifiers inherit the (onwed and inherited) features of their superclassifiers. Full feature names have the form C::f where f ∈ feat(C).
3. A function rng for assigning a range (or co-domain) to any feature C::f with rng(C::f) ∈ Cl.
4. A function mul for assigning multiplicities to features.

5. A function sup for assigning direct superclassifiers to classifiers C ∈ Cl, such that

   1. Anything ∈ sup*(C), where sup* is the transitive closure of sup,
   2. if C ∈ DT, then sup(C) ⊆ DT and DataValue ∈ sup*(C),
   3. if C ∈ OT, then sup(C) ⊆ OT and { Object, Occurrence } ⊆ sup*(C),
   4. if C ∈ AT, then sup(C) ⊆ AT and { Action, Occurrence } ⊆ sup*(C),
   5. if C' ∈ sup(C), then feat(C') ⊆ feat(C).
6. A set of classifier invariants CInvar, which are ordered pairs of a classifier C and a logical formula F(x) with one free variable x, stating that F(i) holds for all instances i from the extent of C.
7. A set of global invariants GInvar, which are logical sentences (formulas without free variables).

Interpretations

While data values are ahistoric (they exist independently of time), all occurrences (objects and actions) have either been existing for some time in the past and possibly still exist, or exist at present. Occurrences remain in the history (of a modeled system) once they have ceased to "exist". Local universes of discourse (at certain points in time) include not only the present occurrences but all past occurrences as well; they increase as time progresses and new occurrences come into being (see also the discussion of constant versus varying domain semantics in [1]).

An interpretation of a Simple KerML model is an octuple

I = ⟨ ⟨Time, <⟩, ct, DV, Obj, Act, Occ, U, I_t ⟩

such that

1. ⟨Time, <⟩ is a linear order of time instants and ct ∈ Time is the current time. We write Time_ct for the set { t ∈ Time : t ≤ ct }.
2. DV is a time-independent (ahistoric) set of data values, which includes strings and numbers.
3. Obj: Time_ct → 2^Obj_ct and Act: Time_ct → 2^Act_ct are functions that assign finite sets of objects Obj_t and actions Act_t to any time instant t ≤ ct such that DV, Obj_t and Act_t are pairwise disjoint. These sets are expanding in time: for all t, t' ≤ ct, if t < t', then Obj_t ⊆ Obj_t' and Act_t ⊆ Act_t'.
4. Likewise, Occ: Time_ct → 2^Occ_ct and U: Time_ct → 2^U_ct are functions that assign a set of occurrences Occ_t and things U_t to any time instant t ≤ ct such that Occ_t = Obj_t ∪ Act_t and U_t = DV ∪ Occ_t.

5. I_t is a time-indexed interpretation function such that for all time instants t, t' ≤ ct:

   1. I_t(Anything) = U_t and I_t(Occurrence) = Occ_t.
   2. I_t(D) = I_t'(D) ⊆ DV for all D ∈ DT, and I_t(DataValue) = DV.
   3. I_t(O) ⊆ Obj_t for all O ∈ OT, and I_t(Object) = Obj_t.
   4. I_t(A) ⊆ Act_t for all A ∈ AT, and I_t(Action) = Act_t.

   5. A feature C::f with mul(C::f) = ⟨ l, u ⟩ and rng(C::f) = R is interpreted as a function I_t(C::f) : I_t(C) → 2^I_t(R) such that for any x ∈ I_t(C) and its feature value set val = I_t(C::f)(x), card(val) ≥ l and, if u≠ ∗, card(val) ≤ u, and

      1. if C is a data type, the feature interpretation function I_t(C::f) is ahistoric: I_t(C::f) = I_t'(C::f),
      2. the predefined occurrence type features startTime and endTime are interpreted according to their intended semantics: for any occurrence o, st = I_t(startTime)(o) ≤ ct and if o has an end time et = I_t(endTime)(o), then st ≤ et ≤ ct.
   6. The interpretation of classifiers respects their specialization hierarchy: for any classifier C ∈ Cl and any of its supertypes C' ∈ sup(C), I_t(C) ⊆ I_t(C').
   7. The interpretation satisfies all constraints of the model:
      1. for all classifier invariants ⟨C, F(x)⟩ ∈ CInvar, I ⊨ F(a) for all a ∈ C,
      2. for all global invariants S ∈ GInvar, I ⊨ S.

An interpretation I, together with a variable value assignment v : Var → U_ct for a finite set of variables Var, allows to interpret expressions. For instance, for expressions of the form x.f where x is an occurrence variable and f is a feature name:

I_t^v(x.f) = I_t(C::f)(v(x)) where v(x) ∈ C and f ∈ feat(C)

Whenever the range of a feature C::f is an occurrence type C', we can interpret expressions of the form x.f₁.f₂ where f₁ ∈ feat(C) and f₂ ∈ feat(C'), which are called path expressions. The resulting value set I_t^v(x.f₁.f₂) is obtained by merging the value sets I_t(C::f₂)(p) for all p ∈ I_t(C::f₁)(v(x)). In this way, we can interpret path expressions of any length greater than zero.

Satisfaction of Logical Formulas

Finally, we can define how a variable-assignment-enhanced interpretation I_t^v satisfies a logical formula F formed with atomic formulas that are composed with the help of the usual logical operators. The base case of atomic formulas includes the following three forms:

1. Classification atoms have the form C(x) where C is a classifier. They are satisfied by I_t^v if and only if v(x) ∈ I_t(C). Symbolically,

   I_t^v ⊨ C(x) iff v(x) ∈ I_t(C).

2. Comparison atoms have the form expr₁ # expr₂ where each expr_k is either a data literal (from one of the underlying data types), a variable, or a path expression, and # is one of the comparison predicates (=, ≠, <, ≤, >, ≥).

   I_t^v ⊨ expr₁ # expr₂ iff I_t^v(expr₁) I_t(#) I_t^v(expr₂),

   where I_t(#) is the interpretation of the comparison predicate #.

Complex logical formulas formed with the logical operators ¬, ∧, ∨, →, ∀, ∃ are satisfied by a variable-assignment-enhanced interpretation in the usual way.

When a logical sentence (variable-free formula) S is satisfied by an interpretation at a time instant t ∈ Time, we write I_t ⊨ S. When it is satisfied at all time instants t ≤ ct, we write I ⊨ S.

Entailment

A Simple KerML model M entails a logical sentence S if S is satisfied by all interpretations of M:

M ⊨ S iff I ⊨ S for all interpretations I of M.

Integrity Constraints

Integrity constraints, as elements of a KerML model, are logical sentences that have to be satisfied by the interpretations of the model. A KerML model may, for instance, define the following types of (integrity) constraints for a classifier:

Range Constraints

require that a feature must have a value from the value space of the type that has been defined as its range. For instance, a value of an attribute declared as feature age : Integer must be an integer. These (implicit) constraints are expressed in a model by specifying a range for the features concerned.

Mandatory Value Constraints

require that a feature must have a value. These constraints are expressed in a model with the help of a feature multiplicity that has a lower bound greater than 0. Notice that the default multiplicity of a feature is 1, implying that it is mandatory and single-valued.

Cardinality Constraints

apply to multi-valued features, only, and can require that the cardinality of a feature's value set is not less than a given minimum cardinality or not greater than a given maximum cardinality, as expressed by the feature's multiplicity.

In addition, there are further types of classifier constraints that only refer to a specific attribute and, therefore, could be expressed within the declaration of the attribute concerned:

Uniqueness Constraints (also called 'Key Constraints')

require that the value of an attribute C::a is unique among all instances of its domain: F(x) ≡ ∀y: C(y) → x.a ≠ y.a. Notice that this is different from declaring a feature to be unique, which requires its value collection to contain no duplicates.

Interval Constraints

require that the value of a numeric attribute a must be in a specific interval [min,max]: F(x) ≡ min ≤ x.a ∧ x.a ≤ max.

Pattern Constraints

require that a string attribute's value must match a certain pattern defined by a regular expression. They allow defining special string data types such as for URLs, email addresses or telephone numbers.

These classifier invariants could be expressed in the simplified way of an annotation appended to the attribute declaration. For instance, UML allows expressing uniqueness constraints with the help of the annotation (property modifier) keyword "key", while it also allows expressing standard identifier (or 'primary key') constraints with the help of the attribute annotation keyword "id" (implying that the attribute is unique and mandatory, and that its values are used as standard identifiers).

An interval constraint could be expressed with the attribute annotation keywords "min" and "max" together with corresponding numbers, while a pattern constraint could be expressed with the attribute annotation keyword "pattern" together with a regular expression.

References

[1] First-order temporal logics, a section of the article "Temporal Logic" by Valentin Goranko and Antje Rumberg, 2024, in Stanford Encyclopedia of Philosophy.