Semantics of the PROV Data Model

3.2.1 Entities

An entity is a kind of object that fixes some aspects of a thing. We assume:

3.2.2 Activities

An activity is an object corresponding to a continuing process rather than an evolving thing. We introduce:

3.2.3 Agents

An agent is an object that can act, by controlling, starting, ending, or participating in activities. An agent is something that bears some form of responsibility for an activity taking place, for the existence of an entity, or for another agent's activity. Agents can act on behalf of other agents. An agent may be a particular type of entity or activity; an agent cannot be both entity and activity because the sets of entities and activities are disjoint. We introduce:

3.2.4 Influences

We consider a set $Influences \subseteq Objects$ which has disjoint subsets $Events$ connecting entities and activities, $Associations$ between agents and activities, $Attributions$ between entities and agents, $Communications$ between pairs of activities, $Delegations$ between pairs of agents, and $Derivations$ that describe chains of generation and usage steps. These kinds of influences are discussed further below. Influences are disjoint from entities, activities and agents.

4.3.1 Entity

An entity formula is of the form $entity(id,attrs)$ where $id$ denotes an entity.

Entity formulas $entity(id,attrs)$ can be interpreted as follows:

 entity(x,[])
 entity(x,[a=5])
 entity(x,[a=4,a=5])
 entity(x,[a=4,b=6])

  entity(x,[a=4,a=5,b=6])

4.3.2 Activity

An activity formula is of the form $activity(id,st,et,attrs)$ where $id$ is a identifier referring to the activity, $st$ is a start time and $et$ is an end time, and $attrs$ are the attributes of activity $id$.

4.3.3 Agent

An agent formula is of the form $agent(id,attrs)$ where $id$ denotes the agent and $attrs$ describes additional attributes.

4.4.1 Generation

The generation formula is of the form $wasGeneratedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is a time.

4.4.2 Use

The use formula is of the form $used(id,a,e,t,attrs)$ where $id$ denotes an event, $a$ is an activity identifier, $e$ is an object identifier, $attrs$ is a set of attribute-value pairs, and $t$ is a time.

4.4.3 Invalidation

The invalidation formula is of the form $wasInvalidatedBy(id,e,a,t,attrs)$ where $id$ is an event identifier, $e$ is an entity identifier, $a$ is an activity identifier, $attrs$ is a set of attribute-value pairs, and $t$ is a time.

4.4.4 Association

An association formula has the form $wasAssociatedWith(id,a,ag,pl,attrs)$.

4.4.5 Start

A start formula $wasStartedBy(id,a_2,e,a_1,t,attrs)$ is interpreted as follows:

4.4.6 End

An activity end formula $wasEndedBy(id,a_2,e,a_1,t,attrs)$ is interpreted as follows:

4.4.7 Attribution

An attribution formula $wasAttributedTo(id,e,ag,attrs)$ is interpreted as follows:

4.4.8 Communication

A communication formula $wasInformedBy(id,a_2,a_2,attrs)$ is interpreted as follows:

4.4.9 Delegation

The $actedOnBehalfOf(id,ag_2,ag_1,act,attrs)$ relation is interpreted as follows:

4.4.10 Derivation

Derivation formulas can be of one of two forms:

• $wasDerivedFrom(id,e_2,e_1,a,g,u,attrs)$, which specifies an activity, generation and usage event. For convenience we call this a precise derivation.
• and $wasDerivedFrom(id,e_2,e_1,-,-,-,attrs)$, which does not specify an activity, generation and usage event. For convenience we call this an imprecise derivation.

4.4.11 Influence

4.4.12 Specialization

The $specializationOf(e_1,e_2)$ relation indicates when one entity formula presents more specific aspects of another.

4.4.13 Alternate

The $alternateOf$ relation indicates when two entity formulas present (possibly different) aspects of the same thing. The two entities may or may not overlap in time.

4.4.14 Membership

The $hadMember$ relation relates a collection to an element of the collection.

4.5.1 Precedes and Strictly Precedes

The precedes relation $x \precedes y$ holds between two events, one taking place before (or simultaneously with) another. Its meaning is defined in terms of the quasiordering on events specified by $\preceq$. The semantics of strictly precedes ($x \strictlyPrecedes y$) is similar, only $x$ must take place strictly before $y$. It is interpreted as $\prec$, which we recall is defined from $\preceq$ as $x \prec y \iff x \preceq y \text{ and } y \not\preceq x$.

entity(e)
activity(a1)
activity(a2)
wasGeneratedBy(gen1; e, a1, 2011-11-16T16:05:00)
wasGeneratedBy(gen2; e, a2, 2012-11-16T16:05:00) //different date

4.5.2 notNull

The $notNull(x)$ formula is used to specify that a value may not be the null value $\bot$. The symbol "$-$" always denotes the null value (i.e. $\rho(-) = \bot$).

4.5.3 typeOf

The typing formula $typeOf(x,t)$ constrains the type of the value of $x$.

5.2.1 Uniqueness constraints

5.2.2 Ordering constraints

5.2.3 Typing constraints

5.2.4 Impossibility constraints

6.2.1 Sets

The sets of structure $M(I)$ are:

In the definitions of $Entities$, $Collections$, $Activities$ and $Agents$ we use the notation $I \models typeOf(id,t)$ to indicate that $id$ must have type $t$ in $I$ according to the typing constraints. For example, for entities, this means that the set $Entities$ contains all identifiers $e,e'$ appearing in the $entity(e,attrs)$, $alternateOf(e,e')$, or $specializationOf(e,e')$ formulas, as well as all tose appearing in the appropriate positions of other formulas, as specified in the typing constraints.

In the definitions of $Activities$, $Generations$, $Invalidations$, and $Usages$ we write $a_{id}$, $g_{id}$, $i_{id}$ and $u_{id}$ respectively to indicate additional activities, generations and usages added for imprecise derivations or entities.

In addition, to define the set of $Things$, we introduce an equivalence relation on $Entities$ as follows:

The fact that this is an equivalence relation follows from the fact that $I$ is in normal form, since the constraints on $alternateOf$ ensure that it is an equivalence relation. Recall that given an equivalence relation $\equiv$ on some set $X$, the equivalence class of $x \in X$ is the set $[x]_\equiv = \{y \in X \mid x \equiv y\}$. The quotient of $X$ by an equivalence relation on $X$ is the set of equivalence classes, $X_\equiv = \{[x]_\equiv \mid x \in X\}$. Now we define the set of $Things$ as the quotient of $\equiv$-equivalence classes of $Entities$.

Observe that since $I$ is normalized and valid, entities and activities are disjoint, the influences are disjoint from entities, activities, and agents, and the different subsets of events and influences are pairwise disjoint, as required.

6.2.2 Functions

First, we consider the functions associated with $Entities$.

Above, we introduce a fresh attribute name $uniq$, not already in use in $I$, along with a fresh value $e$ and for each entity $e$ we add a value $uniq_e$ to $values(e,uniq)$. This construction ensures that if an entity is a specialization of another in $I$ then the specialization relationship will hold in $M(I)$. We also define the set of all events involved in $e$ as the set of events immediately involved in $e$ or any specialization of $e$. Similarly, the values of attributes of $e$ are those immediately declared for $e$ along with those of any $e'$ that $e$ specializes. We also introduce dummy generation and invalidation events for each entity $e$, along with activities $a_e,a'_e$ to perform them.

Similarly, for $Things$, we employ an auxiliary function $events:Things \to P(Events)$ that collects the set of all events in which one of the entities constituting the thing participated.

The functions $events$, $startTime$ and $endTime$ mapping activities to their start and end times are defined as follows:

The start and end times are arbitrary (say, some zero value) for activities with no $activity$ formula declaring the times. The above definitions of $startTime$ and $endTime$ ignore any start times asserted in $wasStartedBy$ or $wasEndedBy$ formulas. If both $activity$ and $wasStartedBy/wasEndedBy$ statements are present, then they must match, but PROV-CONSTRAINTS does not require that the times of multiple start or end events match for an activity with no $activity$ statement.

wasStartedBy(id1;a,e1,a1,t1,[])
wasStartedBy(id2;a,e2,a2,t2,[])

For other $Objects$ besides $Entities$ and $Activities$, the associated sets of $Events$ are defined to be empty. (An $Agent$ that happens to be an $Entity$ or $Activity$ will have the set of events defined above for the appropriate kind of object. Note that since $Entities$ and $Activities$ are disjoint, this definition is unambiguous.)

The function $time$ mapping $Events$ to their $Times$ is defined as follows:

This definition is deterministic because the sets of identifiers of different $Events$ are disjoint, and the associated times are unique.

The functions giving the interpretations of the different identified influences are as follows:

Note that since $I$ is normalized and valid, by the uniqueness constraints these functions are all well-defined. In the case for imprecise derivations, we generate additional activities, generations and usages linking $e_2$ to $e_1$.

The definition of the $influenced$ function is more involved, and is as follows:

This definition ensures that by construction $influenced(id)$ contains all of the other associated relationships. For any specific $id$, however, most of the above sets will be empty, and the final line will often be redundant. It is not always redundant, because it is possible to assert an unspecified influence in $I$.

It is straightforward to verify (by their definitions) that the event sets associated with entities and activities satisfy the side-conditions in Component 9.

Finally, the collection membership function $members$ is defined as follows:

6.2.3 Relations

We introduced a relation $\equiv$ corresponding to $alternateOf$ above, in defining $Things$, but this relation is not a component of the semantics.

The event ordering relation is defined as follows:

closed under reflexivity and transitivity. Here, we are using a slight abuse of notation: we write $G_I$ for the directed graph that is used during validation of $I$ to test for cycles among event ordering constraints. See Sec. 7.1 of PROV-CONSTRAINTS [PROV-CONSTRAINTS].

6.2.4 Axioms

To verify that the construction of $M(I)$ yields a PROV structure, we must ensure that all of the axioms and side-conditions in the components are satisfied. As noted above, the disjointness constraints are satisfied by construction.

For each axiom we give the corresponding justification:

1. Axiom 1 follows because $I$ is normalized with respect to Inference 6.
2. Axiom 2 follows from the construction, since we add dummy generation and invalidation events for every entity.
3. Axioms 3 and 4 follow because $I$ is normalized with respect to Inference 9 and 10 respectively.
4. Axiom 5 follows because $I$ is normalized with respect to Inference 12.
5. Axioms 6 and 7 follow because $I$ is normalized with respect to Inference 13 and 14 respectively.
6. Axioms 8 through 17 follow because $I$ is normalized with respect to Inference 15.
7. Axioms 18 through 21 follow because $I$ is normalized with respect to uniqueness constraints 24 through 27.
8. Axiom 22 follows because constraints 30, 31, 33, 34 ensure that a start event for an activity precedes any other start, end, usage or generation events involving that activity.
9. Axiom 23 follows because constraints 30, 32, 33, 34 ensure that an end event for an activity follows any other events involving that activity.
10. Axiom 24 follows because constraints 34, 36, 37, 39 ensure that a generation event for an entity precedes any other events involving that entity.
11. Axiom 25 follows because constraints 36, 38, 40, 43, 44 ensure that an invalidation event for an entity follows any other generation, usage, or invalidation events involving that entity.
12. Axiom 26 follows from constraint 41.
13. Axiom 27 follows from constraint 42 and from the fact that the event ordering constraint graph $G_I$ associated with a valid instance $I$ cannot have any cycles involving a strict precedence edge.
14. Axioms 28 through 31 follow from Constraint 47.
15. Axioms 32 and 33 follow from Constraint 48.
16. Axioms 34 and 35 follow from Constraint 49.
17. Axiom 36 follows from Constraint 50, part 19, and the semantics of $typeof$.

6.2.5 Main results

The main results of this section are that if a valid PROV instance $I$ has a model $M \models I$ that satisfies all of the inferences and constraints. Thus, a form of completeness holds: every valid PROV instance has a model.