Serge Abiteboul

Pierre Bourhis

Victor Vianu

Explanations and Transparency in Collaborative Workflows

Keywords: data-centric workflows, collaboration, views, explanations

We pursue an investigation of data-driven collaborative workflows. In the model, peers can access and update local data, causing side-e↵ects on other peers' data. In this paper, we study means of explaining to a peer her local view of a global run, both at runtime and statically. We consider the notion of "scenario for a given peer" that is a subrun observationally equivalent to the original run for that peer. Because such a scenario can sometimes di↵er significantly from what happens in the actual run, thus providing a misleading explanation, we introduce and study a faithfulness requirement that ensures closer adherence to the global run. We show that there is a unique minimal faithful scenario, that explains what is happening in the global run by extracting only the portion relevant to the peer.

With regard to static explanations, we consider the problem of synthesizing, for each peer, a "view program" whose runs generate exactly the peer's observations of the global runs. Assuming some conditions desirable in their own right, namely transparency and boundedness, we show that such a view program exists and can be synthesized. As an added benefit, the view program rules provide provenance information for the updates observed by the peer.

INTRODUCTION

Consider peers participating in a collaborative workflow. Such peers are typically willing to publicly share some data and actions, but keep others private or disclose them only to selected participants. During a run of the workflow, a peer observes side e↵ects of other peers' actions, but may wish to be provided with a more informative explanation of the workflow. At runtime, one would like to explain to each peer the side e↵ects she observes, in terms of the unfolding run. Statically, one would like to provide the peer with a program specifying all the transitions she may observe. In this paper, we consider the problem of providing peers with such runtime and static explanations. In particular, we identify two natural properties of workflows, transparency and boundedness, that are of interest in their own right and greatly facilitate the explanation task.

We use the data-driven collaborative workflow model of [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF]. In contrast to process-centric workflows, datadriven workflows treat data as first-class citizens [START_REF] Nigam | Business artifacts: An approach to operational specification[END_REF]. In our collaborative workflow model, each peer sees a view of a global database, that hides some relations, columns of other relations (projection), and tuples (selection).

The workflow is specified by datalog-style rules, with positive and negative conditions in rule bodies, and insertions/deletions in rule heads. An event in the system is an instantiation by some peer of a rule in the workflow's program. Consider a run of a workflow and a particular peer, say p. To be able to understand a run from p's perspective, it is useful to isolate the portion of the run relevant to p from other computations that may be occurring in the system. Towards this goal, we introduce the notion of scenario for p, which is a subrun that is observationally equivalent for p to the original run. Such a scenario includes events visible at p, but also events initiated by other peers, that have no immediate side-e↵ects visible at p, but eventually enable events with visible side-e↵ects. Among possible scenarios, minimal ones are desirable because they exclude redundant or useless (from the peer's viewpoint) events.

We show that computing minimal scenarios for a peer is generally hard (coNP-complete). Moreover, despite being observationally equivalent to the original run, scenarios can be misleading by di↵ering considerably from what occurs in the actual run. To overcome these issues, we consider an additional property of scenarios, called faithfulness, that guarantees tighter consistency between the scenario and the actual run. Moreover, faithful scenarios turn out to be particularly well behaved. They form a semiring with respect to natural operators, which enables e cient computation of minimal faithful scenarios, as well as their incremental maintenance. We show that every run has a unique minimal faithful scenario for each peer, that can be computed efficiently. We use minimal faithful scenarios as the natural semantic and computational basis for explaining runs.

We then turn to the ambitious goal of providing static specifications of the runs as seen from a peer's perspective, which we call view programs for that peer. While such programs cannot generally exist for informationtheoretic reasons, we consider some natural properties of workflows allowing to construct view programs that define precisely a peer's observations of the workflow runs.

The properties we consider, transparency and boundedness, are often desirable in practice, for technical and even ethical reasons. In layman terms, an algorithm is transparent (for a specific purpose) if it discloses its motivation and actions. In workflows involving human participants (often the case for collaborative workflows), one might want to require transparency for particular users; indeed, one may be compelled by law to do so in certain settings. Intuitively, a workflow is transparent for a peer if the data that the peer sees at each point in a run is su cient to determine all possible future transitions visible at that peer. For example, if a CEO vetoes the hiring of Alice, and as a consequence it becomes certain that she cannot be hired in the future, this information must be disclosed to her in the next transition she sees.

Boundedness is a more technical condition. For an integer h, h-boundedness of a run for a peer p limits to h the number of consecutive events invisible but relevant to p that the other peers can perform. (This does not prevent them from performing arbitrarily long sequences of events irrelevant to that particular peer.)

We show that one can decide whether, for a given h, a workflow program only produces transparent and hbounded runs for a particular peer. Furthermore, when this is the case, one can construct a "view program" for a peer that specifies exactly the transitions that peer may see. The rules of the program also provide the peer with provenance information, consisting of the facts visible to that peer that have led to the transition. Because of boundedness, the provenance always involves a bounded number of tuples, which allows their static specification in the bodies of rules of the view program.

The synthesis of view-programs described in Section 5 is related in spirit with partner synthesis in services modeled as Petri Nets [START_REF] Wolf | Does my service have partners? Trans. Petri Nets and Other Models of Concurrency[END_REF][START_REF] Lohmann | Wendy: A tool to synthesize partners for services[END_REF][START_REF] Sürmeli | Synthesizing cost-minimal partners for services[END_REF].

With practical considerations in mind, we lastly present some design guidelines for producing transparent and hbounded programs for a specified peer. We also show that, for a large class of programs, one can force transparency and h-boundedness by rewriting each program so that, modulo minor di↵erences, it has the same transparent and h-bounded runs as the original and filters out runs violating these properties.

The article is organized as follows. The model is described in Section 2. Scenarios are considered in Section 3, faithfulness in Section 4, transparency and view programs in Section 5, and design methodology for transparent and bounded programs in Section 6. Related work and conclusions are considered in two last sections. Some of the proofs are relegated to an appendix.

COLLABORATIVE WORKFLOW

In this section, we recall the collaborative workflow model of [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF], introducing minor extensions.

We start with some basic terminology. We assume an infinite data domain dom with a distinguished element ? (intuitively denoting an undefined value), and including an infinite set P 1 of peers. We also assume an infinite domain of variables var disjoint from dom. A relation schema is a relation symbol together with a sequence of distinct attributes. We denote the sequence of attributes of R by att(R). A database schema is a finite set of relation schemas. A tuple over R is a mapping from att(R) to dom. An instance of a database schema D is a mapping I associating to each R 2 D a finite set of tuples over R, i.e., a relation over R. We denote by Inst(D) the set of instances of D.

We assume that each relation schema R is equipped with a unique key, consisting, for simplicity, of a single attribute K (the same for all relations). An instance I 2 Inst(D) is valid (for the key constraints) if, for each R 2 D, no tuple in I(R) has value ? for attribute K, and there are no distinct tuples u, v in I(R) with the same key. We denote by Inst K (D) the set of valid instances of D.

We can apply to each instance I 2 Inst(D) the following chase step up to a fixpoint J denoted chase K (I): for some R, some A, and distinct u, v in I(R), with u(K) = v(K), u(A) 6 =?, and v(A) =?, replace v by v 0 identical to v except that v 0 (A) = u(A).

Note that the chase turns some invalid instances into valid ones, while for others it terminates with invalid instances. More precisely, an instance is turned into a valid one i↵ it contains no two tuples with the same key and distinct non-null values for the same attribute. In this case, the result of the chase is unique.

For technical reasons, we associate to each relation R (with attribute K), a unary relational view Key R , that consists of the projection of R on K, i.e., for each R and instance I, I(Key R ) = ⇡ K (I(R)). We recall the notion of full conjunctive query with negation (FCQ ¬ query for short). It is adapted to our context to take into account the view relations for keys. A term is a variable or a constant. A literal is of the form (¬) R(x), (¬) Key R (y), x = y, or x 6 = y, where x is a sequence of terms of appropriate arity, x is a variable, and y a term. A FCQ ¬ query is an expression A 1 ^... ^An (for n 0) where each A i is a literal and such that each variable occurs in some positive literal R(u) (a safety condition).

Observe that the use of a literal Key R (k) is syntactic sugar, since it can be replaced by R(k, z 1 , ...) where the z i are new. On the other hand, the use of ¬Key R (k) is not.

For attributes A, B, and a in dom (possibly ?) , A = a and A = B are elementary conditions. A condition is a Boolean combination of elementary conditions. Peer views of the database will be defined using projections and selections. Note that, in order to enable powerful static analysis, the views in [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF] did not use selections. The more powerful views used here better capture realistic peer views.

Collaborative schema. We now define collaborative workflow schemas, extending the definition in [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF]. Starting from a global database schema D and a finite set P of peers participating in the workflow, the collaborative schema specifies, for each peer p, a view of the database. The view consists of selection-projection views of a subset of the relations in D. A view of R 2 D for a peer p (if provided) is denoted R@p. The view allows p to see only some of the attributes of R (projection on att(R@p)) and only some of the tuples (specified by a selection denoted (R@p)). The view of a global instance I of D at p is denoted I@p. Before providing the formal definition, we introduce the following notation. For a relation R and an instance J over a subset att(J) of att(R), J ? denotes the instance of R obtained by padding all tuples of J with the value ? on all attributes in att(R) att(J). Definition 2.1. For a global database schema D, a collaborative schema S consists of a finite set P of peers, and for each p 2 P, a view schema D@p such that:

• each relation in D@p is of the form R@p for R in D, • for each R@p, K 2 att(R@p) ✓ att(R).
To each relation R@p 2 D@p is associated a selection condition (R@p) over att(R). For an instance I over D, the view instance of I at peer p, denoted I@p, is the instance over D@p defined by: for each R@p in D@p,

• I@p(R@p) = ⇡ att(R@p) ( (R@p) (I(R))
). Furthermore, we impose the following (losslessness) condition: For each

I 2 Inst K (D) and R 2 D, I(R) = chase K ⇣ [ {(I@p(R@p)) ? | p 2 P, R@p 2 D@p}

⌘

The losslessness property guarantees that for each tuple in I(R), and each A in R, the value of the tuple for A is visible at some peer. The global instance can therefore be recovered from its peer views using the chase. One can e↵ectively check whether a collaborative schema has the losslessness property.

Let S be a collaborative schema, with global schema D and set P of peers. A peer p can perform two kinds of updates on a valid instance I:

• A deletion of the form Key R@p (k), where R@p 2 D@p and k is a key value in I@p(R@p). The deletion results in removing from I(R) the tuple with key k.

• An insertion of the form +R@p(u), where R@p 2 D@p and u is a tuple over att(R@p) such that:

-(i) J = chase K (I [ {R(u ? )}
) is valid, and -(ii) u is subsumed by some tuple v in J@p(R@p). Then J is the result of the insertion.

Note that the semantics of an update requested by some peer is specified on the global instance. This circumvents the view update problem. Observe also that a peer can delete only a tuple the peer sees, and that, if an insertion succeeds, the tuple the peer inserted is part of its view after the update (by (ii)).

Some subtleties of updates are illustrated next.

Example 2.2. Suppose the database consists of a single relation R over KAB, and we have two peers p, q, att(R@p) = KAB, att(R@q) = KA, (R@p) is A = ?, and (R@q) is true. The losslessness condition is not satisfied by this schema. For example, consider the global instance I obtained using the sequence of inserts: +R@p(k, ?, c); +R@q(k, a). It consists of a single tuple, R(k, a, c). Note that as a result of the second insertion, the tuple with key k disappears from the view of p. Moreover, I cannot be reconstructed from the collective views of the peers (and the value "c" is lost). The losslessness condition prevents such anomalies. Moreover, it allows treating the global instance as a virtual rather than materialized database, represented in a distributed fashion by the views of the peers.

Collaborative workflow.

A collaborative workflow specification (in short workflow spec) W consists of a collaborative schema S and a workflow program for W, i.e., a finite set of "update rules" for each peer p of W.

The rules are defined using the auxiliary notion of "update atom" as follows. An update atom at p is an insertion atom or a deletion atom. An insertion atom at p is of the form +R@p(x) where R@p 2 D@p and x is a tuple of variables and constants, of appropriate arity. A deletion atom p is an expression Key R@p (x), where R@p 2 D@p and x is a variable or constant.

A rule at peer p is an expression Update :-Cond where:

• Cond is a FCQ ¬ query over D@p, and • Update is a sequence of update atoms at p such that: If the sequence includes two updates of the same relation R of tuples with keys x, x 0 , respectively, then x and x 0 are not both the same constant and the body includes a condition x 6 = x 0 .

In the previous definition, the conditions x 6 = x 0 impose that no two updates in the same rule a↵ect the same tuple. As a consequence, the order of the update atoms in a rule is irrelevant. An example of rule is the following, where Assign(x, y) says that employee x is assigned to project y, and HR is the Human Relations peer:

Key Assign@HR (x), + Assign@HR(x 0 , y) : Assign@HR(x, y), Replace@HR(x, x 0 ), x 6 = x 0

The rule allows the HR peer to replace employee x by employee x 0 on project y.

If P is the program of a workflow spec W for a collaborative schema S, we speak simply of the (workflow) program P when S and W are understood.

Let P be a program. To simplify, we assume that a run of P starts from the empty instance (note that an arbitrary "initial" instance can be constructed by the peers due to losslessness). The global instance then evolves under transitions caused by updates in rule instantiations, defined next. Let ↵ = Update(ȳ) :-Cond(x) be a rule of P at some peer p where x are the variables occurring in Cond and ȳ are the variables in Update. A valuation ⌫ of ↵ for a global instance I is a mapping from ȳ [ x to dom such that I@p |= Cond(⌫(x)). For a valuation ⌫ of a rule ↵ at some p for some I, the instantiation ⌫↵ is called an event; p the peer of this event, denoted peer (⌫↵), and ↵ its rule.

We define the transition relation `e among valid global instances of D as follows. For I, J, and some event e as above, I `e J if all insertions and deletions in Update(⌫(ȳ)) are applicable, and J is obtained from I by applying them in any order.

A run of P is a finite sequence ⇢ = {(e i , I i )} 0in , such that ; `e0 I 0 , where ; is the empty instance; and for each 0 < i  n, I i 1 `ei I i . Additionally, we require: for each event e i = ⌫↵, if x is a variable occurring in the head of ↵ but not in its body, then x must be instantiated to a globally fresh value, i.e. ⌫(x) does not occur in const(P ) or in I 1 . . . I i 1 . We denote by Runs(P ) the set of runs of P .

Let ⇢ = {(e i , I i )} 0in be a run of P . Note that the event sequence (e 1 ...e n ), denoted e(⇢), uniquely determines the run ⇢. By slight abuse, we sometimes call run a sequence (e 1 ...e n ) of events that yields a run. It is occasionally useful to consider runs starting from an arbitrary initial instance I rather than ;. A run on initial instance I is defined in the obvious manner, by replacing ; with I in the previous definition.

Normal-form programs. We show a normal form for workflow programs that will be particularly useful in the next sections. A workflow program P is in normal form if (i) each rule whose head contains a deletion Key R@q (x) also contains a literal R@q(x, u) in its body, and (ii) rule bodies do not contain negative literals of the form ¬R@q(x, u) or positive literals of the form Key R@q (x). Intuitively, (i) simply makes explicit that deletion updates are e↵ective. (Recall that this is imposed by the definition of deletion.) As for (ii), it allows distinguishing between the cases when a fact R@q(k, u) is false because no tuple in R@q has key k, or because R@q(k, v) is a fact for some v 6 = u. Thus, rules in normal form provide more refined information. We next show that this does not limit the expressivity of the model. Proposition 2.3. For each workflow program P , one can construct a normal-form program P nf , and a function ✓ from the rules of P nf to rules of P , such that

⇢ = {(e i , I i )} 0in is a run of P i↵ ⇢ nf = {(f i , I i )} 0in is a run of P nf for some {f i } 0in such that peer(e i ) = peer(f i ) and rule(e i ) = ✓(rule(f i )). Proof.
Informally, P nf is constructed as follows.

For each rule containing a deletion Key R@q (x) in its head, a literal R@q(x, u) is added to the body, where u consists of distinct new variables. This guarantees (i). For (ii), a literal Key R@q (x) occurring in the body of some rule of P can be replaced by a literal R@q(x, u), where u consists of distinct new variables. Now suppose a literal ¬R@q(x, u) occurs in the body of some rule r of P . First, an instantiation ⌫ of this rule may hold because ¬Key R@q (⌫(x)) holds. Then this can be captured by a rule obtained from r by replacing ¬R@q(x, u) by ¬Key R@q (x). Next, an instantiation ⌫ of r may hold because R@q(⌫(x), v) holds for some v and ⌫(u(A)) 6 = v(A) for some attribute A 6 = K of R@q. Then this can be captured by a rule obtained from r by replacing ¬R@q(x, u) by R@q(x, z) where z is a tuple of distinct new variables, and adding the condition u(A) 6 = z(A). Note that the previous construction replaces r with a set Rules(r) of rules in P nf , corresponding to the different cases. The mapping ✓ is defined by ✓(r 0 ) = r for each r 0 2 Rules(r). Rules r of P that are not modified are included as such in P nf , and ✓(r) = r.

VIEWS AND SCENARIOS

In this section, we isolate the portions of a run that are relevant to a particular peer and accurately mirror what is actually occurring in the workflow from that peers viewpoint. Towards this goal of filtering out irrelevant events, we introduce the notions of subruns and scenarios. In the next section, we further consider scenarios called faithful that adhere more closely to the actual run and also turn out to have desirable properties from a semantic and computational viewpoint.

We first define the p-view of a run, for a peer p. Intuitively, this is the most basic view of a run, consisting essentially of the observations of peer p. Let ⇢ = {(e i , I i )} 0in be a run of P . An event e i is visible at p if peer(e i ) = p or peer(e i ) 6 = p and I i 1 @p 6 = I i @p. Otherwise, e i is invisible (or silent) at p. The p-view of an event e, denoted e@p, is e if peer(e) = p and ! if peer(e) 6 = p, where ! is a new symbol (standing for "world"). Definition 3.1. Let ⇢ = {(e i , I i )} 0in be a run of P , p a peer, and ⇢ 0 = {(e i @p, I i @p)} 0in . The sequence obtained from ⇢ 0 by deleting all (e i @p, I i @p) such that e

i is invisible at p, is called the view of ⇢ at p, and denoted ⇢@p. We denote Runs@p(P ) = {⇢@p | ⇢ 2 Runs(P )}. Thus, ⇢@p consists of all transitions caused by p marked with e i @p, as well as all transitions of events visible at p caused by other peers, marked with !.

We next consider subruns of a given run, with the goal of isolating the portion of the run that is relevant to p, and which can be used as a sound basis for providing the peer with additional information. For example, in Section 5 we discuss richer views that include provenance information for the updates observed by a peer, extracted from subruns relevant to the peer.

A subrun b ⇢ of ⇢ is a run such that e(b ⇢) is a subsequence of e(⇢). In a subrun, only some of the events of ⇢ are retained, in the same order as they occur in ⇢. Observe that the instances in b ⇢ are typically di↵erent than those in ⇢. Of course, not all subsequences of e(⇢) yield subruns. If a subsequence ↵ of e(⇢) does yield a subrun, it is denoted run(↵) (or ↵ by slight abuse).

We are interested in those subruns of a run that are compatible with p's observations of the run. This is captured by the notion of "scenario". We will, in particular, be interested by "minimal" such scenarios that, in some sense, explain what can be observed by p in a non-redundant manner. Definition 3.2. Let P be a workflow program, p a peer of P , and

⇢ = {(e i , I i )} 0in a run of P . A sce- nario of ⇢ at p is a subrun b ⇢ of ⇢ such that ⇢@p = b ⇢@p. A scenario b ⇢ of ⇢ at p is minimal if there is no sce- nario ⇢ of ⇢ at p for which e(⇢) is a strict subsequence of e(b ⇢). A minimal scenario is minimum if there is no shorter scenario of ⇢ at p.
Clearly, ⇢ itself is a scenario for ⇢ at p, but is likely to include portions that are irrelevant to p's observations, which motivates the study of minimal and minimum scenarios.

We next show that finding a minimum scenario is hard. (We will see that the problem is hard also for minimal scenarios.) In the proof, and throughout the paper whenever convenient, we use propositions in workflow programs as syntactic sugar. A proposition x can be simulated by a unary relation R x (with key K), a literal (¬)x by (¬)R x (0), an insertion or deletion of this literal by +R x (0) or Key R x (0).

Theorem 3.3. It is np-complete, given a workflow program P , a run ⇢ of P , a peer p and an integer N , whether there exists a scenario of ⇢ at p, of length at most N . Moreover, this holds even for workflows with ground positive rules and no deletions.

Proof. Membership in np is obvious. For hardness, we use a reduction from the hitting set problem. An instance of Hitting Set consists of a finite set

V = {v 1 , . . . , v n }, a set {c 1 , . . . , c
k } of subsets of V , and an integer M < n. It is np-complete whether there exists W ⇢ V of size at most M such that W \ c j 6 = ; for 1  j  k [START_REF] Garey | Computers and Intractibilitiy: A Guide to the Theory of NP-Completeness[END_REF]. From an instance of Hitting Set, we construct a program and a run ⇢ as follows. The schema consists of propositions

V i (1  i  n), C j (1  j  k)
, and OK. There are two peers p, q. Peer q sees all propositions and p only OK. The rules are the following:

(a) +V i @q :-, for each i 2 [1..n], (b) +C j @q :-V i @q, for each i 2 [1..n], j 2 [1..k], v i 2 c
j , (c) +OK@q :-C 1 @q, . . . , C k @q Observe that the workflow program uses only propositions.

Note that all rules belong to peer q but p can observe the value of OK. Intuitively, firing a subset of the (a)rules designates a subset W of V . With W chosen, the (b)-rules designate the sets c j hit by some element in W . If all sets are hit, rule (c) is enabled. Consider firing first all (a)-rules, followed by all (b) rules, and ending with rule (c). It is clear that this yields a run; call it ⇢. Intuitively, ⇢ corresponds to picking the trivial hitting set W = V . It is easy to check that there exists a hitting set W of size at most M i↵ there exists a scenario of ⇢ for p, of length at most M + k + 1.

For the specific runs ⇢ used in the proof, some minimal scenario can always be found e ciently in a greedy manner. (Start with ⇢. First, remove one (a)-rule at a time together with the (b) rules depending on it, and check if the remaining sequence is still a scenario. Then when no (a) rule can be further removed, keep only one (b) rule for each j. The resulting scenario is minimal.) However, this cannot be done for arbitrary runs. Indeed, the next result shows that testing whether a scenario is minimal is hard (see Appendix for proof).

Theorem 3.4. It is coNP-complete, given a workflow program P , a run ⇢ of P , and a peer p, whether ⇢ is a minimal scenario of ⇢ at p. Moreover, this holds even for workflows with ground positive rules and no deletions.

The lack of a unique minimal scenario of runs for a given peer is problematic when richer views need to be defined starting from several candidate minimal scenarios. Moreover, as seen in the next section, even minimal scenarios can provide misleading explanations about what occurs in the global run. We will propose a natural restriction called faithfulness, that overcomes the problems of unrestricted scenarios.

FAITHFUL SCENARIOS

A scenario b ⇢ of a run ⇢ at peer p produces the same observations as ⇢ at p, but is allowed to achieve this by means that di↵er considerably from what occurred in the original run. This can be misleading, as illustrated further in Examples 4.1 and 4.2. We therefore consider an additional property of subruns, called faithfulness, that guarantees tighter consistency between what happens in the subrun and in the actual run. The idea, that we will pursue in the next section, is that the workflow system wants to be more transparent for particular individual peers. Furthermore, as we shall see, faithful scenarios turn out to be particularly well behaved: each run has a unique minimal faithful scenario for p, computable in polynomial time, that explains what happens at p in a concise, non-redundant way. We also demonstrate useful properties of faithful scenarios, in particular that they are closed under intersection and union.

Before defining faithful scenarios, we illustrate some of the discrepancies that may arise between arbitrary scenarios and actual runs.

C i , i 2 [1, k].
Consider a run that derives OK. Suppose the run starts with V 1 @q :-; C 5 @q :-V 1 @q ; V 2 @q :-; C 5 @q :-V 2 @q.

Then a scenario could ignore C 5 @q :-V 1 @q although this is the event that actually derived C 5 @q.

Example 4.2. Consider a workflow with peers cto, ceo, assistant, and applicant and propositions ok and approval. The peers cto, ceo, and assistant all see ok and approval, and applicant sees only approval. Consider the run ⇢ consisting of the following events: e: +ok@cto :f : ok@cto :g: +ok@ceo :h: +approval@assistant :-ok@assistant

The subrun e h is a scenario of ⇢ at peer applicant. It indicates that the applicant's request was approved because it was ok'd by the cto. This subrun is misleading, since in the actual workflow, the cto retracted its ok and the request was approved by the ceo. This arises because the subrun ignores the deletion of ok@cto.

Let p be a fixed peer of some workflow program P and ⇢ a run. We next introduce the notion of "p-faithful subrun of ⇢", that prevents the kinds of anomalies previously illustrated. First, the definition is driven by the intuition that tuples in a given relation with a fixed key k represent evolving objects in the workflow. Objects identified by k can go through several lifecycles, occurring between the creation and deletion of a tuple with key k. Faithfulness requires that boundaries of lifecycles of events in the subrun be the same as those in the run, eliminating anomalies such as Example 4.2. It also requires that the events a↵ecting relevant attributes of object k in the same lifecycle be the same in the subrun as in the actual run, eliminating alternative subruns as in Example 4.1.

To define faithful subruns formally, we use the following auxiliary definitions. We assume wlog that all programs are in normal form. Let P be a program and ⇢ = {(e i , I i )} 0in a run of P . We say that k occurs as a key of R in an event e i of peer q, if it occurs in a literal R@q(k, ū) or ¬Key R@q (k) in the body of e i , or as an update +R@q(k, ū) or Key R@q (k) in the head of e i . We say that k occurs as a key of R in a sequence ↵ of events if it occurs as a key of R in some event of ↵. We denote the set of such keys by K(R, ↵).

Let k 2 K(R, e(⇢)) where We now define the ingredient of faithfulness concerning boundaries of lifecycles. For a subrun b ⇢ of ⇢, the requirement applies to e(b ⇢) alone. In fact, it will be useful to define this notion for arbitrary subsequences of e(⇢). Observe that boundaries of R-lifecycles of k in ⇢ that do not contain events in ↵ need not be included in ↵.

⇢ = {(e i , I i )} 0in . A closed R-lifecycle of k in ⇢ is an interval [i 1 , i 2 ] ✓ [0, n] such that e i1 inserts in
We now consider the last ingredient of faithfulness. Its definition relies on the auxiliary concept of the set of attributes of R that are "relevant" to peer q, that is denoted att(R, q). Specifically, the values on att(R, q) determine whether a given tuple is seen by q, and provides the visible values. Formally, for a peer q with selection condition (R@q), we define att(R, q) = att(R@q) [ att( (R@q)), where att( (R@q)) is the subset of attributes of R used in (R@q).

The last ingredient of faithfulness focuses on events that modify existing tuples with a given key. Intuitively, modification faithfulness for a peer p requires that, within a lifecycle of key k, all updates of attributes relevant to p must be included in the subsequence. It also requires that updates of attributes relevant to other peers participating in the subsequence be included as well.

Definition 4.4. Let ⇢ = {(e i , I i )} 0in be a run of P and p a fixed peer. A subsequence ↵ = {e ij } 0jm of e(⇢) is modification faithful for p if the following holds for each e ij , for each R and each k 2 K(R, e ij ): if e i belongs to the same R-lifecycle of k in ⇢ as e ij , i < i j , peer(e ij ) = q, and e i contains an insertion that turns in ⇢ some attribute in att(R, q) [ att(R, p) of an existing tuple with key k from ? to some other value, then e i also belongs to ↵.

Observe that boundary faithfulness is independent of the fixed peer p but modification faithfulness is dependent on p. We can now define the notion of faithful subsequence and subrun of a run. Observe that faithfulness rules out the counterintuitive scenarios in Examples 4.1 and 4.2. For instance, gh is an applicant-faithful subsequence of the run in Example 4.2, whereas eh is not. Moreover, note that gh is a subrun. This is not coincidental. We next show the following key fact: p-faithful subsequences of e(⇢) always yield scenarios of ⇢ for p. The proof is provided in the appendix. Lemma 4.6. Let ⇢ be a run of W, p a peer, and ↵ a p-faithful subsequence of e(⇢). Then (i) ↵ yields a subrun of ⇢, and (ii) run(↵) is a scenario of ⇢ for p.

We next show the existence of a unique minimal pfaithful scenario of ⇢ for p, that can be computed in ptime. To this end, we define an operator T p (⇢, •) on subsequences of e(⇢). For each subsequence ↵ of e(⇢), T p (⇢, ↵) consists of the subsequence of e(⇢) obtained by adding to ↵ all events of ⇢ whose presence is required by boundary and modification p-faithfulness due to events that are already in ↵.

Observe that (almost by definition) a subsequence ↵ of ⇢ is boundary and modification p-faithful i↵ it is a fixed-point of T p (⇢, •), i.e., T p (⇢, ↵) = ↵. Let ⌧ be the subsequence relation on sequences of events. Note that T p (⇢, •) is monotone with respect to ⌧, i.e., for ↵ ⌧ , T p (⇢, ↵) ⌧ T p (⇢, ). Consider the increasing sequence

↵ 0 = ↵, ↵ 1 = T p (⇢, ↵ 0 ), ↵ 2 = T p (⇢, ↵ 1 ), ... and let T ! p (⇢, ↵) = ↵ n
where n is the minimum integer for which ↵ n = ↵ n+1 . Now we have:

Theorem 4.7. Let P be a program schema. For each run ⇢ of P there is a unique minimal p-faithful scenario ⇢ of ⇢. Moreover, ⇢ equals run(T ! p (⇢, ↵)), where ↵ consists of all events of ⇢ visible at p, and can be computed from ⇢ in polynomial time.

Proof. Clearly, T ! p (⇢, ↵) is p-faithful, because it is a fixed-point of T p (⇢, •)
and contains all events of ⇢ visible at p. By Lemma 4.6, it also yields a scenario for p. Consider any p-faithful scenario ⇢ of ⇢ for p. By definition of p-faithfulness, ⇢ must include the events in ↵. From the fact that ↵ ⌧ e(⇢), T p (⇢, •) is monotone, and e(⇢) is a fixed-point of T p (⇢, •), it follows that T ! p (⇢, ↵) ⌧ e(⇢). Thus, ⇢ = T ! p (⇢, ↵) is the unique minimal p-faithful scenario of ⇢. Clearly, T ! p (⇢, ↵) can be computed in polynomial time from ⇢.

We now consider two natural ways of combining subsequences of a run ⇢, that are useful in many practical situations: "multiplying" them by taking the intersection of their events, and "adding" them by taking the union of their events. We will show that p-faithful subsequences of a run ⇢ are closed under both operations, and form a semiring.

Formally, let ↵ 1 and ↵ 2 be subsequences of e(⇢) for a run ⇢. Their product, denoted ↵ 1 ⇤↵ 2 is the subsequence consisting of the events in ⇢ occurring in both ↵ 1 and ↵ 2 . Their addition, denoted ↵ 1 + ↵ 2 , is the subsequence consisting of the events of ⇢ in ↵ 1 or ↵ 2 . Clearly, if ⇢ 1 and ⇢ 2 are subruns of ⇢, e(⇢ 1 ) + e(⇢ 2 ) and e(⇢ 1 ) ⇤ e(⇢ 2 ) are not guaranteed to yield subruns of ⇢.

Addition and multiplication of sequences are both of interest in practice. Closure under intersection is the core reason for the existence of a unique minimal pfaithful scenario for a peer. As we will see, addition is useful in incremental maintenance of minimal p-faithful scenarios.

We next show the following (see Appendix for proof).

Theorem 4.8. Let ⇢ be a run of W. The set of pfaithful scenarios of ⇢ is closed under addition and multiplication, and forms a semiring.

Incremental evaluation To conclude the section, we discuss how to maintain incrementally the minimum pfaithful scenario of a run, leveraging the closure under addition of p-faithful scenarios. More specifically, for a run ⇢, we wish to maintain incrementally T ! p (⇢, ↵), where ↵ consists of the events of ⇢ visible at p. To do so, we additionally maintain some auxiliary information, consisting of T ! p (⇢, f ) for each event f in ⇢. Intuitively, T ! p (⇢, f ) represents an "explanation" of the individual event f by a minimal boundary and modification pfaithful subrun of ⇢ containing f . Note that f need not be visible at p.

Suppose the current run is ⇢ and we have computed T ! p (⇢, ↵) and T ! p (⇢, f ) for each event f in ⇢. Now suppose that a new event e arrives. We need to compute the following (where ⇢.e denotes the concatenation of ⇢ and e):

(i) T ! p (⇢.e, f ), for each event f in ⇢.e. (ii) T ! p (⇢.e, ↵ 0 ), where ↵ 0 = ↵.e if e is visible at p and ↵ 0 = ↵ otherwise.

Consider (i). For f = e, T ! p (⇢.e, e) consists of e together with all events in T ! p (⇢, g) for some g 2 T p (⇢.e, e). For f 6 = e, there are two cases, depending on whether e is the right-boundary of an open lifecyle of a key occurring in T ! p (⇢, f ). If this is the case, meaning that e is in T p (⇢.e, T ! p (⇢, f )), then T ! p (⇢.e, f ) consists of e together with the events in T ! p (⇢, f ) and those in T ! p (⇢, g) for some g 6 = e in T p (⇢.e, e). Otherwise,

T ! p (⇢.e, f ) = T ! p (⇢, f ). Now consider (ii)
. Suppose e is visible at p, or is the right-boundary of an open lifecycle of a key in T ! p (⇢, ↵), meaning that e is in T p (⇢.e, T ! p (⇢, ↵)). Then T ! p (⇢.e, ↵ 0 ) consists of e together with the events in T ! p (⇢, ↵) and in T ! p (⇢, g) for some g 6 = e in T p (⇢.e, e). Otherwise,

T ! p (⇢.e, ↵ 0 ) = T ! p (⇢, ↵).
Observe that the incremental maintenance algorithm outlined above requires only single applications of the operator T p (⇢, •), avoiding computations of its least fixpoint from scratch. This is similar in spirit to results on incremental maintenance of recursive views by nonrecursive queries (e.g., see [START_REF] Dong | Incremental maintenance of recursive views using relational calculus/sql[END_REF]).

TRANSPARENCY & VIEW-PROGRAMS

The goal. Let P be a workflow program, and p a peer.

We have defined, for each run ⇢ of P , the view ⇢@p of the run as seen by peer p. As a next step, we would like to also provide p with a "view-program" P 0 whose runs are precisely the views Runs(P )@p. Intuitively, we wish such a program to provide p with an "explanation" of the global workflow in terms it can understand and access. The view-program will use the same schema D@p as p, and the fictitious peer ! (world) that represents the environment. The rules of P 0 consist of the rules of p in P , together with new rules for peer !, that define the transitions caused by other peers with visible side-e↵ects at p.

More precisely, a program P 0 is a view-program for P at p if:

• P 0 is over global schema D@p and uses two peers p and !, both with schema D@p, and all selection conditions true. • the rules of peer p are the same in P and P 0 .

• (completeness) for each run ⇢ of P , there exists a run ⇢ 0 of P 0 such that ⇢@p is obtained from ⇢ 0 by replacing all !-events with !. • (soundness) for each run ⇢ 0 of P 0 , there exists a run ⇢ of P , such that ⇢@p is obtained from ⇢ 0 by replacing all !-events with !.

We illustrate the notion of view-program with an example.

Example 5.1. Consider a program P with peers hr, ceo, cfo, and Sue, using the following rules: +Cleared@hr(x) :-+cfoOK@cfo(x) :-+Approved@ceo(x) :-Cleared@ceo(x), cfoOK@ceo(x) +Hire@hr(x)

:-Approved@hr(x)

Note that there are no rules for Sue. Suppose hr, cfo, and ceo see all relations, but Sue sees only relations Cleared and Hire. A view-program P 0 for Sue operates on the schema Cleared and Hire and has the following rules:

+Cleared@!(x) :-( †) +Hire@!(x)

:-Cleared@!(x)

It is easy to check that P 0 is sound and complete for P and peer Sue, and so it is a view-program for P at Sue. Remark 5.2. Observe that soundness and completeness of view-programs amounts to equivalence of P 0 and P with respect to the views of their linear runs. However, consider the following subtlety in the above example. By soundness of P 0 and rule ( †), if Sue sees Cleared(x), then there exists a run of P in which Sue sees Hire(x) inserted in the next transition visible to her. However, it is not the case that this is possible in every run of P , because the transition is also dependent on relation cfoOK, invisible to Sue. Enforcing this stronger property requires a more stringent notion of equivalence based on the trees of runs rather than just linear runs. We later show how this can be done by forbidding the use of information invisible to the given peer that affects the view of the peer. Intuitively, this makes the collaborative workflow more transparent to the peer. We formally introduce the notion of transparency further.

Note that one can trivially define a sound program for P at p (by keeping only the rules of P at peer p) and a complete one (by adding to the rules of p all rules at ! that insert or delete up to M arbitrary tuples in relations of D@p, where M is the maximum number of updates in the head of a rule in P ). Clearly, these are of little interest. Ideally, one would like a program that is both sound and complete. Unfortunately, as shown next, it is not generally possible to construct such a program.

Proposition 5.3. There exists a program P and a peer p, such that there exists no view-program for P at p.

Proof. (sketch) The program P uses three binary relations R, S, T that a peer q sees, whereas peer p sees only R, T . Suppose p has a rule inserting an arbitrary tuple in R (so p can construct arbitrary instances over R). Peer q has two rules to add to S pairs in the transitive closure of R. Finally, q has a rule to transfer a tuple (0, 1) from S to T . No view-program can exist for P at p because the insertion of the tuple (0, 1) in T @p is conditioned by the existence of a directed path of arbitrary length from 0 to 1 in R@p. This cannot be expressed by any rule with a bounded number of literals in its body.

Theorem 5.4. It is undecidable, given a program P and a peer p, whether there exists a view-program for P at p.

Proof. (sketch) We use the following observation:

(?) It is undecidable, given a program Q whose schema includes a unary relation U , whether there exists a run of Q leading to an instance where U is non-empty.

The proof of (?) is by a straightforward reduction from the Post Correspondence Problem, known to be undecidable [START_REF] Post | Recursive unsolvability of a problem of Thue[END_REF]. Intuitively, Q attempts to construct a solution to an instance of the PCP. If it succeeds, a fact is inserted in U (details omitted).

Consider the program P in the proof of Proposition 5.3, modified so that the rule to transfer the tuple S(0, 1) to T (0, 1) is controlled by non-emptiness of U . Now add to P the rules of an arbitrary program Q whose schema contains U (and no other relations of P ). Then a viewprogram at p exists for the resulting program i↵ there is no run of Q leading to some non-empty U . This is undecidable by (?).

Transparency and Boundedness. Clearly, an obstacle towards obtaining a view-program for P at p is that updates visible at p may depend on information unavailable to p. To overcome this di culty, we consider a property of programs called "transparency". Intuitively, transparency of a program P for peer p guarantees that the possible updates of a view instance I@p caused by other peers are determined by I@p. Put di↵erently, the other peers must disclose to p all information that they use in order to modify p's view of the data. The only action that can depend on hidden information is the creation of new values, which is constrained by the global history.

It turns out that transparency of a program P for p does not alone guarantee the existence of a viewprogram of P for p. This is because the other peers can still perform arbitrarily complex computations hidden from p. For instance, the program used in the proof of Proposition 5.3 is transparent for p but does not have a view-program for p. To control the complexity of computations a↵ecting p, we introduce a notion of "boundedness" of P with respect to p, that limits the number of steps invisible but relevant to p that are carried out by other peers. As we will see, transparency together with boundedness guarantee the existence of a view-program and its e↵ective construction.

We next define transparency, then turn to boundedness. To formalize the notion of transparency, we first define "fresh" instances, obtained as the results of events visible at p. We use the following notation. If ↵ is a sequence of events of P yielding a run on initial instance I, we say that ↵ is applicable at I and denote by ↵(I) the last instance in the run. Definition 5.5. Let P be a program and p a peer. An instance I is p-fresh if I = ; or there exists an instance I 0 and an event e of P that is applicable to I 0 and visible at p, such that e(I 0 ) = I.

We can now define transparency. We will use the notion of minimum p-faithful run, defined as follows. A run ↵ on initial instance I is a minimum p-faithful run if ↵ = T ! p (↵, v), where v consists of the events of ↵ that are visible at p. In other words, ↵ is its own minimum p-faithful scenario for p.

To deal with new values, we will need the following. For a sequence ↵, let adom(↵) consist of all values occurring in ↵, and new(↵) consist of all values a for which there is an event e in ↵ such that a occurs in the head but not in the body of e. Let const(P ) denote the set of constants used in program P , together with ?.

Definition 5.6. A program P is transparent for p if for all p-fresh instances I, J such that I@p = J@p the following holds. For every sequence ↵ of events such that adom(J)\new(↵) = ;, if ↵ is a minimum p-faithful run on I such that all its events but the last are silent at p, then the same holds on J, and ↵(I)@p = ↵(J)@p.

Intuitively, transparency implies that the computation as seen from p depends only on what p sees, except for the specific choice of new values. The definition is illustrated by the following example.

Example 5.7. Consider again Example 5.1. It is easy to see that the program in the example is not transparent for Sue. Intuitively, this is because the relation cfoOK carries information that Sue does not see, yet it impacts Sue's view of the workflow. Now consider the following program (obtained by eliminating cfoOK): +Cleared@hr(x) :-+Approved@ceo(x) :-Cleared@ceo(x) +Hire@hr(x) :-Approved@hr(x)

At first glance, the program may now appear to be transparent for Sue. However, this is not the case. Indeed, consider the instances I, J containing the following facts: I: Cleared(Sue); Approved(Sue) J: Cleared(Sue) Clearly, I and J are Sue-fresh since both can be obtained by an application of the Sue-visible event +Cleared@hr(Sue). In addition, I@Sue = J@Sue = {Cleared@Sue(Sue)}. The sequence consisting of the single event +Hire@hr(Sue) :-Approved@hr(Sue) is a minimum Sue-faithful run on instance I. Transparency requires it to also be applicable on J, which is not the case. Intuitively, in order for transparency to hold, Sue-freshness must ensure that pre-existing information invisible to Sue, such as the fact Approved(Sue) in instance I, cannot be used in later events leading to transitions visible by Sue. This can be achieved in various ways. We illustrate one approach, that is also adopted in the design methodology for transparent programs in Section 6. We introduce an additional binary relation Stage visible by all peers, that inhibits the use of any information computed prior to the latest Sue-visible update. Relation Stage is either empty or contains a single tuple Stage(0, s) where s is a value refreshed by peer Sue prior to events by other peers. The invisible relation Approved is extended with an extra column holding the current value of s. The program is the following:

+Stage@Sue(0,s) :-¬ Key Stage@Sue (0) +Cleared@hr(x), Key Stage@Sue (0) :-Stage@hr(0,s) +Approved@ceo(x,s) :-Cleared@ceo(x), Stage@ceo(0,s) +Hire@hr(x), Key Stage@hr (0) :-Approved@hr(x,s), Stage@hr(0,s)

Observe that Stage(0,s) is deleted by each event visible at Sue, which forces its re-initialization with a fresh s before any event using invisible relations can proceed, preventing the use of previous invisible facts. It is easy to check that the program is now transparent for Sue.

We next introduce the boundedness property. Definition 5.8. Let P be a program, p a peer, and h an integer. P is h-bounded for p if for each instance I and sequence ↵ of events applicable to I that yields a minimum p-faithful run at p such that all its events but the last are invisible at p, |↵|  h.

Intuitively, this bounds the number of consecutive events that are silent but relevant to p. Note that the bound applies only to minimum p-faithful subruns. Thus, the other peers are still allowed to carry out arbitrarily long silent computations that do not a↵ect p.

We next consider the decidability of transparency and boundedness. It is easy to show: Theorem 5.9. It is undecidable, given a program P and peer p, (i) whether P is transparent for p, and (ii) whether there exists h such that P is h-bounded for p.

Proof. Straightforward, using (?) in the proof of Theorem 5.4.

On the other hand, as shown next, it is decidable if a program is h-bounded for some given h. Moreover, for programs that are h-bounded, transparency is decidable. In particular, it is decidable whether a program is simultaneously h-bounded and transparent. Indeed, we will see that the two together guarantee the existence of a view program that can be e↵ectively constructed.

We first show that h-boundedness is decidable (see Appendix for proof). Intuitively, this holds because violations of h-boun-dedness are witnessed by minimum p-faithful runs of bounded length, on initial instances of bounded size.

Theorem 5.10. It is decidable in pspace, given a program P , peer p, and integer h, whether P is h-bounded for p.

Next, we show that transparency is decidable for hbounded programs.

Theorem 5.11. The following are decidable in pspace: (i) given a program P that is h-bounded for peer p, whether P is transparent for p, and (ii) given a program P , a peer p and an integer h, whether P is h-bounded and transparent for p.

The proof is provided in the appendix. Clearly, (ii) follows from (i) and Theorem 5.10. The proof of (i) relies on the existence of short counterexamples for violations of transparency by h-bounded programs.

Remark 5.12. Observe that the p-fresh instances used in the definition of transparency need not be reachable in actual runs of P . Thus, the definition has a "uniform" flavor, reminiscent of uniform containment for Datalog. Limiting transparency to reachable instances would yield a much weaker requirement, leading to undecidability of p-transparency even for h-bounded programs.

Previously, we assumed that the boundedness parameter h is given. There are various ways to obtain h. One approach is heuristic: by examining traces of runs, one can "guess" h and then test h-boundedness using Theorem 5.10. Another possibility, briefly considered in Section 6, is to provide syntactic restrictions on the program P that ensure h-boundedness for some h computable from P . Alternatively, we introduce in Section 6 the means of ensuring by design transparency and hboundedness of a program, for a given peer and desired h.

View-programs and provenance. We show that for each program P and peer p such that P is h-bounded and transparent for p, one can construct a view-program of P for p. As discussed earlier, the view program uses peers p and ! (for world). It contains the rules for p, and additional rules for ! that define the side-e↵ects observed by p as a result of actions by other peers. We describe the construction of the rules for !. Intuitively, the rules specify, for each instance I@p visible at p, the possible updates to I@p caused by minimal p-faithful runs of length up to h starting from I. The body of each rule specifies the tuples of I@p causing the update, so intuitively provides the provenance of the update in terms of the data visible at p.

The view program P @p. We outline informally the construction of the view-program of P for p, that we denote P @p.

Let C h+1 = {a 1 , ..., a m }, where C h+1 is the set of constants (polynomial in P ) defined in the proof of Theorem 5.10. For each i 2 [1, m], let x i be a new distinct variable. Let ⌫ be the mapping defined by ⌫(a i ) = x i if a i 6 2 const(P ) and ⌫(a i ) = a i otherwise. Consider a p-fresh instance I and a sequence of events ↵ of P , both over C h+1 , such that the tuples in I(R) use only keys in K(R, ↵) for each relation R, and ↵ is a minimal p-faithful run of P on I in which all events but the last are invisible at p. Let J = ↵(I). Observe that by boundedness of P for p, |↵|  h, and so there are finitely many triples (I, ↵, J) as above. For each such triple (I, ↵, J), the view program P @p contains a rule for peer ! constructed as follows. For each relation R:

• (positive body) for each t in I@p(R), add R@!(⌫(t))

to the body. • (negative body) for each a i in K(R, ↵) that is not a key value in I@p(R), add ¬Key R@! (⌫(a i )) to the body.

• (inequalities) for all a i , a j where i 6 = j, the body contains the inequality ⌫(a i ) 6 = ⌫(a j ). • (head insertions) For each t in J@p(R) I@p(R), add +R@!(⌫(t)) to the head. • (head deletions) For each a i in I@p(Key R@p ) J@p(Key R@p ), add Key R@! (⌫(a i )) to the head. Observe that P @p is a syntactically valid program with schema D@p and peers p and !. We next show that the construction is correct (see Appendix for proof).

Theorem 5.13. Given a program P that is h-bounded and transparent for peer p, the program P @p is a viewprogram of P for p.

Moreover, as suggested in Remark 5.2, the view-program P @p constructed above is sound and complete not only with respect to the linear runs of P as viewed by p, required by the definition, but also with respect to its tree of runs as viewed by p. We omit the formal development.

TRANSPARENT PROGRAM DESIGN

Transparency and h-boundedness for a given peer may be desirable goals for some applications. There are various ways to achieve them. It is of course possible to first design the workflow program and then test it a posteriori for transparency and h-boundedness. However, it may be preferable in practice to specify directly view programs that are transparent and h-bounded by design. We begin the section by showing how this can be done by following some simple design guidelines. We then show that a large class of programs can be transformed so as to make them transparent and h-bounded, by filtering out the runs that violate these properties while preserving the runs that satisfy them (modulo some minor di↵erences).

Before proceeding, we introduce some notions used throughout the section. Consider a run ⇢, and a subsequence e.↵.e 0 of consecutive events of ⇢, of which the only events visible at p are e and e 0 . Then ↵.e 0 is a p-stage. In the following, each non-trivial stage (↵ 6 = ✏) will be equipped with a unique id, in order to identify the facts produced during that stage. Intuitively, transparency is obtained by controlling the provenance of facts produced in that stage that lead to the visible event e 0 . Generating the stage ids can be done using a binary relation Stage, visible by all peers. Stage is either empty or contains a single tuple with key 0. A fact Stage(0, s) indicates that the current stage id is s. When a peer q carries out an event visible at p, it deletes the current fact Stage(0, s) (if such exists). A special rule, that can be performed by any peer q, inserts a new tuple Stage(0, s 0 ) with a fresh value s 0 . Specifically, the rule is +Stage@q(0, z) :-¬ Key Stage@q (0). All rules generating events invisible at p are guarded by an atom Stage(0, x) (so all p-invisible events of the stage are preceded by the event creating a new stage id).

Note that the above assumes that each peer q can tell whether its updates are visible at p. This is not always the case, but holds under certain conditions, such as (C1) further.

Transparency and boundedness by design. We introduce design guidelines to guarantee transparency and h-boundedness for a designated p. It turns out to be rather subtle to guarantee transparency while allowing other peers to perform arbitrary computations that do not impact p.

In order to ensure transparency of a program P for a peer p, we impose the following restrictions on program specifications, to be followed in the design process: (C1) Each peer that sees a relation R visible at p (including p) sees it fully. Formally, for each relation R@p 2 D@p, if R@q 2 D@q then att(R@q) = att(R) and (R@q) = true. (C2) The program maintains the Stage relation as previously described. Note that, because of (C1), every non-trivial update of a relation in D@p, caused by any peer, is also visible at p. Thus, every peer can tell when it performs an update visible at p. As noted previously, this enables the maintenance of relation Stage. (C3) The relations in D are separated in two disjoint classes: p-transparent and p-opaque. The relations that p sees are all p-transparent. The ptransparent relations that p does not see include an attribute, StageID, that contains the id of the stage in which the tuple was created. (C4) If an event modifies some p-transparent relation, (i) only positive facts from p-transparent relations with the current stage id can occur in its body, and (ii) all the updates in the head are either updates of p-visible relations, creations of tuples with new keys in a p-transparent relation, or modifications of tuples in such a relation that have been created during the same stage and are visible by the peer performing the event.

When p is understood, we simply speak of transparent and opaque relations/facts. It is straightforward to specify syntactic criteria to guarantee (C1-C2-C3-C4). For instance, (C4)(ii) can be ensured as follows: if +R@q(x, u) occurs in the head of a rule for a transparent p-invisible relation R, then either x is a variable that does not occur in the body (so it generates a new key) or R@q(x, v) occurs in the body, where v(StageID) is the current stage id provided by relation Stage.

Condition (C1) is natural in many applications where peers are doing some computations about a peer p, for which transparency is desired. For instance, p may be a customer, a job applicant, a participant in a crowdsourcing application, etc. Intuitively, (C1) prevents a peer from unknowingly performing some update that is visible at p.

We briefly elaborate on the motivation of (C4). Clearly, the use of opaque relations in rule bodies may lead to non-transparent computations. The restriction disallowing deletions from p-invisible transparent relations in heads of rules simplifies the presentation, but such deletions could be allowed at the cost of a more complex construction. The following example illustrates the motivation for prohibiting simultaneous updates of transparent and opaque relations in rule heads.

Example 6.1. Consider a workflow program P with a peer p, a p-visible relation R, and a p-invisible opaque relation T . Note that there is no transparent invisible relation. Suppose that P includes the following rules:

+R@q(Sue, hire), +T@q(Sue, hire) :-+R@q(Sue, reject), +T@q(Sue, reject) :-The other peers may have silently computed for an arbitrarily long time, and derived T (Sue, reject). This precludes application of the first rule. Intuitively, they have ruled out a possible future event for Sue without letting her know, thus violating transparency.

It is straightforward to see that a program satisfying (C1-C2-C3-C4) is transparent for p. Note that other peers may perform arbitrary computations as long as they do not a↵ect what p sees. Observe that the transparent program shown in Example 5.7 follows the previous design guidelines.

We next show how to guarantee h-boundedness within a stage ↵.e 0 immediately following an event e. We wish to ensure that the minimum p-faithful subrun of ↵.e 0 contains no more than h events, leading to the activation of the visible event e 0 . This could be easily done by limiting the length of the entire stage to h + 1 using a propositional counter. However, this brute-force solution would be overly restrictive, because one often wishes to allow within the same stage an unbounded number of events that a↵ect only p-opaque relations, or p-transparent relations in events not leading to e 0 .

Achieving this requires a more careful approach, in which the "steps" in each stage are identified by ids consisting of fresh values. More precisely, each event within the stage ↵.e 0 is called a step, and is identified by a step id. We will use the notion of step-provenance of a fact, i.e. the set of step ids in that stage that contribute to deriving the fact. In more detail, we equip each p-transparent relation invisible at p, say Q, with h additional columns B 1 • • • B h that are used to record the step-provenance of each fact in the relation (ids of the steps contributing to its creation). When an update +Q(u, b 1 , ..., b h ) is performed, its set of non-? B i 's is set to the concatenation of all distinct non-? values of the B i 's in the body of the event, augmented with a new id for the current step (shared by all insertions in the head). Recall that by (C4), there is no key deletion from Q. (In some sense, all the facts in Q are logically deleted when a new stage is entered.) Thus, a p-transparent event can be activated only if there is "enough room", i.e., if a sequence of at most h events of the stage are su cient to enable this event. In particular, the last update of the stage has at most h non-? B i 's. The events of the corresponding steps provide a p-equivalent sequence of length at most h, so the minimal p-faithful scenario for that stage has length at most h. Thus, the resulting run is h-bounded for p.

In summary, we can show: Theorem 6.2. Each program obtained using the aforementioned guidelines is transparent and h-bounded for p.

Boundedness by acyclicity. We next show how to guarantee boundedness for a certain class of programs using an acyclicity condition. We consider programs with single updates in heads of rules (which we call linear-head programs), satisfying (C1). For such a program, we define the p-graph of P as follows. Its nodes are the relations in D, and there is an edge (intuitively "depends on") from R to Q if Q is invisible at p and there is a rule at some peer q whose head is +R@q(u) or Key R@q (h) and its body contains Q@q(v) or ¬Key Q@q (k). The program P is p-acyclic if for each R@p 2 D@p, the subgraph of its p-graph induced by the nodes reachable from R is acyclic.

We can show the following (see Appendix for proof). Enforcing transparency and boundedness. We next show, given a program P and peer p, how to rewrite P into a transparent and h-bounded program for p that has essentially the same behaviour as P except that it filters out the runs that are either not transparent or not h-bounded for p. We already defined these properties for programs. We need to define them for runs. Definition 6.4. Let P be a program and p a peer. A run ⇢ of P is transparent for p if for each stage ↵.e 0 of ⇢, the minimum p-faithful subrun ↵ 0 .e 0 of ↵.e 0 has the following property. For any p-fresh instance J such that I@p = J@p, and adom(J) \ new(↵ 0 .e 0 ) = ;, ↵ 0 .e 0 is a minimum p-faithful run on J, all its events but e 0 are silent at p, and ↵ 0 .e 0 (I)@p = ↵ 0 .e 0 (J)@p. We say that ⇢ is h-bounded for p if |↵ 0 .e 0 |  h for every ↵ 0 .e 0 as above. The set of transparent and h-bounded runs of P for p is denoted tRuns p,h (P ).

Our rewriting technique applies to the programs satisfying certain conditions, that we call transparencyform. Unlike the conditions used in the design guidelines, transparency-form does not require separating transparent and opaque relations at the schema level, instead allowing to make a more refined distinction at the fact level. In this more permissive setting, runs are no longer guaranteed to be transparent and h-bounded. However, we show how the violating runs can be filtered out. Definition 6.5. A normal-form program is in transparencyform (TF for short) for p if it satisfies (C1-C2) and: (C3') For each rule of a peer q 6 = p, if its head contains an update +R@q(x, ȳ) for some R that p does not see, either x is a variable that does not appear in the body (key creation) or the body contains an atom R@q(x, z). (C4') For each relation R that p does not see, and each peer q such that R@q 2 D@q, the selection (R@q) uses only attributes in att(R@q).

As discussed earlier, condition (C1) is meant to guarantee that a peer knows when it is performing an event visible at p, which enables maintaining the relation Stage.

(C3') is a natural condition that essentially comes down to preventing the "reuse" of a key after it has been deleted. The motivation for (C4') is more subtle. The presence of a fact in the view of some peer q may depend (because of selections) on some values that q does not see and that have been derived in a non-transparent manner. This may lead to violations of transparency that cannot be filtered out.

We will show the main result of this section for programs satisfying (C1-C2-C3'-C4'). We first need to introduce the notion of "run projection". Definition 6.6. (run projection) Let P be a program over schema D. Let ⇧ be a schema consisting of a subset of the relations in D, each having a subset of its attributes in D (always containing the key). ⇧ induces a projection function on runs, defined as follows. The projection ⇧(⇢) of a run ⇢ of P is obtained from ⇢ by removing facts and updates over relations not in ⇧, projecting out the missing attributes in facts and updates over relations in ⇧, and removing events with resulting empty heads. We say that ⇧ is the identity for peer p if for every run of ⇢ of P , ⇧(⇢)@p = ⇢@p.

We extend this definition to a set Runs of runs and denote the result ⇧(Runs). We now state the main result of the section: Theorem 6.7. Let P be a TF program, p a peer, and h an integer. One can construct a program P t that is transparent and h-bounded for p, and a projection function ⇧ that is the identity for p, such that the runs of P that are transparent and h-bounded for p are exactly the projections of the runs of P t , i.e., tRuns p,h (P ) = ⇧(Runs(P t )).

The construction of the program P t is outlined further. From Theorems 5.13 and 6.7 it also follows that, for an arbitrary TF program P , we can obtain a view program that specifies precisely the views at p of the runs of P that are transparent and h-bounded for p. Corollary 6.8. Let P be a TF program, p a peer, and h an integer. One can construct a view program P t p for P t and p such that Runs(P t p ) = {⇢@p | ⇢ 2 tRuns p,h (P )}.

Remark 6.9. Note that, if the peers attempt to perform a non-transparent computation, the transformed program P t will prevent carrying out the run and the computation may block. In practice, one might want to let the computation proceed and simply send an alert. Alternatively, one might wish to perform some "recovery", e.g., roll back to the state at the beginning of the stage. It is possible to modify P t to implement such an alert or a roll-back.

Program construction. We next outline the construction of the program P t from the given TF program P . Intuitively, we need to identify, in each stage of a run of P , the "transparent facts" that have been obtained in a transparent manner within that stage. Transparent facts can only be created or updated by "transparent events", in which all the facts used in the body are transparent. More precisely, a positive fact is transparent at a particular time within a stage if it is p-visible, or if all events that participate in defining that fact up to that time, within that stage, are transparent. A negative fact is transparent if it concerns a p-visible relation or if its key was transparently created and transparently deleted in the same stage (recall that by (C3') keys cannot be reused after being deleted).

We next enrich the schema of P in order to keep track of the transparent facts. There are some subtleties in the process: (i) a p-invisible tuple may have portions that are transparent and portions that are not, (ii) stepprovenance has to be recorded at the level of attributes rather than of the entire fact, and (iii) the system remembers which are the keys that were created and then deleted transparently during that stage.

The schema is modified as follows. Each relation R of P has a corresponding relation R t in P t . Tuples in R t will use the same keys as in R; intuitively, the tuple of key k of R t will hold information about the tuple of key k in R. For each attribute A of R, R t has an attribute tA. For each q, tA has the same visibility as A, i.e. tA 2 att(R t @q) i↵ A 2 att(R@q). For the key k, besides the attribute tK, the relation R t includes an attribute dK with the same visibility as K. Intuitively, the attribute tA indicates if the value of the corresponding attribute was produced transparently (its value is ?) or not (it has the particular value 1). Each p-visible fact is transparent by definition. The attribute dK is turned to 1 when the tuple is deleted transparently. Finally, for each A 2 att(R), R t has attributes A s 1 , ..., A s h in R t , where A s 1 holds the step id of the event that defined this attribute, and the others provide the step-provenance of that event (the list of step ids that lead to it).

A rule r in R at q is transformed into a set of transparent rules in P t by adding new atoms and updates as follows. For each atom R@q(k, u) in the body, we add an atom R t @q(k, ...) to the body to record extra information for k, and for each atom ¬Key R@q (k), an atom R t @q(k, ...) to the body to record extra information about k, including the fact that the deletion of k was transparent. For each update +R@q(k, u), there exists an update +R t @q(k, ...), and for each update Key R@q (k) an update +R t @q(k, ...). The information included in +R t @q is explained further.

Consider a fact R@q(k, u) in a p-invisible relation. Suppose that the tuple with key k in R t @q satisfies: for each A in att(R@q), the value of tA is ?, the tuple stage (as provided by K s 1 ) is the current stage id, and dK is ?. Then R@q(k, u) holds transparently. Now, consider ¬Key R@q (k) holds. Suppose that the tuple with key k in R t @q satisfies: tK is ?, the tuple stage (as provided by K s 1 ) is the current stage id, and dK is 1. Then ¬Key R@q (k) holds transparently. To detail the use of the A s i attributes, consider the firing of a transparent event and let H be the set of step-IDs occurring in its body augmented with the current step-ID. Then:

• | H | h.

• If the event modifies a non-key attribute A (there is a single step in the minimum p-faithful subrun of a stage that may do that), the set of non-? values in the A s i attributes of the resulting tuple is H. • If the event creates a tuple with a new key, the set of non-? values of the K s i attributes of the created tuple equals H.

• If the event deletes a tuple already recording a set H 0 of step-IDs in its attributes K s i , the values in H H 0 are added in still-available places in the K s i . Note that this imposes that runs can only progress transparently as long as there is enough space available to record h step ids, which guarantees h-boundedness. It is also important to observe that, in transparent events, all updates are e↵ective. This is guaranteed because the program is in TF.

The program also allows non-transparent events. These may come from the use of some non-transparent fact in the body. They may also come from the use of only transparent facts in the body, but such that the number of step ids occurring in them plus one is larger than h. When an event is not transparent, it is not allowed to modify a visible relation; it can only update other relations in an opaque manner.

The program P can be modified to incorporate the above information, allowing to trace transparency status and step ids. All the necessary information can be maintained as outlined above. Each rule of P yields at most exponentially many new rules resulting from a case analysis on the transparency status of the attributes, and the number of steps constributing to their generation.

One can show correctness of the construction, which yields Theorem 6.7 and Corollary 6.8.

RELATED WORK

A survey on data-centric business process management is provided in [START_REF] Hull | Data management perspectives on business process management: tutorial overview[END_REF], and surveys on formal analysis of data centric workflows are presented in [START_REF] Calvanese | Foundations of data-aware process analysis: a database theory perspective[END_REF][START_REF] Deutsch | Automatic verification of database-centric systems[END_REF].

Although not focused explicitly on workflows, Dedalus [START_REF] Alvaro | Dedalus: Datalog in time and space[END_REF][START_REF] Hellerstein | The declarative imperative: experiences and conjectures in distributed logic[END_REF] and Webdamlog [START_REF] Abiteboul | A rule-based language for web data management[END_REF][START_REF] Abiteboul | Viewing the web as a distributed knowledge base[END_REF] are systems supporting distributed data processing based on condition/action rules. Local-as-view approaches are considered in a number of P2P data management systems, e.g., Piazza [START_REF] Tatarinov | The piazza peer data management project[END_REF] that also consider richer mappings to specify views. Update propagation between views is considered in a number of systems, e.g., based on ECA rules in Hyperion [START_REF] Arenas | The hyperion project: from data integration to data coordination[END_REF].

Finite-state workflows with multiple peers have been formalized and extensively studied using communicating finite-state systems (called CFSMs in [START_REF] Parosh | Verifying programs with unreliable channels[END_REF][START_REF] Brand | On communicating finite-state machines[END_REF], and ecompositions in the context of Web services, as surveyed in [START_REF] Hull | Web services composition: A story of models, automata, and logics[END_REF][START_REF] Hull | Tools for composite web services: a short overview[END_REF]). Formal research on infinite-state, datadriven collaborative workflows is still in an early stage. The business artifact model [START_REF] Nigam | Business artifacts: An approach to operational specification[END_REF] has pioneered datadriven workflows, but formal studies have focused on the single-user scenario. Compositions of data-driven web services are studied in [START_REF] Deutsch | Verification of communicating data-driven web services[END_REF], focusing on automatic verification. Active XML [START_REF] Abiteboul | The Active XML project: an overview[END_REF] provides distributed datadriven workflows manipulating XML data. A collaborative system for distributed data sharing geared towards life sciences applications is provided by the Orchestra project [START_REF] Green | Orchestra: facilitating collaborative data sharing[END_REF][START_REF] Ives | The orchestra collaborative data sharing system[END_REF].

Our model is an extension of the collaborative datadriven workflow of [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF]. The results in [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF] focus on the ability of peers to reason about temporal properties of global runs based on their local observations, and are orthogonal to the present investigation. To enable static analysis, the model of [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF] uses more restricted views that those considered here.

Attaching provenance to facts derived in a rule-based language is considered in, e.g., [START_REF] Zaychik Mo Tt | Collaborative access control in Webdamlog[END_REF][START_REF] Abiteboul | A formal study of collaborative access control in distributed datalog[END_REF]. The paper [START_REF] Bourhis | Analyzing data-centric applications: Why, what-if, and how-to[END_REF] studies a notion of explanation in a model of datacentric workflows with a single user, no views, and no abstraction. They consider a notion of explanation that has some similarities to our faithful explanations, but is much simpler. Their results do not apply here.

There has been extensive work on causality and explanations in logic and AI. More specific to data-centric workflows, the relationship between provenance, explanations, and causality is considered in [START_REF] Cheney | Causality and the semantics of provenance[END_REF]. The focus is on provenance of data resulting from complex processes, such as scientific workflows.

The synthesis of view-programs described in Section 5 is related in spirit to partner synthesis in services modeled as Petri Nets [START_REF] Wolf | Does my service have partners? Trans. Petri Nets and Other Models of Concurrency[END_REF][START_REF] Lohmann | Wendy: A tool to synthesize partners for services[END_REF][START_REF] Sürmeli | Synthesizing cost-minimal partners for services[END_REF].

The issue of transparency of algorithms is gaining increased attention, see e.g., the Data Transparency Lab (datatransparencylab.org/) in the US, and the Transalgo Lab starting in France. Data transparency has been studied in di↵erent contexts. For instance, the causality of machine-learning-based decisions is studied in [START_REF] Datta | Algorithmic transparency via quantitative input influence: Theory and experiments with learning systems[END_REF].

Workflow transparency sometimes refers to the ability of considering a business process independently of the workflow implementing it, an aspect not considered here. Data transparency has also been considered in the context of workflows in [START_REF] Wolter | Collaborative workflow management for egovernment[END_REF], where an architecture for providing transparency in human-centric eGovernment workflows is proposed.

CONCLUSION

In this paper, we formally studied the problem of providing explanations of data-driven collaborative workflows to peers participating in the workflows, exploring semantic and computational issues.

We identified faithful scenarios for a peer p as a particularly appealing basis for explanations from a semantic viewpoint. In a first contribution, we show that faithful scenarios form a semiring with respect to union and intersection, implying the existence of a unique minimal faithful scenario for each peer, computable in polynomial time, and enabling incremental maintenance of scenarios. In a second contribution, we identified desirable properties of workflows, namely transparency and boundedness, that guarantee the existence of a view program for a peer p, and showed how such a program can be constructed.

Finally, we studied how programs satisfying transparency and h-boundedness for some peer p can be designed. We also show how, under certain restrictions, runs violating transparency or h-boundedness can be filtered out. A remaining open question is whether it is possible to perform such a filtering for arbitrary workflows.

It is possible to implement workflow programs by relying on a master server that has access to all the information, receives the updates, propagates them to appropriate peers, and controls transparency and boundedness for certain peers. Blockchain technology provides an alternative to such a central authority. It is, in spirit, an excellent match with collaborative workflows. A blockchain-based implementation of collaborative workflows is therefore a promising research direction with challenging technical issues, notably with respect to performance and access control. hold for the valuation mapping all variables to true. Let R be a relation of arity n + 2, with key K, attributes A x for each x 2 X, and a last attribute A q . For each variable x 2 X, there is a peer p

x that sees the projection of R over K, A

x . There is a peer q that sees K, A q . In addition, there is a peer p that sees the projection of R on K with the selection p = (A q = 1) ^( _ ' ) where = ^x2X (A x = 1), and ' checks that the formula ' is true for the valuation ⌫ of X such that ⌫(x) = true i↵ A

x = 1. The program consists of all ground rules of the form r xi : +R@p xi (0, 1) :-(for each x i 2 X) e :

+R@q(0, 1) :-Consider the run ⇢ consisting of r x1 . . . r xn e. Observe that p sees R@p(0) only after the last event, because of the condition A q = 1 in its selection condition on R. We prove that ' is not satisfiable i↵ ⇢ is a minimal scenario of ⇢ at p. First suppose that ' is satisfiable. Let ⌫ be a valuation satisfying '. Consider the subsequence of r xi 1 . . . r

xi k e obtained by keeping only the events r xi j such that ⌫(x ij ) is true. By (*), it is shorter than the original sequence. Let ⇢ ⌫ be the corresponding run. It is easy to see that ⇢ ⌫ is a strict subrun of ⇢ and that ⇢ ⌫ @p = ⇢@p. Thus ⇢ is not minimal at p. Now suppose that ' is not satisfiable. Let ⇢ 0 be a scenario of ⇢ at p. Because ' is not satisfiable, ' can never be satisfied, so in order for p to see R@p(0), it is necessary that hold, so ⇢ 0 must contain all events in ⇢. Thus, ⇢ is minimal.

Proof of Lemma 4.6 Let ⇢ = {(e i , I i )} 0in and ↵ = {e ij } 0jm . We prove by induction on h (0  h  m) that ( †) ↵| h = {e ij } 0jh yields a subrun {(e ij , I 0 j )} 0jh of ⇢ and I 0 h @p = I i h @p. Suppose ( †) holds. Then ↵ yields a subrun of ⇢, establishing (i). Additionally, I 0 j @p = I ij @p for 0  j  m. This together with the fact that ↵ includes all events in ⇢ visible at p implies that run(↵)@p = ⇢@p. Thus, run(↵) is a scenario of ⇢ for p, establishing (ii)

We now prove ( †). For the basis, let h = 0. We need to show that (a) e i0 is applicable to the empty instance and (b) I 0 0 @p = I i0 @p. For (a), suppose the body of e i0 contains a literal R@q(k, u). Then i 0 belongs to an Rlifecycle of k in ⇢, whose left boundary must be included in ↵, a contradiction. Thus the body of e i0 contains no literal of the form R@q(k, u) and is applicable to the empty instance, proving (a). Now consider (b). Consider t 2 I 0 0 @p(R@p) with key k. Then e i0 must insert in R a tuple t 0 with the same key, such that t 0 @p = t. Thus, i 0 belongs to the R-lifecycle of k in ⇢, and in fact it must be its left boundary (otherwise, by boundary faithfulness, e i0 must be preceded by another event in ↵, a contradiction). It follows that I 0 0 and I i0 both contain t 0 , so t 2 I i0 @p(R@p). Thus, I 0 0 @p ✓ I i0 @p. Conversely, let t 2 I i0 @p(R@p) with key k. Let h 0 (h 0  i 0 ) be the minimum in the same R-lifecycle of k in ⇢, for which a tuple with key k is visible by p in I h 0 @p(R@p).

It follows that e h 0 is visible at p so it is included in ↵, so h 0 = i 0 and e i0 must insert a tuple t 0 with key k. Moreover, i 0 must also be the left boundary of the Rlifecycle of k (or else, that left boundary would have to be included in ↵ prior to e i0 ). It follows that t 0 @p = t. Thus, t 2 I 0 0 (R@p), and I i0 ✓ I 0 0 . This completes the basis.

For the induction step, suppose {e ij } 0jh yields a subrun {(e ij , I 0 j )} 0jh of ⇢ where I 0 h @p = I i h @p, for h < m, and consider e i h+1 . For (a), we need to show that e i h+1 is applicable in I 0 h . Let R@q(k, u) occur in the body of e i h+1 . Then i h belongs to an R-lifecycle of k in ⇢, and, by modification faithfulness, all prior events of the Rlifecycle that a↵ect attributes in att(R, q) of tuples with key k are included in ↵. It follows that I 0 h (R) and I i h (R) both contain tuples with key k, that agree on att(R, q). Thus, since R@q(k, u) holds in I i h , it also holds in I 0 h . Next, suppose ¬Key R @q(k) occurs in the body of e i h+1 . Suppose k 2 I i h (Key R ). Then, similarly to the previous case, I 0 h (R) and I i h (R) both contain tuples with key k, that agree on att(R, q), so ¬Key R @q(k) holds in I 0 h . Now suppose that k 6 2 I i h (Key R ) but k 2 I 0 h (Key R ). Let v < h be the left boundary of the R-lifecycle in run(↵| h ) to which h belongs. It follows that i v belongs to an R-lifecycle of k in ⇢ but i h does not, so the Rlifecycle has a right boundary in ⇢ occurring before i h , which by boundary faithfulness must also belong to ↵. This contradicts the fact that h is in an R-lifecyle of k in run(↵| h ). So, k 6 2 I 0 h (Key R ) and ¬Key R @q(k) holds in I 0 h . In summary, e i h+1 is applicable in I 0 h . Now consider (b). Let t 2 I 0 h+1 @p(R@p) where t has key k. Thus, I 0 h+1 (R) contains a tuple t 0 with key k such that t 0 @p = t. From boundary and modification faithfulness it easily follows that I i h+1 (R) contains a tuple t 00 with key k that agrees with t 0 on att(R, p), so t 00 @p = t 0 @p = t and t 2 I i h+1 @p(R@p). Thus, I 0 h+1 @p ✓ I i h+1 @p. Conversely, let t 2 I i h+1 @p(R@p) with key k. Similarly to the base case, let h 0 be the minimum in the same R-lifecycle of k in ⇢, for which a tuple with key k is visible by p in I h 0 @p(R@p). It follows that e h 0 is visible at p so is included in ↵. Clearly, e h 0 must contain an insertion of a tuple with key k into R.

From boundary and modification faithfulness it follows that I i h+1 (R) and I 0 h+1 (R) contain tuples with key k that agree on att(R, p), so t 2 I 0 h+1 @p(R@p). Thus, I i h+1 @p ✓ I 0 h+1 @p. This completes the induction and the proof of ( †). 2

Example 4 . 1 .

 41 Consider again the worlflow used in the proof of Theorem 3.3. Suppose that p also sees the propositions

Definition 4 . 3 .

 43 Let ⇢ = {(e i , I i )} 0in be a run of some workflow program P . A subsequence ↵ = {e ij } 0jm of e(⇢) is boundary faithful if for every e ij and k 2 K(R, e ij ) such that i j belongs to an R-lifecycle 1 of k in ⇢, the left boundary event of the R-lifecycle belongs to ↵, and the right boundary event of the R-lifecycle also belongs to ↵, if the R-lifecycle is closed.

Definition 4 . 5 .

 45 A subsequence ↵ of e(⇢) is p-faithful if it contains all events of ⇢ that are visible at p, is boundary faithful, and modification faithful for p. A subrun b ⇢ of ⇢ is p-faithful if e(b ⇢) is p-faithful.

Theorem 6 . 3 .

 63 Let P be a linear-head program over schema D satisfying (C1). Let b be the maximum number of facts in a rule body of P , d = |D|, and a the maximum arity of a relation in D plus one. If P is pacyclic then it is h-bounded for p, where h = (ab + 1) d .

  R a new tuple with key k, this tuple is not deleted between i 1 and i 2 , and e i2 deletes it. An open R-lifecycle of k in ⇢ is an interval [i 1 , 1) such that e i1 inserts in R a new tuple with key k and this tuple is not deleted later on in ⇢. In both cases, we say that e i1 is the left boundary event of the lifecycle, and we say that e i2 is the right boundary event of the closed lifecycle [i 1 , i 2 ].

Observe that k

K(R, ei j ) need not belong to an Rlifecycle containing ij, because k may occur in a negative literal ¬Key R@q (k).

Acknowledgment.

Serge Abiteboul and Pierre Bourhis are supported by the ANR Project Headwork, ANR-16-CE23-0015, 2016-2021. Victor Vianu is supported in part by the National Science Foundation under award IIS-1422375.

APPENDIX A. APPENDIX

We provide proof outlines for several results of the paper.

Proof of Theorem 3.4 Membership in coNP is immediate. For hardness, we reduce the problem of testing unsatisfiability of a Boolean formula to testing whether a scenario for some peer p is minimal. Let ' be a formula over some set X = {x 1 , ..., x n } of variables. We assume without loss of generality that (*) ' does not Proof of Theorem 4.8 We first note the following useful fact, that follows immediately from the definition of T p (⇢, •). Lemma A.1. The operator T p (⇢, •) is additive: for all subsequences ↵ 1 , ↵ 2 of e(⇢), T p (⇢, ↵ 1 +↵ 2 ) = T p (⇢, ↵ 1 )+ T p (⇢, ↵ 2 ). We now turn to the proof of the theorem. Let ⇢ 1 an ⇢ 2 be p-faithful scenarios of ⇢. Consider first e(⇢ 1 ) + e(⇢ 2 ). By definition, e(⇢ 1 ) + e(⇢ 2 ) contains all events of ⇢ visible at p. By additivity of T p (⇢, •), T p (⇢, e(⇢ 1 ) + e(⇢ 2 )) = T p (⇢, e(⇢ 1 )) + T p (⇢, e(⇢ 2 )) = e(⇢ 1 ) + e(⇢ 2 ). Thus, e(⇢ 1 ) + e(⇢ 2 ) is also a fixed-point of T p (⇢, •) and so it is a p-faithful scenario of ⇢.

Now consider e(⇢ 1 ) ⇤ e(⇢ 2 ). Since ⇢ 1 and ⇢ 2 are pfaithful scenarios, e(⇢ 1 ) and e(⇢ 2 ) are fixed-points of T p (⇢, •) and contain all events of ⇢ visible at p. Since e(⇢ 1 ) ⇤ e(⇢ 2 ) ⌧ e(⇢ 1 ) and e(⇢ 1 ) ⇤ e(⇢ 2 ) ⌧ e(⇢ 2 ), it follows that T ! p (⇢, e(⇢ 1 ) ⇤ e(⇢ 2 )) ⌧ e(⇢ 1 ) and T ! p (⇢, e(⇢ 1 ) ⇤ e(⇢ 2 )) ⌧ e(⇢ 2 ), so

. Since e(⇢ 1 ) ⇤ e(⇢ 2 ) also contains all events visible at p, by Lemma 4.6, e(⇢ 1 ) ⇤ e(⇢ 2 ) yields a p-faithful scenario of ⇢.

Finally, observe that multiplication distributes over addition, ✏ is the additive identity and ⇢ the multiplicative identity. 2

Proof of Theorem 5.10 We begin with two technical lemmas. The first essentially says that various properties of sequences of events are invariant under isomorphism.

Lemma A.2. Let I be an instance and ↵ = e 1 . . . e n a sequence of events applicable at I. Let f be a bijection on dom that is the identity on const(P ). We denote by f (↵) the sequence of events obtained by applying f to every value occurring in ↵. Then the following hold:

(minimum) p-faithful run on f (I), and the events visible at p are the same in the two runs.

Proof. Straightforward induction on the length of ↵.

We also need the following. Recall that, for each relation R, K(R, ↵) denotes the set of values occurring as keys of relation R in some event of ↵. For an instance I, we denote by I|K(↵) the instance retaining, for each relation R, only the tuples in I(R) with keys in K(R, ↵).

Lemma A.3. Let I be an instance, ↵ a sequence of events, and I|K(↵) ✓ J ✓ I. The following hold: (i) if ↵ is a (minimum) p-faithful run on I then it is also a (minimum) p-faithful run on J, and the events visible at p are the same in the two runs. (ii) if ↵ is a (minimum) p-faithful run on J such that adom(I) \ new(↵) = ; then ↵ is also a (minimum) p-faithful run on I, and the events visible at p are the same in the two runs.

Proof. Also by induction on the length of ↵. The only subtlety concerns new values. For (i), note that, if an event of ↵ creates a new value on I, that value is also new in the run on J, since J ✓ I. For (ii), the converse holds because adom(I) \ new(↵) = ; ensuring that the new values created in ↵ do not occur in I.

We can now prove Theorem 5.10. By definition, P is not h-bounded i↵ ( ‡) there is an instance I and sequence ↵ of events, of length h + 1, that yields a minimim p-faithful run on initial instance I, such that all of its events but the last are silent at p. Let c m be the maximum number of values occurring in a sequence ↵ of events of length at most m and an instance I such that the tuples in I(R) use only keys in K(R, ↵) for each relation R. Let cm = |const(P )| + c m and C m consist of const(P ) together with c m additional distinct constants (so |C m | = cm ). By Lemmas A.2 and A.3 (i), it is sucient to check ( ‡) for sequences ↵ of events of length at most h + 1 and instances I, both using only values in C h+1 . This establishes decidability. The pspace upper bound follows from the fact that ch+1 is polynomial in h and P , which yields a non-deterministic pspace test. This completes the proof. 2

Proof of Theorem 5.11 Clearly, (ii) follows from (i) and Theorem 5.10. Consider (i). Let P be a program that is h-bounded for p. By a slight reformulation of the definition of transparency, P is transparent for p i↵ the following holds.

( †) For all instances I 1 , I 2 and events e 1 , e 2 such that e i is applicable at I i and visible at p (i = 1, 2) and e 1 (I 1 )@p = e 2 (I 2 )@p, and for each sequence ↵ of events such that adom(e 2 (I 2 )) \ new(↵) = ;, if ↵ is a minimum p-faithful run on e 1 (I 1 ) such that all its events but the last are silent at p, then the same holds on e 2 (I 2 ), and ↵(e 1 (I 1 ))@p = ↵(e 2 (I 2 ))@p. We show that ( † 0 ): ( †) holds i↵ it holds for all instances I 0 1 , I 0 2 such that, for each relation R, I 0 i (R) contains at most c|↵|+2 tuples. For suppose this holds. Since P is h-bounded, it is su cient to check ( †) for instances I 1 and I 2 with at most ch+2 tuples in each relation. The existence of counterexamples can be easily checked by a nondeterministic pspace algorithm. This completes the proof.

We now show ( † 0 ). The "only if" part is trivial. Consider the "if" part. Suppose ( †) holds for all instances I 0 1 , I 0 2 such that, for each relation R, I 0 i (R) contains at most c|↵|+2 tuples. Let I 1 , I 2 be arbitrary instances, e 1 , e 2 events such that e i is applicable at I i and visible at p (i = 1, 2), e 1 (I 1 )@p = e 2 (I 2 )@p, ↵ is a minimum p-faithful run on e 1 (I 1 ) such that all but its last event are silent at p, and adom(e 2 (I 2 )) \ new(↵) = ;.

We can assume without loss of generality that adom(I 2 )\ new(↵) = ;; otherwise, we can rename the values in I 2 and e 2 that occur in the intersection by a bijection that is the identity on const(P

1 and I 0 2 contains at most c|↵|+2 tuples. We next show that I 0 1 , I 0 2 satisfy the conditions of ( †).

By Lemma A.3 (i), e i is applicable to I 0 i and is visible at p (i = 1, 2). Moreover, ↵ is a minimum pfaithful run on e 1 (I 0 1 ) and all but its last event are silent at p. We show that e 1 (I 0 1 )@p = e 2 (I 0 2 )@p. Let t 2 e 1 (I 0 1 )@p(R@p) with key k for some R. Observe that k 2 K 1,2 . Since e 1 (I 0 1 ) ✓ e 1 (I 1 ) and e 1 (I 1 )@p = e 2 (I 2 )@p, t 2 e 2 (I 2 )@p(R@p) and there is t 0 2 e 2 (I 2 )(R), with the same key k as t, such that t = t 0 @p. Suppose there is no tuple with key k in I 2 , so t 0 is created by e 2 . Then t 0 is also in e 2 (I 0

2 ) and t 2 e 2 (I 0 2 )@p(R@p). Now suppose there is a tuple t 00 with key k in I 2 (R). Since k 2 K 1,2 , t 00 2 I 0 2 (R) and so t 0 2 e 2 (I 0 2 )(R) and t 2 e 2 (I 0

2 )@p(R@p). We have shown that e 1 (I 0 1 )@p ✓ e 2 (I 0

2 )@p. The converse holds by symmetry, so e 1 (I 0 1 )@p = e 2 (I 0

2 )@p. Also, adom(e 2 (I 0 2 )) \ new(↵) = ;. Since I 0 1 and I 0 2 satisfy the condition of ( †), it follows that ↵ is a minimum p-faithful run on e 2 (I 0

2 ) such that all but its last event are silent at p, and ↵(e 1 (I 0 1 ))@p = ↵(e 2 (I 0

2 ))@p. By Lemma A.3 (ii), ↵ is also a minimum p-faithful run on e 2 (I 2 ) such that all but its last event are silent at p.

It remains to show that ↵(e 1 (I 1 ))@p = ↵(e 2 (I 2 ))@p. Let t 2 ↵(e 1 (I 1 ))@p(R@p) with key k for some R. Thus, there exists a tuple t 0 2 ↵(e 1 (I 1 ))(R), with key k, such that t = t 0 @p. First suppose k 6 2 K 1,2 , then t 0 also belongs to e 1 (I 1 ). Since e 1 (I 1 )@p = e 2 (I 2 )@p, t 2 e 2 (I 2 )@p(R@p). Thus, there is t 00 2 e 2 (I 2 )(R) with key k, such that t 00 @p = t. Since k 6 2 K 1,2 , ↵ does not a↵ect t 00 , so t 00 2 ↵(e 2 (I 2 ))(R) and t 2 ↵(e 2 (I 2 ))@p(R@p). Now suppose k 2 K 1,2 . If there is no tuple in e 1 (I 1 )(R) with key k, then ↵ creates t 0 on any initial instance on which it is applicable, so t 0 2 ↵(e 2 (I 2 ))(R) and t 2 ↵(e 2 (I 2 ))@p(R@p). Suppose there is a tuple t 00 in e 1 (I 1 )(R) with key k. Since k 2 K 1,2 , t 00 2 e 1 (I 0 1 )(R). It follows that t 0 2 ↵(e 1 (I 0 1 ))(R) and t 2 ↵(e 1 (I 0 1 ))@p(R@p). Since ↵(e 1 (I 0 1 ))@p = ↵(e 2 (I 0 2 ))@p, t 2 ↵(e 2 (I 0

2 ))@p. Since ↵ is applicable to e 2 (I 2 ) and I 0 2 ✓ I 2 , it follows that ↵(e 2 (I 0 2 ))@p ✓ ↵(e 2 (I 2 ))@p, and t 2 ↵(e 2 (I 2 ))@p(R@p). In both cases, t 2 ↵(e 2 (I 2 ))@p(R@p), thus, ↵(e 1 (I 1 ))@p ✓ ↵(e 2 (I 2 ))@p. The converse holds by symmetry. Hence, ↵(e 1 (I 1 ))@p = ↵(e 2 (I 2 ))@p, which concludes the proof. 2

Proof of Theorem 5. [START_REF] Datta | Algorithmic transparency via quantitative input influence: Theory and experiments with learning systems[END_REF] We need to show that P @p is sound and complete for P and p.

Consider completeness. For runs ⇢ of P and ⇢ 0 of P @p, we denote by ⇢@p ⇠ ⇢ 0 that fact that ⇢@p is obtained from ⇢ 0 by replacing all !-events with !. Let ⇢ = {(e i , I i )} 0in be a run of P . We can write e(⇢) as ↵ 1 .e i1 .↵ 2 .e i2 . . . ↵ n .e in .↵ n+1 where e ij are the events visible at p (1  j  n) and ↵ j are sequences of events invisible at p (1  j  n + 1). We define a sequence of events E 1 . . . E n yielding a run of P @p, such that

Consider a fixed j > 1 for which e ij is not en event of p (the case j = 1 is a straightforward variation). Let e = e ij , e 0 = e i (j 1) , ↵ = ↵ j , I = I i (j 1) , I 0 = I i (j 1) 1 , and J = I ij . Let ↵ be the subsequence of ↵ such that ↵.e is the unique minimum p-faithful subrun of ↵.e on initial instance I. Since P is h-bounded for p, | ↵.e|  h. Let Ī = I|K(e 0 . ↵.e). By Lemma A.3 (i), ↵.e is a minimum p-faithful run of P on Ī, all events of ↵ are invisible at p, and e is visible at p. Also, Ī is a p-fresh instance, since it is easily seen that Ī = e 0 (I 0 |K(e 0 .↵.e)) and e 0 is visible at p. Let J = ↵.e( Ī). Observe that | Ī|  c h+1 . By Lemma A.2 we can assume without loss of generality that Ī and ↵.e use only constants in C h+1 . Consider the rule of P @p corresponding to the triple ( Ī, ↵.e, J). Consider the event E j obtained by applying to the variables of the rule the valuation ⌫ 1 . Clearly, the event is applicable to Ī@p and E j ( Ī@p) = J@p. It remains to show that E j (I@p) = J@p. Let Īc = I Ī. By definition, Īc contains no tuple a↵ected by ↵.e, so J = J [ Īc . Similarly, no tuple of Īc @p is a↵ected by E j . It follows that E j (I@p) = E j ( Ī@p) [ Īc @p = J@p [ Īc @p = J@p. This establishes completeness of P @p. Now consider the soundness of P @p. Let ⇢ p = {(E i , I i )} 0in be a run of P @p. We show that there exists a run ⇢ of

We prove the statement by induction on j. Consider j = 0. Thus, E 0 (;) = I 0 . If E 0 is an event of p then the statment holds. Otherwise, by definition, there exists a p-fresh instance I and a minimum p-faithful run ↵.e of P on I, such that the tuples in I(R) use keys in K(R, ↵) for each relation R, and ↵.e(I)@p = E 0 (I@p). By construction, since E 0 has no positive atoms in its body, I@p = ;. By transparency of P , ↵.e is also a minimum p-faithful run of P on ; in which all events but e are invisible at p, and ↵.e(;)@p = ↵.e(I)@p = E 0 (;). This completes the base of the induction.

For the induction step, let 0 < j < n suppose there is a run ⇢ j of P such that ⇢ j @p ⇠ ⇢ p | j . Let e(⇢ j ) = ↵ j and ↵ j (;) = J. So J is a p-fresh instance and J@p = I j . From the definiton of E j+1 , it can be shown similarly to the base case that there exists a p-fresh instance I over D, and a minimum p-faithful run ↵.e of P on initial instance I, in which all events but e are invisible at p, such that I@p = I j and ↵.e(I)@p = I j+1 . We would like to obtain a run corresponding to ⇢ p | j+1 by concatenating ↵ j with ↵.e. However, it could be that new(↵.e) \ adom(↵ j ) 6 = ;. Observe that new(↵.e) \ adom(I j ) = ; since adom(I j ) ✓ adom(I). Thus, there are two cases to handle:

(i) new(↵.e) contains values in adom(⇢ p | j 1 ), (ii) new(↵.e) contains values in adom(↵ j ) adom(⇢ p | j 1 ) Case (i) can be handled by applying to ↵.e a bijection f on dom that is the identity on const(P ) [ adom(I) [ adom(I j+1 ) and such that adom(f (new(↵.e)))\adom(⇢ p | j 1 ) = ;, and using Lemma A.2. Case (ii) can then be avoided by applying to ↵ j a bijection g on dom that is the identity on const(P )[adom(⇢ p | j ) and such that adom(g(↵ j ))\ new(↵.e) = ;, and using again Lemma A.2.

Thus, we can assume that new(↵.e) \ adom(↵ j ) = ;. By transparency of P , since I and J are p-fresh, I@p = J@p, and adom(J) \ new(↵.e) = ;, it follows that ↵.e is a run of P on J and ↵.e(J)@p = ↵.e(I)@p = I j+1 . Thus, ↵ j .↵.e yields a run of P and run(↵ j .↵.e) ⇠ ⇢ p | j+1 . This completes the induction and the proof of soundness of P @p. 2 Proof of Theorem 6.3 Consider an instance I and a sequence ↵.e of events applicable to I that yields a minimum p-faithful run at p, such that all its events but e are invisible at p. Observe that no event of ↵ has a relation visible at p in the head. Since ↵.e is a minimum p-faithful run, ↵.e = T ! p (↵.e, e). Let R be the relation occurring in the head of e. Since e is visible at p, R@p 2 D@p. It can be shown that T ! p (↵.e, e) = T g p (↵.e, e), where g is the maximum length of a path in the p-graph of P , starting from relation R. Intuitively, this is because every productive application of T p (↵.e, •) to an event corresponds to traversing at least one edge in the p-graph (from the relation in the head to some in the body). It follows that T p (↵.e, e) can only be applied g times before converging. Moreover, given a set E of events, T p (↵.e, E) adds to E at most b • |E| lifecycles of keys, each containing at most a events. It follows that |↵.e|  (ab + 1) g  (ab + 1) d . 2

Proof of Theorem 6.7 (sketch) Let P be a TF program, p a peer, and h an integer. Let P t be the program constructed from P as previously described. We show that (*) P t is transparent and h-bounded for p, and (**) each run of P that is transparent and h-bounded for p is the projection of a run of P t . Towards (*), consider a p-fresh instance I and a minimal p-faithful sequence ↵ of events of P t such that only the last one is visible for p. Transparency is satisfied by construction. For h-boundedness, observe that the subrun consisting of the events corresponding to the stepIDs occurring in the B i attributes of the last event of ↵ is observationally equivalent to ↵ for p. Therefore h-boundedness holds as well.

Towards (**), first observe that the projection simply removes from the runs of P t , the relations R t for each R. Consider a transparent and h-bounded run ⇢ of P . Let its stages be ↵ i for i 2 [1.

.n], and I i be the instance reached after ↵ i for each i. We construct a corresponding run ⇢ 0 of P t . For this, for each i, consider the minimal faithful subrun ↵ 0 i of ↵ i on input I i 1 . It is transparent and, by h-boundedness, its length is less or equal to h. We can therefore extend the events of P to transparent events of P t to capture the events in ↵ 0 i . Because its length is less that h, we dispose of enough space in the B i . For the other events, it is irrelevant whether we extend them using transparent or non transparent events. We thus obtain a run ⇢ 0 such that ⇢ = ⇧(⇢ 0 ), which concludes the proof. 2