--- a/model/working-copy/wd5-prov-dm-constraints-revised.html Sun Apr 15 14:27:49 2012 +0100
+++ b/model/working-copy/wd5-prov-dm-constraints-revised.html Mon Apr 16 00:48:00 2012 +0100
@@ -225,6 +225,7 @@
specification [[PROV-DM]] that defines a data model for
provenance on the Web. </p>
+<!-- Commented out since seems redundant -- jcheney
<div class="note"> Revise list to match SOTD. Seems redundant.
</div>
<p>This specification is one of several specifications, referred to as the PROV family of specifications, defining the various aspects
@@ -247,7 +248,7 @@
<div class="note">
Revise this section to match the revised document structure.
</div>
-
+-->
<!--
<p>PROV-DM is essentially defined without any constraints
@@ -303,30 +304,41 @@
PROV-DM data by specifying <em>constraints</em> that valid PROV-DM data must
satisfy. Applications SHOULD produce valid provenance and
MAY reject provenance that is not valid in order to increase
-the usefulness of provenance.</p>
+the usefulness of provenance and reliability of applications that
+process it.</p>
<p> This specification lists inferences and definitions together in one
-section (<a href="#inferences" class="sectionRef"></a>), and then
+section (<a href="#inferences" class="sectionRef"></a>), defines the
+induced notion of <a>equivalence</a> (<a href="#equivalence"
+class="sectionRef"></a>), and then
considers two kinds of validity constraints (<a href="#constraints"
class="sectionRef"></a>): <em>structural constraints</em> that
prescribe properties of PROV-DM instances that can be checked directly
by inspecting the syntax, and <em>event ordering</em> constraints that
require that the records in a PROV-DM instance are consistent with a
sensible ordering of events relating the activities, entities and
-actors involved. In separate sections we consider additional
+agents involved. In separate sections we consider additional
constraints specific to collections and accounts (<a
href="#collection-constraints" class="sectionRef"></a> and <a
href="#account-constraints" class="sectionRef"></a>). </p>
<p>
-The specification also describes how the inferences, definitions, and constraints should be used (<a href="#compliance" class="sectionRef"></a>). Briefly, a PROV-DM compliant application is allowed (but not required) to treat two PROV-DM instances as the same if they are equal after applying the inference rules and possibly reordering expressions, and we can define a canonical form for PROV-DM instances obtained by applying all possible inference rules. In addition, a validating PROV-DM application is required to check that the constraints are satisfied in (the canonical form of) provenance data generated or consumed by the application.
+The specification also describes how the inferences, definitions, and
+constraints should be used (<a href="#compliance"
+class="sectionRef"></a>). Briefly, a PROV-DM compliant application is
+allowed (but not required) to treat two PROV-DM instances as the same
+if they are equal after applying the inference rules and possibly
+reordering expressions, and we can define a canonical form for PROV-DM
+instances obtained by applying all possible inference rules. In
+addition, a validating PROV-DM application is required to check that
+the constraints are satisfied in (the normal form of) provenance data generated or consumed by the application.
</p>
<p>
Finally, the specification includes a section (<a
href="#rationale" class="sectionRef"></a>) describing the rationale
for the inferences and constraints in greater detail, particularly
-background on events, attributes, the the role of inference, and
+background on events, attributes, the role of inference, and
accounts. A formal mathematical model that further justifies the
constraints and inferences is found in [[PROV-SEM]].
</p>
@@ -359,14 +371,54 @@
<p>
In this section we describe <a title="inference">inferences</a> and <a title="definition">definitions</a> that MAY be used on
- provenance data.
+ provenance data, and a notion of <a
+title="equivalence">equivalence</a> on PROV-DM instances.
An <dfn id="inference">inference</dfn> is a rule that can be applied
to PROV-DM to add new provenance expressions. A <dfn
id="definition">definition</dfn> is a rule that states that a
provenance expression is equivalent to some other expressions; thus,
- defined provenance expressions can be replaced by their definitions.
+ defined provenance expressions can be replaced by their definitions,
+and vice versa.
</p>
+<p> Inferences have the following general form:
+<div class='inference' id='inference-example'>
+ <span class='conditional'>IF</span> hyp_1 and ... and
+hyp_k <span class='conditional\'>THEN</span> there exists a_1,..., a_m such that conclusion_1 ... conclusion_n.
+ </div>
+
+ This means that if provenance expressions matching hyp_1... hyp_k
+ can be found in a PROV-DM instance, we can add the expressions
+ concl_1 ... concl_n to the instance, possibly after generating fresh
+ identifiers a_1,...,a_m for unknown objects. These fresh
+ identifiers might later be found to be equal to known identifiers;
+ they play a similar role in PROV-DM to existential variables in logic.
+</p>
+<div class='note'>
+ TODO: Is this re-inventing blank nodes in PROV-DM, and do we want to
+ do this? A lot of the inferences have existentially quantified
+ conclusions (and there is some theory that supports this).
+ </div>
+
+<p> Definitions have the following general form:
+<div class='definition' id='definition-example'>
+ defined_exp holds <span class='conditional\'>IF AND ONLY IF </span>
+ there exists a_1,..., a_m such that defining_exp_1 ... defining_exp_n.
+ </div>
+
+ This means that a provenance expression defined_exp is defined in
+ terms of other expressions. This can be viewed as a two-way
+ inference: If defined_exp
+ can be found in a PROV-DM instance, we can add the expressions
+defining_exp_1 ... defining_exp_n to the instance, possibly after generating fresh
+ identifiers a_1,...,a_m for unknown objects. Conversely, if there
+ exist identifiers a_1...a_m such that defining_exp_1
+ ... defining_exp_n hold in the instance, we can add the defined
+ expression def_exp. When an expression is defined in terms of
+ others, it is in a sense redundant; it is safe to replace it with
+ its definition.
+</p>
+
<p>Applications that process provenance MAY use these definitions or
inferences. Moreover, they SHOULD apply all applicable inferences
before determining whether an instance of PROV-DM is <a
@@ -376,6 +428,8 @@
application.
</p>
+
+
<section>
<h3>Component 1: Entities and Activities</h3>
@@ -384,7 +438,7 @@
as the existence of an underlying entity generated by one activity and used by the
other.</p>
-<div class='definition' id='wasInformedBy-communication'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
+<div class='definition' id='wasInformedBy-definition'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasInformedBy(a2,a1)</span>
holds <span class='conditional'>if and only if</span>
there is an entity with some identifier <span class="name">e</span> and some sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
@@ -395,14 +449,13 @@
<p>Start of <span class="name">a2</span> by activity <span
class="name">a1</span> is <a title="definition">defined</a> as follows.</p>
-<div class='definition' id='wasStartedBy'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
+<div class='definition' id='wasStartedBy-definition'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
<span class="name">wasStartedBy(a2,a1)</span>
holds <span class='conditional'>if and only if</span>
- there exist an entity with some identifier <span class="name">e</span>
-and some attributes <span class="name">gAttr</span> and <span class="name">sAttr</span>,
+ there exists an entity <span class="name">e</span>
such that
- <span class="name">wasGeneratedBy(-,e,a1,-,gAttr)</span>
- and <span class="name">wasStartedBy(-,a2,e,-,sAttr)</span> hold.
+ <span class="name">wasGeneratedBy(-,e,a1,-,-)</span>
+ and <span class="name">wasStartedBy(-,a2,e,-,-)</span> hold.
</div>
@@ -424,13 +477,15 @@
<span class="name">e</span> and <span class="name">ag</span>,
<span class='conditional'>then</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
<pre>
-activity(a, t1, t2, attr1)
+activity(a, -, -,-)
wasGeneratedBy(-,e, a, -)
-wasAssociatedWith(-,a, ag, -, attr2)
+wasAssociatedWith(-,a, ag, -, -)
</pre>
-for some sets of attribute-value pairs <span class="name">attr1</span>
- and <span class="name">attr2</span>, and times <span class="name">t1</span> and <span class="name">t2</span>.
</div>
+
+<div class="note">
+ There should probably be some inferences about responsibility/actedOnBehalfOf.
+ </div>
</section>
<section>
@@ -439,18 +494,16 @@
<h4>Derivation</h4>
<p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
<div class='inference' id='derivation-use'>
-<p>Given an activity <span class="name">a</span>, entities denoted by <span class="name">e1</span> and <span class="name">e2</span>, and sets of attribute-value
-pairs <span class="name">dAttrs</span>, <span class="name">gAttrs</span>,
-<span class='conditional'>if</span> <span class="name">wasDerivedFrom(e2,e1, a, dAttrs)</span> and <span class="name">wasGeneratedBy(e2,a,-,gAttrs)</span> hold, <span
-class='conditional'>then</span> <span class="name">used(a,e1,-,uAttrs)</span> also holds
-for some set of attribute-value pairs <span class="name">uAttrs</span>.
+<p>Given an activity <span class="name">a</span>, entities denoted by <span class="name">e1</span> and <span class="name">e2</span>,
+<span class='conditional'>if</span> <span class="name">wasDerivedFrom(-,e2,e1, a, -)</span> and <span class="name">wasGeneratedBy(-,e2,a,-,-)</span> hold, <span
+class='conditional'>then</span> <span class="name">used(-,a,e1,-,-)</span> also holds.
</div>
<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity in a given account
(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
</p>
-<p>We note that the converse inference, does not hold.
+<p>The converse inference does not hold.
From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
derive <span class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span class="name">e1</span> may occur in usages performed by many activities, which may have not generated the entity denoted by <span class="name">e2</span>.</p>
@@ -463,22 +516,19 @@
<div class='inference' id='wasRevision'>
Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities, and an identifier <span class="name">ag</span> identifying an agent,
-<span class='conditional'>if</span> <span class="name">wasRevisionOf(e2,e1,ag)</span> holds, <span class='conditional'>then</span>
-there exists an entity with some identifier <span class="name">e</span> and some attribute-values <span class="name">eAttrs</span>, <span class="name">dAttrs</span>, such that the following
+<span class='conditional'>if</span> <span class="name">wasRevisionOf(-,e2,e1,ag)</span> holds, <span class='conditional'>then</span> the following
hold:
<pre>
-wasDerivedFrom(e2,e1,dAttrs)
-entity(e,eAttrs)
-specializationOf(e2,e)
-specializationOf(e1,e)
+wasDerivedFrom(-,e2,e1,-)
+alternateOf(e1,e2)
wasAttributedTo(e2,ag)
</pre>
</div>
-<p>
-<div id="optional-attributes5">In a revision of the form <span class="name">wasRevisionOf(e2,e1,-,attr)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
-
-
+<div class="note">
+ The following doesn't make sense because wasRevisionOf and
+ wasDerivedFrom have different types.
+ </div>
<p><span class="name">wasRevisionOf</span> is a strict sub-relation
of <span class="name">wasDerivedFrom</span> since two entities <span class="name">e2</span> and <span class="name">e1</span>
may satisfy <span class="name">wasDerivedFrom(e2,e1)</span> without being a variant of
@@ -516,7 +566,7 @@
<p>Traceability allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
<p>Traceability can be inferred from existing descriptions, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured
-by the following inference and constraint, respectively.
+by the following inferences:
<div class='inference' id='traceability-inference'>
Given two identifiers <span class="name">e2</span> and <span class="name">e1</span> for entities,
@@ -546,7 +596,7 @@
<p>We note that the inference rule <a
href="#traceability-inference">traceability-inference</a> does not
allow us to infer anything about the attributes of the related
-entities or events.
+entities, agents or events.
</p>
</section>
@@ -556,42 +606,46 @@
<section>
<h3>Component 4: Alternate Entities</h3>
-<div class="note">TODO: There are currently no widely agreed inferences on
- alternate or specialization.
+<div class="note">TODO: There is currently no consensus what inferences on
+ alternate or specialization should be assumed.
</div>
- The relation alternateOf is an equivalence relation: reflexive,
+ The relation <span class='name'>alternateOf</span> is an equivalence relation: reflexive,
transitive and symmetric.
<div class='inference' id="alternate-reflexive">
- For any entity e, we have alternateOf(e,e).
+ For any entity <span class='name'>e</span>, we have <span class='name'>alternateOf(e,e)</span>.
</div>
<div class='inference' id="alternate-transitive">
- For any entities e1, e2, e3, if alternateOf(e1,e2) and
- alternateOf(e2,e3) then alternateOf(e1,e3).
+ For any entities <span class='name'>e1</span>, <span
+ class='name'>e2</span>, <span class='name'>e3</span>, <span class="conditional">if</span> <span class='name'>alternateOf(e1,e2)</span> and
+ <span class='name'>alternateOf(e2,e3)</span> <span class="conditional">then</span> <span class='name'>alternateOf(e1,e3)</span>.
</div>
<div class='inference' id="alternate-symmetric">
- For any entity e1, e2, if alternateOf(e1,e2) then alternateOf(e2,e1).
+ For any entity <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>if</span> <span class='name'>alternateOf(e1,e2)</span> <span class='conditional'>then</span> <span class='name'>alternateOf(e2,e1)</span>.
</div>
Similarly, specialization is a partial order: it is reflexive and
transitive.
<div class='inference' id="specialization-reflexive">
- For any entity e, we have specializationOf(e,e).
+ For any entity <span class='name'>e</span>, we
+ have <span class='name'>specializationOf(e,e)</span>.
</div>
<div class='inference' id="specialization-transitive">
- For any entities e1, e2, e3, if specializationOf(e1,e2) and
- specializationOf(e2,e3) then specializationOf(e1,e3).
+ For any
+ entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, <span class='conditional'>if</span> <span class='name'>specializationOf(e1,e2)</span>
+ and
+ <span class='name'>specializationOf(e2,e3)</span> <span class='conditional'>then</span> <span class='name'>specializationOf(e1,e3)</span>.
</div>
If one entity specializes another, then they are also alternates:
<div class='inference' id="specialization-alternate">
- For any entities e1, e2 if specializationOf(e1,e2) then alternateOf(e1,e2).
+ For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>if</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>then</span> <span class='name'>alternateOf(e1,e2)</span>.
</div>
@@ -604,9 +658,44 @@
</section>
-<div class="note">
- TODO Merge material from <a href="#definitional-constraints" class="sectionRef"></a>.
- </div>
+ <section id="equivalence">
+<h2>Equivalence</h2>
+
+For the purpose of checking inferences and constraints, we define a
+notion of <a>equivalence</a> of PROV-DM instances. Equivalence is
+defined as follows:
+
+
+<ul>
+ <li>
+ The order of provenance expressions is irrelevant to the meaning of a PROV-DM instance. That is, a
+ PROV-DM instance is equivalent to any other instance obtained by
+ permuting its expressions.
+ </li>
+ <li>
+ Inference rules and definitions preserve equivalence. That is, a PROV-DM
+ instance is equivalent to the instance obtained by applying any
+ inference rule.
+ </li>
+ <li>Equivalence is reflexive, symmetric, and transitive.</li>
+</ul>
+
+<p>
+We define the <dfn>normal form</dfn> of a PROV-DM instance as the set
+of provenance expressions resulting from combining all of the
+expressions in the instance and applying all possible inference rules
+to this set. Formally, we say that two PROV-DM instances are
+<dfn>equivalent</dfn> if, after applying all applicable inference
+rules, they yield the same set of provenance expressions.
+</p>
+
+<p> An application that processes PROV-DM data SHOULD handle
+equivalent instances in the same way. (Common exceptions to this rule
+include, for example, pretty printers that seek to preserve the
+original order of statements in a file and avoid expanding
+inferences.) </p>
+
+</section>
</section> <!-- inferences -->
@@ -614,6 +703,8 @@
<h2>Validity Constraints</h2>
+
+
<p>
This section defines a collection of constraints on instances of
PROV-DM. An instance of PROV-DM is <dfn id="dfn-valid">valid</dfn>
@@ -640,24 +731,33 @@
is used).
</li>
</ul>
-
-<section id="structural-constraints">
+
+<div class="note">
+ TODO: More about what it means for constraints to be satisfied;
+ constraint template(s)
+ </div>
+
+ <section id="structural-constraints">
<h3>Uniqueness Constraints</h3>
<div class="note">
TODO Merge material from <a href="#structural-constraints"
class="sectionRef"></a> and <a href="#definitional-constraints" class="sectionRef"></a>.
</div>
+<div class="note">
+Attribute uniqueness constraints?
+</div>
<p> We assume that the various identified objects of PROV-DM have
unique expressions describing them within a PROV-DM instance.
</p>
<div class='constraint' id='entity-unique'>
-<p>Given an entity identifier <span class="name">e</span>, there is at most one description
+<p>Given an entity identifier <span class="name">e</span>, there is at most oneexpression
<span class="name">entity(e,attrs)</span>, where <span
class="name">attrs</span> is some set of attribute-values.</p>
</div>
<div class='constraint' id='activity-unique'>
-<p>Given an activity identifier <span class="name">a</span>, there is at most one description
+<p>Given an activity identifier <span class="name">a</span>, there is
+ at most one expression
<span class="name">activity(a,t1,t2,attrs)</span>, where <span
class="name">attrs</span> is some set of attribute-values.</p>
</div>
@@ -685,8 +785,18 @@
<span class='conditional'>then</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.
</div>
+<div class="note">
+Wouldn't the above constraint violate uniqueness?
+</div>
+
+<div class="note">
+Invalidation uniqueness?
+</div>
+
<p>A generation can be used to indicate a generation time without having to specify the involved activity. A generation time is unique, as specified by the following constraint.<p>
-
+<div class="note">
+Seems redundant given generation-uniqueness
+</div>
<div class='constraint' id='unique-generation-time'>
Given an entity denoted by <span class="name">e</span> and
two time instants <span class="name">t1</span> and <span
@@ -747,13 +857,13 @@
though the actual mapping is not in scope of this specification.</p>
<p>Given that provenance consists of a description of past entities
-and activities, to be valid provenance descriptions MUST
+and activities, <a>valid</a> provenance descriptions MUST
satisfy <em>ordering constraints</em> between instantaneous events, which we introduce in
this section. For instance, an entity can only be used after it was
generated; hence, we say that an entity's <a title="entity generation
event">generation event</a> precedes any of this
-entity's <a title="entity usage event">usage event</a>. Should this
-ordering constraint be proven invalid, the associated generation and
+entity's <a title="entity usage event">usage events</a>. Should this
+ordering constraint be violated, the associated generation and
usage could not be credible. The rest of this section defines
the <dfn>temporal interpretation</dfn> of provenance descriptions as a
set of instantaneous event ordering constraints. </p>
@@ -790,48 +900,32 @@
</div>
+<section>
+<h3>Activity constraints</h3>
+
+<p>
+In this section we discuss constraints from the perspective of
+the <a>lifetime</a> of an activity. An activity starts, then during
+its lifetime uses, generates entities and communicates with or starts
+other
+activities, and finally ends. The following constraints amount to
+checking that all of the events associated with an activity take place
+within the activity's lifetime, and the start and end events mark the
+start and endpoints of its lifetime.
+</p>
<p>The existence of an activity implies that the <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
event</a>. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (a) and expressed by constraint <a href="#start-precedes-end">start-precedes-end</a>.</p>
-<div class='constraint' id='start-precedes-end'> The following ordering constraint holds for any activity: the
-<a title="activity start event">start event</a> <a>precedes</a> the <a title="activity end event">end event</a>.</div>
-
-<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation
-event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (b) and expressed by constraint <a href="#generation-precedes-usage">generation-precedes-usage</a>.</p>
-
-<div class='constraint' id='generation-precedes-usage'>For any entity, the following ordering constraint holds: the <a title="entity generation event">generation</a> of an entity always
-<a>precedes</a> any of its <a title="entity usage event">usages</a>.
-</div>
-
-<div class="note">
-ISSUE-345: does not clearly delineate where the discussion for one constraint starts and where the next ends.
- </div>
-
-<p>Invalidation is defined at the event at which an entity ceases to exist as such. All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p>
-
-<div class='constraint' id='usage-precedes-invalidation'>For any entity, the following ordering constraint holds: any <a title="entity usage event">usage</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
-</div>
-
-<p>Similarly, generation of an entity precedes its invalidation. (This
-follows from other constraints if the entity is used, but we state it
-explicitly to cover the case of an entity that is generated and
-invalidated without being used.)</p>
-
-<div class='constraint' id='generation-precedes-invalidation'>For
- any entity, the following ordering constraint holds: the <a
- title="entity generation event">generation</a> of an entity always
-<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
-</div>
-
+<div class='constraint' id='start-precedes-end'>The
+<a title="activity start event">start event</a> of any
+activity <a>precedes</a> its <a title="activity end event">end event</a>.</div>
<p>A usage implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (c) and expressed by constraint <a href="#usage-within-activity">usage-within-activity</a>.</p>
<div class='constraint' id='usage-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span>
- <span class="name">used(a,e,attrs)</span> or <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
+ <span class="name">used(a,e,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint holds:
the <a title="entity usage event">usage</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a> of
activity denoted by <span class="name">a</span> and <a>follows</a> its <a title="activity start event">start</a>.
</div>
@@ -842,12 +936,79 @@
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (d) and expressed by constraint <a href="#generation-within-activity">generation-within-activity</a>.</p>
<div class='constraint' id='generation-within-activity'>Given an activity with identifier <span class="name">a</span>, an entity with identifier <span class="name">e</span>, a set
-of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span> <span class="name">wasGeneratedBy(e,a,attrs)</span> or <span
+of attribute-value pairs <span class="name">attrs</span>, and optional time <span class="name">t</span>, <span class='conditional'>if</span> <span
class="name">wasGeneratedBy(e,a,attrs,t)</span> holds, <span class='conditional'>then</span> the following ordering constraint also holds: the <a title="entity generation
event">generation</a> of the entity denoted by <span class="name">e</span> <a>precedes</a> the <a title="activity end event">end</a>
of activity <span class="name">a</span> and <a>follows</a> the <a title="activity start event">start</a> of <span class="name">a</span>.
</div>
+<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
+title="instantaneous event">events</a>, since some entity must have been generated by the former and used by the latter, which implies that the start event of <span class="name">a1</span>
+cannot follow the end event of <span class="name">a2</span>. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (g) and expressed by constraint <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.</p>
+
+<div class='constraint' id='wasInformedBy-ordering'>
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
+class="name">wasInformedBy(a2,a1)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraint holds:
+the <a title="activity start event">start event</a> of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
+the activity denoted by <span class="name">a2</span>.
+</div>
+
+<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
+title="instantaneous event">events</a>, since <span class="name">a1</span> must have been active before <span class="name">a2</span> started. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
+
+
+<div class='constraint' id='wasStartedBy-ordering'>
+Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
+class="name">wasStartedBy(a2,a1)</span>
+ holds, <span class='conditional'>then</span> the following ordering constraint holds: the
+<a title="activity start event">start</a> event of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
+the activity denoted by <span class="name">a2</span>.
+</div>
+
+</section>
+
+<section>
+<h3> Entity constraints</h3>
+
+<p>
+As with activities, entities have lifetimes: they are generated, then
+can be used, revised, or other entities can be derived from them, and
+finally are invalidated.
+</p>
+</p>
+<p>Generation of an entity precedes its invalidation. (This
+follows from other constraints if the entity is used, but we state it
+explicitly to cover the case of an entity that is generated and
+invalidated without being used.)</p>
+
+<div class='constraint' id='generation-precedes-invalidation'>The <a
+ title="entity generation event">generation</a> of an entity always
+<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+</div>
+
+<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation
+event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
+illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (b) and expressed by constraint <a href="#generation-precedes-usage">generation-precedes-usage</a>.</p>
+
+<div class='constraint' id='generation-precedes-usage'>The <a title="entity generation event">generation</a> of an entity always
+<a>precedes</a> any of its <a title="entity usage event">usages</a>.
+</div>
+
+
+<p>All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p>
+
+<div class='constraint' id='usage-precedes-invalidation'>Any <a title="entity usage event">usage</a> of an entity always
+<a>precedes</a> its <a title="entity invalidation event">invalidation</a>.
+</div>
+
+
+
+
+
+
@@ -889,34 +1050,18 @@
which implies ordering ordering between the usage of <span class="name">e1</span> and
generation of <span class="name">e2</span>. </p>
-<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
-title="instantaneous event">events</a>, since some entity must have been generated by the former and used by the latter, which implies that the start event of <span class="name">a1</span>
-cannot follow the end event of <span class="name">a2</span>. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (g) and expressed by constraint <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.</p>
-
-<div class='constraint' id='wasInformedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
-class="name">wasInformedBy(a2,a1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds:
-the <a title="activity start event">start event</a> of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity end event">end event</a> of
-the activity denoted by <span class="name">a2</span>.
-</div>
-
-<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
-title="instantaneous event">events</a>, since <span class="name">a1</span> must have been active before <span class="name">a2</span> started. This is
-illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
-
-
-<div class='constraint' id='wasStartedBy-ordering'>
-Given two activities denoted by <span class="name">a1</span> and <span class="name">a2</span>, <span class='conditional'>if</span> <span
-class="name">wasStartedBy(a2,a1)</span>
- holds, <span class='conditional'>then</span> the following ordering constraint holds: the
-<a title="activity start event">start</a> event of the activity denoted by <span class="name">a1</span> <a>precedes</a> the <a title="activity start event">start event</a> of
-the activity denoted by <span class="name">a2</span>.
-</div>
-
-
-<p>Further constraints appear in Figure <a href="#constraint-summary2">constraint-summary2</a> and are discussed below.</p>
+</section>
+
+<section>
+<h3> Agent constraints</h3>
+
+<p>
+Like entities and activities, agents have lifetimes that follow a
+familiar pattern: an agent is generated, can participate in
+interactions such as starting, ending or association with an
+activity, attribution, or delegation, and finally the agent is invalidated.
+</p>
+<p>Further constraints associated with agents appear in Figure <a href="#constraint-summary2">constraint-summary2</a> and are discussed below.</p>
<div style="text-align: center;">
<figure>
@@ -928,11 +1073,12 @@
<p>The agent that started an activity must exist before the activity starts.
This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and expressed by constraint <a href="#wasStartedByAgent-ordering">wasStartedByAgent-ordering</a>.</p>
-
-
-<div class='constraint' id='wasStartedByAgent-ordering'>
-Given an activity denoted by <span class="name">a</span> and an entity denoted by <span class="name">e</span>, <span class='conditional'>if</span> <span
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (a) and expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
+
+
+<div class='constraint' id='wasStartedBy-ordering'>
+Given an activity denoted by <span class="name">a</span> and an entity
+denoted by <span class="name">e</span>, <span class='conditional'>if</span> <span
class="name">wasStartedBy(a,e)</span>
holds, <span class='conditional'>then</span> the following ordering constraints hold: the
<a title="activity start event">start</a> event of the activity denoted by <span class="name">a</span> <a>follows</a> the <a title="entity generation event">generation event</a> for entity <span class="name">e</span>, and
@@ -945,7 +1091,7 @@
activity ends, as illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (b).</p>
-<div class='constraint' id='wasEndedByAgent-ordering'>
+<div class='constraint' id='wasEndedBy-ordering'>
Given an activity denoted by <span class="name">a</span> and an entity denoted by <span class="name">e</span>, <span class='conditional'>if</span> <span
class="name">wasEndedBy(a,e)</span>
holds, <span class='conditional'>then</span> the following ordering constraints hold: the
@@ -976,7 +1122,7 @@
with the agent. The agent is required to exist before the entity
invalidation. Likewise, the entity generation must precede the agent destruction.
This is
-illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (d) and expressed by constraint <a href="#wasAttributedWith-ordering">wasAttributedWith-ordering</a>.</p>
+illustrated by Subfigure <a href="#constraint-summary2">constraint-summary2</a> (d) and expressed by constraint <a href="#wasAttributedTo-ordering">wasAttributedTo-ordering</a>.</p>
@@ -1006,6 +1152,8 @@
<a>precedes</a> <a title="entity invalidation event">invalidation</a> event for <span class="name">ag2</span>.
</div>
+</section>
+
</section> <!--event-ordering-constraints-->
</section> <!-- constraints -->
@@ -1157,6 +1305,10 @@
<section id="account-constraints">
<h2>Account Constraints</h2>
+<div class="note">
+Work on accounts has been deferred until after the next working draft,
+so this section is very unstable
+</div>
<p>PROV-DM allows for multiple descriptions of entities (and in general any identifiable object) to be expressed. </p>
@@ -1179,12 +1331,7 @@
<p>Two different descriptions of a same entity cannot co-exist in a same account
as formalized in <a href="#unique-description-in-account">unique-description-in-account</a>.</p>
-<div class="note">
- TODO:
- We should list all of the other expressions to which this applies,
- maybe by defining the set of "object expressions" that have an
- identity.
- </div>
+<!-- Moved to uniqueness constraints section
<div class='constraint' id='unique-description-in-account'>
<p>Given an entity identifier <span class="name">e</span>, there is at most one description
<span class="name">entity(e,attrs)</span> occurring in a given account, where <span class="name">attrs</span> is some set of attribute-values. Other descriptions of the same entity can exist in different accounts.</p>
@@ -1192,6 +1339,7 @@
<p>This constraint similarly applies to all other types and relations,
with explicit identity.</p>
</div>
+-->
<p>
<div class="structural-forward">
@@ -1199,7 +1347,8 @@
</div>
-<p>In some cases, there may be a requirement for two different descriptions of a same entity to be included in a same account. To satisfy the constraint <a href="#unique-description-in-account">unique-description-in-account</a>, we can adopt a different identifier for one of them, and relate the two descriptions with the <span class="name">alternateOf</span> relation. </p>
+<p>In some cases, there may be a requirement for two different
+ descriptions of the same entity to be included in the same account. To satisfy the constraint <a href="#unique-description-in-account">unique-description-in-account</a>, we can adopt a different identifier for one of them, and relate the two descriptions with the <span class="name">alternateOf</span> relation. </p>
<div class="anexample" id="merge-with-rename">
<p>We now reconsider the same two descriptions of a same entity, but we change the identifier for one of them:</p>
@@ -1288,9 +1437,7 @@
</div>
-<div class='note'>Collect the discussion of uniqueness of generation
- in one place</div>
-
+
<p>Structurally well-formed provenance satisfies some constraints, which force the structure of descriptions to be exposed by means of accounts. With these constraints satisfied, further
inferences can be made about structurally well-formed descriptions.
The uniqueness of generations in accounts is formulated as follows.
@@ -1314,16 +1461,18 @@
<ul><li>When processing provenance obtained from another source, an
application MAY apply the inferences and definitions in <a
href="#inferences" class='sectionRef'></a>.</li>
+ <li>An application SHOULD process <a>equivalent</a> PROV-DM
+ instances in the same way, described in <a href="#equivalence" class="sectionRef"></a>
+ <li>When determining whether a PROV-DM instance is <a>valid</a>, an
+ application MUST check that all of the
+ constraints of <a href="#constraints" class="sectionRef"></a> are
+ satisfied on the <a>normal form</a> of the instance.</li>
<li> When producing provenance meant for other applications to
use, the application SHOULD produce valid provenance. </li>
- <li>When determining whether provenance is <a>valid</a>, an
- application MUST check that all of the
- constraints are satisfied, even if some
- inferences and definitions are used.</li>
-</ul>
+ </ul>
<div class="note">
Should we specify a way for PROV-DM instances to say whether they
- are meant to be validated or not?
+ are meant to be validated or not? Seems outside the scope of this document.
</div>
</section>
@@ -1333,9 +1482,6 @@
<h2>Rationale for inferences and constraints</h2>
-
-<div class='note'>TODO: Better section title/headings; move this
- material later or embed it into appropriate sections</div>
<section id='section-attributes'>
<h4>Entities and Attributes</h4>