Serge Abiteboul

A Comparing Workflow Specification Languages: A Matter of Views

Keywords: H, 2, 3 [Database Management]: Data Manipulation Languages; H, 4, 1 [Information Systems Applications]: Office Automation-Workflow Management

We address the problem of comparing the expressiveness of workflow specification formalisms using a notion of view of a workflow. Views allow to compare widely different workflow systems by mapping them to a common representation capturing the observables relevant to the comparison. Using this framework, we compare the expressiveness of several workflow specification mechanisms, including automata, temporal constraints, and pre-and post-conditions, with XML and relational databases as underlying data models. One surprising result shows the considerable power of static constraints to simulate apparently much richer workflow control mechanisms.

INTRODUCTION

There has recently been a proliferation of workflow specification languages, notably data-centric, in response to the need to support increasingly ubiquitous processes centered around databases. Prominent examples include e-commerce systems, enterprise business processes, health-care and scientific workflows. Comparing workflow specification languages is intrinsically difficult because of the diversity of formalisms and the lack of a standard yardstick for expressiveness. In this paper, we develop a flexible framework for comparing workflow specification languages, in which the pertinent aspects to be taken into account are defined by views. We use it to compare the expressiveness of several workflow specification mechanisms based on automata, pre/post conditions, and temporal constraints.

Consider a system that evolves in time as a result of internal computations or interactions with the rest of the world. Fundamentally, a workflow specification imposes constraints on this evolution. There are numerous approaches for specifying such constraints. Perhaps the most popular consists of specifying a set of abstract states of the system and imposing state transition constraints, in the spirit of a BPEL program [BPEL ]. Another, more declarative approach is to define a set of tasks equipped with pre/post conditions, such as IBM's Business Artifact model (see Related Work). Artifact systems may also impose constraints by temporal formulas on the history of the run ( [Hull 2009]).

The richness and variety of these approaches renders their comparison difficult. In particular, little is known of their relative expressive power. This is the main focus of the present paper.

We argue that a very useful approach for comparing workflow specification languages is provided by the notion of workflow view. More broadly, the notion of view is essential in the context of workflows, and the need to provide different views of workflows is pervasive. For example, views can be used to explain a workflow or provide customized interfaces for different classes of stakeholders, for convenience or privacy considerations. The interaction of workflows and contractual obligations are also conveniently specified by views. The design of complex workflows naturally proceeds by refinement of abstracted views. Views can be used at runtime for surveillance, error detection, diagnosis, or to capture continuous query subscriptions. The abstraction mechanism provided by views is also essential in static analysis and verification.

Depending on the specific needs, a workflow view might retain information about some abstract state of the system and its evolution, about some particular events and their sequencing, about the entire history of the system so far, or a combination of these and other aspects. Even if not made explicit, a view is often the starting point in the design of workflow specifications. This further motivates using views to bridge the gap between different specification languages. To see how this might be done, consider a workflow W specified by tasks and pre/post conditions and another Although presented here in the context of BAXML, these extensions capture the essential aspects of the three specification paradigms regardless of the specific underlying data model.

Our main results concern the relative power of BAXML and its extensions as workflow specification languages. When we insist that they generate exactly the same runs, the three extensions turn out to be incomparable. More interestingly, we then consider a more permissive and realistic notion of equivalence in which a view allows to hide portions of the data and some of the functions, thus providing more leeway in simulating one workflow by another. Surprisingly, we show that the core BAXML alone is largely capable to simulate the three specification mechanisms based on guards, automata, and temporal properties. This indicates the considerable power of static constraints to simulate apparently much richer workflow control mechanisms. Of course, specifications using guards, automata, and temporal properties are typically much more readable than their equivalent specifications in BAXML using hidden functions and static constraints.

The above results show the usefulness of seeing a workflow abstractly as a constraint on the runs of an underlying system, decoupled from the specific approach for defining the constraint. It also demonstrates the effectiveness of views in comparing workflows and worklow specification languages. Although the above languages are formalized in a specific Active XML context, we believe that the results demonstrate the wide applicability of the approach beyond this particular setting. In particular, the proofs provide general insight into when and how specifications based on automata, guards, and temporal constraints can simulate each other.

After settling the relative expressiveness of the languages using BAXML as a common core, we finally consider IBM's business artifact model, which uses a different paradigm based on the relational model and services equipped with first-order pre/post conditions. Relying once again on the views framework, we compare BAXML to the business artifact model, as formalized in [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]. We prove that BAXML can simulate artifacts, but the converse is false. The first result uses views mapping XML to relations and functions to services, so that artifacts become views of BAXML systems. For the negative result we use views retaining just the trace of function and service calls from the BAXML and the artifact system. This is a powerful result, since it extends to any views exposing more information than the function/service traces. The latter results demonstrate once again the flexibility and power of the views approach to comparing workflows.

Related work

Workflow modeling and specification has traditionally been process centric (e.g., [START_REF] Georgakopoulos | An overview of workflow management: From process modeling to workflow infrastructure management[END_REF][START_REF] Van Der Aalst | Business process management demystified: A tutorial on models, systems and standards for workflow management[END_REF]). This has been captured in the workflows community by flowcharts, Petri nets [START_REF] Van Der Aalst | The application of petri nets to workflow management[END_REF][START_REF] Van Der Aalst | Workflow patterns: On the expressive power of (petri-net-based) workflow languages[END_REF][START_REF] Adam | Modeling and analysis of workflows using Petri nets[END_REF]], and state charts [START_REF] Harel | Statecharts: A visual formulation for complex systems[END_REF][START_REF] Mok | Using Harel's statecharts to model business workflows[END_REF]. The comparison of such systems using the notion of bisimulation is considered in [START_REF] Milner | Communication and concurrency[END_REF][START_REF] Van Benthem | Modal correspondence theory[END_REF]. More recently, data-centric workflows have been considered in [START_REF] Wang | A framework for document-driven workflow systems[END_REF], and in particular the artifact model of IBM [START_REF] Nigam | Business artifacts: An approach to operational specification[END_REF]. Verification for such models is considered in [Gerede et al. 2007;Gerede and Su 2007;[START_REF] Bhattacharya | Towards formal analysis of artifact-centric business process models[END_REF][START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF][START_REF] Fritz | Automatic construction of simple artifact-based business processes[END_REF]]. The comparison of such systems is considered in [START_REF] Calvanese | Artifact-centric workflow dominance[END_REF]] using the notion of dominance, which focuses on the input/output pairs of the workflows. Other models in the same spirit include the Vortex workflow framework [START_REF] Hull | Declarative workflows that support easy modification and dynamic browsing[END_REF][START_REF] Dong | A framework for optimizing distributed workflow executions[END_REF][START_REF] Hull | Optimization techniques for data-intensive decision flows[END_REF]], the OWL-S proposal [START_REF] Mcilraith | Semantic web services[END_REF][START_REF] Martin | OWL-S: Semantic markup for web services, W3C Member Submission[END_REF] as well as some work on semantic Web services [START_REF] Narayanan | Simulation, verification and automated composition of web services[END_REF]. The article [START_REF] Deutsch | Specification and verification of data-driven web applications[END_REF]] (building on [START_REF] Spielmann | Verification of relational transducers for electronic commerce[END_REF][START_REF] Abiteboul | Relational transducers for electronic commerce[END_REF]), considers the verification of properties of data-centric workflows specified in LTL-FO, first-order logic extended with linear-time temporal logic operators. Similar extensions have been previously used in various contexts [START_REF] Emerson | Temporal and modal logic[END_REF][START_REF] Abiteboul | Temporal versus first-order logic to query temporal databases[END_REF][START_REF] Spielmann | Verification of relational transducers for electronic commerce[END_REF]. Apart from the work on verification of BAXML with guards mentioned above [Abiteboul et al. 2008], most other work on static analysis on XML (with data values) deals with documents that do not evolve in time, e.g., [START_REF] Fan | On XML integrity constraints in the presence of DTDs[END_REF][START_REF] Arenas | Consistency of XML specifications[END_REF][START_REF] Alon | XML with data values: typechecking revisited[END_REF]]. This motivated studies of automata and logics on strings and trees over infinite alphabets [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]Demri and Lazić 2009;[START_REF] Bojanczyk | Two-variable logic on words with data[END_REF]]. See [START_REF] Segoufin | Static analysis of XML processing with data values[END_REF]] for a survey on related issues.

A survey on Active XML may be found in [Abiteboul et al. 2008]. In [Abiteboul et al. 2009], active XML documents are used to capture data and workflow management activities in distributed settings, in the spirit of the artifact approach. The study of the interplay between queries and sequencing in the artifact approach was the driving motivation of the present work.

This paper is the extended version of the conference article [START_REF] Abiteboul | Comparing workflow specification languages: a matter of views[END_REF]. It differs from the latter by including the full technical development, including the proofs.

Organization The paper is organized as follows. We introduce the view-based framework for comparing workflow languages in Section 2. The BAXML model and the workflow languages are presented in Sections 3 and 4. Their expressive power with respect to different views is compared in Section 5. In Section 6 we compare BAXML with a variant of IBM's business artifacts, and show that BAXML can simulate artifacts, but the converse is false. We end with brief conclusions.

VIEWS AND SIMULATIONS

In this section, we introduce an abstract framework for workflows and views of workflows. We then use it to compare workflows.

Workflow Systems and Languages. The model for workflows we consider is quite general. Intuitively, a workflow system describes the infinite tree of the possible runs of a particular system. More formally, the nodes of a workflow system are labeled by states from an infinite set Q ∞ and the edges by events from an infinite set E ∞ (Q ∞ ∩ E ∞ = ∅). For example, a state of a workflow system may be an instance of a relational database or an XML document. It may also include various other relevant information such as the state of an automaton controlling the workflow, or historical information such as the prefix of the run leading up to it. A typical event may consist of the activation of a task, including its parameters. The presence of data explains why the sets Q ∞ and E ∞ are taken to be infinite.

The workflow systems we consider include two particular events, namely block and ǫ, both in E ∞ , whose role we explain briefly. First consider block. For uniformity, it is convenient to assume that all runs are infinite. To this end, we use the distinguished event block to signal that the system has reached a terminal state that repeats forever (so once a system blocks, it remains blocked).

On the other hand, the ǫ event corresponds to the classical notion of silent transition. Its meaning is best explained in the context of a view (to be formally defined further), which defines the observable portion of states and events. In particular, it may hide information about states as well as events in the source system. For a transition in the source system, if the event is (even partially) visible in the view or if the state of the view changes, the transition is observable in the view. On the other hand, it may be the case that both the event and the state change are invisible in the view. So, although there has been a transition in the workflow system, nothing can be observed in the view. This is modeled by a silent transition, indicated by the special event ǫ. Observe that, unlike for blocking transitions, an ǫ transition may be followed in the view by non-ǫ (visible) transitions, in which the state may change.

More formally: Definition 2.1. [Workflow System] A workflow system is a tuple WS = (N, n 0 , δ, q 0 , λ N , λ δ ) where:

-(N, n 0 , δ) is a tree with root n 0 , nodes N , edges δ.

-all maximal paths from n 0 are infinite. -λ N is a function from N to Q ∞ , and λ N (n 0 ) = q 0 . -λ δ is a function from δ to E ∞ .

-for each (n, n ′ ) ∈ δ, if λ δ ((n, n ′ )) = ǫ then λ N (n) = λ N (n ′ ).

-for each (n, n ′ ) ∈ δ, if λ δ ((n, n ′ )) = block then n ′ is the only child of n and λ N (n) = λ N (n ′ ). Moreover, n ′ has only one outgoing edge also labeled block.

The edges in δ are also called transitions of the workflow, and q 0 is called its initial state.

Finally, a workflow language W consists of an infinite set of expressions, called workflow specifications. For example, BAXML, and its extensions with guards, automata, and temporal constraints, defined in Section 4, are all workflow languages. Given a workflow language W and W ∈ W, the semantics of W is a workflow system (i.e., the tree of runs defined by W ) and is denoted by

[W ] W , or [W ] when W is understood.
Views of Workflow Systems. We next formalize the notion of view of a workflow system. We will argue that this is an essential unifying tool for understanding diverse workflow models. In the present paper, we rely heavily on the notion of view in order to compare workflow languages.

A view V is a mapping on

Q ∞ ∪ E ∞ , such that V (Q ∞ ) ⊆ Q ∞ , V (E ∞ ) ⊆ E ∞ , V (ǫ) = ǫ
, and V (e) = block iff e = block. This mapping is extended to workflow systems as follows. Let WS = (N, n 0 , δ, q 0 , λ N , λ δ ) and V be a view. Then V (WS) is defined1 as (N, n 0 , δ, V (q 0 ),

λ N • V, λ δ • V ). We say that the view V is well-defined for WS if V (WS) is a workflow system.
Note that, by definition of the mapping, the properties of blocking transitions are automatically preserved. Note also that, by definition of well-defined workflow systems, for each

(n, n ′ ) ∈ δ, if V (λ δ ((n, n ′ ))) = ǫ then V (λ N (n)) = V (λ N (n ′ )).

Simulation of Workflows

We next consider the comparison of workflow systems and workflow languages based on the concept of view. We use a variant of bisimulation [START_REF] Milner | Communication and concurrency[END_REF]] (that we call w-bisimulation). Of course, many other semantics for comparison are possible. We refrain from attempting a taxonomy of such semantics, and instead settle on one definition that is quite general and adequate for our purposes.

In our semantics, we wish to be able to capture silent transitions as well as infinite branches of such transitions. Given a workflow system as above, for each e ∈ E -{ǫ}, we define the relation e → on nodes by n e → m if there is a sequence of transitions from n to m, all of which are silent except for the last one, which is labeled e.

Informally, the silent transitions are seen as partial internal computation that do not have impact on the possible observable reachable events. The choices made during the internal computation may be different, but the visible transitions at the end of sequences of silent transitions are the same. Definition 2.2. [w-bisimulation] Let WS i = (N i , n i 0 , δ i , q 0 , λ i N , λ i δ ), i ∈ {1, 2}, be two workflow systems (with the same initial state). A relation B from N 1 to N 2 is a w-bisimulation of WS 1 and WS 2 if B(n 1 0 , n 2 0 ) and for each n 1 , n 2 such that B(n 1 , n 2 ) the following hold:

-λ 1 N (n 1 ) = λ 2 N (n 2 ). -For each event e = ǫ, if there exists n ′ 1 such that n 1 e → n ′ 1 in WS 1 then there exists n ′ 2 such that n 2 e → n ′ 2 in WS 2 and B(n ′ 1 , n ′ 2 ), -For each event e = ǫ, if there exists n ′ 2 such that n 2 e → n ′ 2 in WS 2 then there exists n ′ 1 such that n 1 e → n ′ 1 in WS 1 and B(n ′ 1 , n ′ 2 ).
-there is an infinite path of silent transitions from n 1 in WS 1 iff there is an infinite path of silent transitions from n 2 in WS 2 .

We denote by WS 1 ∼ WS 2 the fact that there exists a w-bisimulation of WS 1 and WS 2 .

The last condition captures the intuition that progress from a given state along a path in the simulated system must imply progress from the corresponding state along a path in the simulating system, where progress means the occurrence of a non-silent event. We note that there are well-known notions of bisimulation related to ours, such as weak-bisimulation and observation-congruence equivalence, motivated by distributed algebra [START_REF] Milner | Communication and concurrency[END_REF]]. These differ from w-bisimulation in their treatment of silent transitions. For example, infinite paths of silent transitions are relevant to w-simulation but are ignored in weak bisimulation. It can be seen that observation-congruence equivalence implies w-bisimulation, but weak bisimulation and w-bisimulation are incomparable.

Clearly, ∼ is an equivalence relation. Observe that views preserve w-bisimulation. More precisely, let

WS 1 ∼ WS 2 . Then for each view V , (*) V (WS 1 ) is well-defined iff V (WS 2 ) is well-defined, in which case V (WS 1 ) ∼ V (WS 2 ).
Equivalence of workflow systems as previously defined essentially requires the two systems to have the same set of states and events. However, in general we wish to compare workflow systems whose states and events may be very different. In order to make them comparable, we use views mapping the states and events of each system to a common, possibly new set of states and events. Intuitively, these represent abstractions extracting the observable information relevant to the comparison. The views may also involve substantial restructuring, thus extending classical database views.

Suppose we wish to compare languages W 1 and W 2 . To compare workflow specifications in W 1 and W 2 , we use sets of views V 1 and V 2 that map the states and events of W 1 and W 2 to a common set.

Definition 2.3. [Simulation] Let W 1 , W 2 be workflow languages and V 1 , V 2 be sets of views. The language W 2 simulates W 1 with respect to (V 1 , V 2 ), denoted by W 1 ֒→ (V1,V2) W 2 , if for each W 1 ∈ W 1 and V 1 ∈ V 1 such that V 1 (W 1 ) is well-defined, there exist W 2 ∈ W 2 and V 2 ∈ V 2 such V 2 (W 2 ) is well-defined and V 1 (W 1 ) ∼ V 2 (W 2 ).
Remark 2.4. Note that the definition of simulation does not require effective construction of the simulating workflow specification. However, all our positive simulation results are constructive. The negative result in Theorem 6.9 also concerns effective simulation.

For sets of views V, V ′ , we define

V • V ′ = {V • V ′ | V ∈ V, V ′ ∈ V ′ }. Intuitively, a view V • V ′ is coarser than V (or equivalently, V is more refined than V • V ′ ).
The following key lemma is a straightforward consequence of (*). It states that the relation ֒→ is stable under composition of views.

LEMMA 2.5. [Composition Lemma] Let W 1 and W 2 be workflow languages and V 1 , V 2 and V be sets of views. If

W 1 ֒→ (V1,V2) W 2 then W 1 ֒→ (V1•V,V2•V) W 2 .
The Composition Lemma allows to relate simulations relative to different classes of views. It says that simulation relative to given views implies simulation relative to any coarser views. This provides a tool for proving both positive and negative simulation results.

A useful version of the above lemma is the following, combining composition and transitivity.

LEMMA 2.6. Let W 1 , W 2 , W 3 be workflow languages, and V 1 , V 2 , V 3 and V be sets of views.

If W 1 ֒→ (V1,V2•V) W 2 and W 2 ֒→ (V2,V3) W 3 , then W 1 ֒→ (V1,V3•V) W 3 .
As we will see, the version of transitivity provided by the above is routinely used in proofs that combine multiple stages of simulation.

THE BASIC AXML MODEL

In this section we present BAXML, the Basic AXML model. This is essentially a simplified version of the GAXML model of [Abiteboul et al. 2008], obtained by stripping it of the control provided by call and return guards of functions (all such guards are set to true). We consider such control later as one of the workflow specification mechanisms. The section may be skipped by readers familiar with the GAXML model.

We begin with an informal overview of the model, then provide more details. To illustrate our definitions, we use a simplified version of the Mail Order example of [Abiteboul et al. 2008]. The purpose of the Mail Order system is to fetch and process individual mail orders. The system accesses a catalog subtree providing the price for each product. Each order follows a simple workflow whereby a customer is first billed, a payment is received and, if the payment is in the right amount, the ordered product is delivered.

BAXML documents are abstractions of XML with embedded service calls. A BAXML document is a forest of unordered, unranked trees, whose internal nodes are labeled with tags from a finite alphabet and whose leaves are labeled with tags, data values, or function symbols. More precisely, a function symbol !f indicates a node where function f can be called, and a function symbol ?f indicates that a call to f has been made but the answer has not yet been returned. For example, a BAXML document is shown in Figure 1. The BAXML document may be subject to static constraints specified by a DTD, as well as Boolean combinations of tree patterns. For example, the negation of the pattern in Figure 2 (a) says that an Order ID uniquely determines the product and customer names. In patterns, double edges denote descendant and single edges the child relation.

A BAXML document evolves as a result of making function calls and receiving their results. A call can be made and an answer can be returned at any point, as long as the resulting instance satisfies the static constraints. The argument of the call is specified by a query on the document, producing a forest. The query may refer to the node at which the call is made (denoted by self ), so the location of the call in the document is important. When a call is made at node x labeled !f, its label changes from !f to ?f. The result of a call consists of another BAXML document, so a forest, whose trees are added as siblings of the node x where the call was made. After the answer of the call at node x is returned, x may be kept (in which case its label reverts to !f) or x may be deleted. This is specified by the schema, for each function f. If calls to !f are kept, f is called continuous, otherwise it is non-continuous (this is specified in the schema).

For example, consider the MailOrder function in Figure 1. Intuitively, its role is to fetch new mail orders from customers. For instance, one result of a call to !MailOrder may consist of the subtree with root MailOrder in Figure 1. Since the function is processed externally, the semantics of its evaluation is not known. We call such a function external. Its specification consists of its input query and a DTD constraining the allowed answers. In addition to external functions, there are functions processed internally by the BAXML system. These are called internal. For example, Bill is such a function. When a call to Bill is made at a node x labeled !Bill, the label of x turns to ?Bill (to indicate that a call has been made whose answer is still pending) and the call is processed internally. Specifically, the call generates a new BAXML document (a workspace) that evolves under function calls and returns. The answer can be returned at any point when the workspace contains no running calls (i.e. no nodes labeled ?g for some g) and the resulting instance satisfies the static constraints. The contents of the result is specified by a return query that applies to the workspace. For example, the answer to a call to Bill can be returned once payment has been received. The answer, specified by the return query, provides the product paid for and amount of payment (see Example 3.1).

Once the result of a call has been returned, the BAXML document of the corresponding workspace is removed. In order for the result to be returned at the correct location (next to node x), a mapping called eval is maintained between nodes where calls have been made and BAXML document corresponding to the workspaces (e.g., see Figure 5). The system evolves by repeated function calls and answer returns, occurring one at a time non-deterministically. This may reach a blocking instance in which no function can be called and no result can be returned, or may continue forever, leading to an infinite run. For example, runs of the Mail Order system are always infinite since new mail orders can always be fetched. For uniformity, we make all runs infinite by repeating blocking instances forever.

We now describe the BAXML model in more detail. We assume given the following disjoint infinite sets: nodes N (denoted by n, m), tags Σ (denoted by a, b, c, . . .), function names F, data values D (denoted by α, β, . . .) data variables V (denoted by X, Y, Z, . . .), possibly with subscripts. In the model, trees are unranked and unordered.

For each function name f, we also use the symbols !f and ?f, called function symbols, and denote by F ! the set {!f | f ∈ F} and by F ? the set {?f | f ∈ F}. As described above, !f labels a node where a call to function f can be made (possible call), and ?f labels a node where a call to f has been made and some result is expected (running call). When a call to f is made at a node x labeled !f, the label changes from !f to ?f. After the answer of the call at node x is returned, the node x may be kept or the node x may be deleted. If x is kept, its label changes from ?f back to !f. If calls to !f are kept, f is called continuous, otherwise it is non-continuous. For example, the role of the MailOrder function in Figure 1 is to indefinitely fetch new mail orders from customers, so MailOrder is specified to be continuous. On the other hand, the function !Bill occurring in a MailOrder is meant to be called only once, in order to carry out the billing task. Once the task is finished, the call can be removed. Therefore, Bill is specified to be non-continuous. A BAXML document is a tree whose internal nodes are labeled with tags in Σ and whose leaves are labeled by either tags, function symbols, or data values. A BAXML forest is a set of BAXML trees. An example of BAXML document is given in Figure 1.

To avoid repetitions of isomorphic sibling subtrees, we define the notion of reduced tree. A tree is reduced if it contains no distinct isomorphic sibling subtrees without running calls ?f. We henceforth assume that all trees considered are reduced, unless stated otherwise. However, note that the forest of an instance may generally contain multiple isomorphic trees.

Patterns. We use patterns as the basis for our query language, and later in the specification of workflow constraints and temporal properties. A pattern is a forest of tree-patterns. A tree-pattern is a tree whose edges are labeled by child (/) or descendant (//) where descendant is reflexive. Nodes are labeled by tags if they are internal, and by tags, function symbols, or variables if they are leafs. In addition, nodes may be labeled by wildcard (*), which can map to any tag. A constraint consisting of a Boolean combination of (in)equalities between the variables and/or data constants may also be given. In particular, we can specify joins (equality of data values). A tree-pattern is evaluated over a tree in the straightforward way. The definition of the evaluation of patterns over forests extends the above in the natural way. An example is given in Figure 2 (a). The pattern shown there expresses the fact that the value Order-Id is not a key. It does not hold on the BAXML document of Figure 1. (Indeed, it is natural to require that Order-Id be a key).

We sometimes use patterns that are evaluated relative to a specified node in the tree. More precisely, a relative pattern is a pair (P , self ) where P is a pattern and self is a node of P . A relative pattern (P , self ) is evaluated on a pair (F, n) where F is a forest and n is a node of F . Such a pattern forces the node self in the pattern to be mapped to n. Figure 2 (b) provides an example of a relative pattern. The pattern shown there checks that a product that has been ordered occurs in the catalog. It holds in the BAXML document of Figure 1 when evaluated at the unique node labeled !Bill.

We also consider Boolean combinations of (relative) patterns. The (relative) patterns are matched independently of each other and the Boolean operators have their standard meaning. If a variable X occurs in two different patterns P and P ′ of the Boolean combination then it is quantified existentially in P and P ′ , independently of each other.

It will be useful to occasionally consider parameterized patterns, in which some variables are designated as free. Let P ( X) be a pattern with free variables X, and ν an assignment of data values to X. A BAXML forest I satisfies P ( X) for assignment ν, denoted by I, ν |= P ( X), if I satisfies the pattern P (ν( X)) obtained by replacing each variable in X by its value under ν. Queries. As previously mentioned, patterns are used in queries, as shown next. A query is a finite union of rules of the form Body → Head, where Body and Head are patterns and Head contains no descendant edges and no constants, and all its variables occur in Body. In each tree of Head, all variables occur under a designated constructor node, specifying a form of nesting. When evaluated on a forest, the matchings of Body define a set of valuations of the variables. The answer for the rule is obtained by replacing, in each tree of Head, the subtree rooted at the constructor node with the forest obtained by instantiating the variables in the subtree with all their matchings provided by the Body. The answer to the query is the union of the answers for each rule. As for patterns, we may consider queries evaluated relative to a specified node in the input tree. A relative query is defined like a query, except that the bodies of its rules are relative patterns (P , self ). An example of a relative query (with a single rule) is given in Figure 3 (the notation self :!Bill means that the node self must be labeled !Bill). The label of the constructor node (indicated by brackets) is Process-bill. DTD. Trees used by a BAXML system may be constrained using DTDs and Boolean combinations of patterns. For DTDs, we use a typing mechanism that restricts, for each tag a ∈ Σ, the labels of children that a-nodes may have. As our trees are unordered we use Boolean combinations of statements of the form |b| ≥ k for b ∈ Σ ∪ F ! ∪ F ? ∪ {dom}, k a non-negative integer, and dom a symbol indicating the presence of a data value. Validity of trees and of forests relative to a DTD is defined in the standard way.

Schemas and instances.

A BAXML schema S is a tuple (Φ int , Φ ext , ∆) where (i) the set Φ int contains a finite set of internal function specifications, (ii) the set Φ ext contains a finite set of external function specifications, and (iii) ∆ consists of a DTD and a Boolean combination of patterns providing static constraints on instances of the schema. For instance, the negation of the pattern in Figure 2 (a) states that Order-Id uniquely determines the mail order.

We next detail Φ int and Φ ext . For each f ∈ F, let a f be a new distinct label in Σ. Intuitively, a f labels the roots of all workspaces resulting from calls to f. The specification of a function f of Φ int indicates whether f is continuous or not, provides its argument query , and return query . The role of the argument query is to define the initial state of the workspace generated by the call to f. The argument query is a relative query. When the query is evaluated, self binds to the node at which the call !f is made. The return query applies to the current state of the workspace corresponding to the call. Thus, it is a query in which every tree pattern occurring in the body of a rule is rooted at a f . . where p is the product name and a the amount of payment.

Each function f in Φ ext is specified similarly, except that the return query is missing. In addition, a DTD ∆ f constrains the answers returned by f (the DTD assumes a virtual root under which the answer forest is placed). Intuitively, an external call can return any answer satisfying ∆ f at any time, as long as the resulting instance also satisfies the global static constraints ∆. For example, MailOrder is external, since its role is to fetch orders from an external user.

An instance I over a BAXML schema S = (Φ int , Φ ext , ∆) is a pair (T, eval), where T is a BAXML forest and eval an injective function over the set of nodes in T labeled with ?f for some f ∈ Φ int such that: (i) for each n with label Fig. 4: Answer of the query in Figure 3 applied to the instance in Figure 1 ?f, eval(n) is a tree in T with root label a f (its workspace), and (ii) every tree in T with root label a f is eval(n) for some n labeled ?f. An instance of S is valid if it satisfies ∆. More precisely, each tree in the forest making up the instance satisfies the DTD of ∆, and the instance as a whole satisfies the Boolean combination of patterns of ∆.

Runs. Let I = (T, eval) and I ′ = (T ′ , eval ′ ) be instances of a BAXML schema S = (Φ int , Φ ext , ∆). The instance I ′ is a possible next instance of I iff I ′ is obtained from I by making a function call or by receiving the answer to an existing call. We refer to the latter as an event. More precisely, an event is an expression of the form !f(F ) or ?f(G), where:

f is a function; -F is the forest consisting of the result of applying the argument query of f to T, at some node labeled !f; -G is the forest consisting of the answer to a running call ?f at some node n. More precisely, if f is internal, G is the result of applying the return query of f to eval(n). If f is external, G is any forest satisfying the DTD ∆ f for answers of f.

For technical reasons, we also use two special events, init that only generates the initial instance, and block, whose use will be clear shortly. Initial instances of BAXML schemas are defined below. We denote by I ⊢ e I ′ the fact that I ′ is a possible next instance of I caused by event e.

We now provide more details. Consider I = (T, eval) and an event !f(F ), resulting from a call to !f at some node n of T. The next instance, if it exists, is the instance I ′ = (T ′ , eval ′ ) satisfying ∆, obtained as follows:

-change the label of n to ?f -if f is internal, add to the graph of eval the pair (n, T ′ ) where T ′ is a tree consisting of a root a f connected to all trees in F (the result of evaluating the argument query of f on input (T, n)).

If the resulting instance does not satisfy ∆, there is no next instance under the event !f(F ). Now consider an event ?f(G), resulting from returning the answer G of a running call ?f at some node n of T. Recall that, if f is internal and eval(n) contains no running function calls, G is the result of applying the return query of f to eval(n). If f is external, G is any forest satisfying ∆ f . Then the instance I ′ is obtained as follows:

-add all trees in G as siblings to n -if f is internal, remove (n, eval(n)) from the graph of eval and the tree eval(n) from T -if f is non-continuous, remove the node n from T -if f is continuous, change the label of n from ?f to !f.

If the resulting instance does not satisfy ∆, then there is no next instance under the event ?f (G).

Figure 5 shows a possible next instance for the instance of Figure 1 after an internal call has been made to !Bill. The node associated with this internal call is denoted by n. Recall the specification of Bill from Example 3.1. The argument query of Bill is the query in Figure 3. For each homomorphism from the body (left pattern) of Figure 3 to the document such that the node labeled self is associated with n, a valuation of the variables is defined. In this example, there is one homomorphism defining the following valuation : X = N ikon and Y = 199. The answer of the query is built by applying the previous valuation to the variable in the head of the query (the right part). The answer is described in Figure 4. The workspace of the function Bill is built by placing the answer from Figure 4 under a new root n ′ labeled a Bill . This workspace is added to the current instance and the function eval is updated by setting eval(n) = n ′ . The resulting instance is shown in Figure 5, where the dotted arrow represents the function eval.

We will typically be interested in runs of such systems. An initial instance of schema S is an instance of S consisting of a single tree whose root is not a function call and for which there is no running call. For runs, we use a variation of the model of [Abiteboul et al. 2008]. A prerun of a schema S is a finite sequence {(I i , e i )} 0≤i≤n , such that (i) for each i, I i satisfies the static constraints ∆, (ii) e 0 = init, and (iii) for each i > 0, I i-1 ⊢ ei I i . Intuitively, e 0 generates the initial instance I 0 . A run is an infinite sequence ρ = {(I i , e i )} i≥0 such that each finite prefix of ρ is a prerun of S, or there is a finite prefix (I 0 , e 0 ), ..., (I n , e n ) of ρ that is a maximal prerun2 of S; and for each i > n, I i = I n and e i = block. In the first case the run is called nonblocking; in the second case it is called blocking. Thus, we force all runs to be infinite by repeating forever a blocking instance from which no legal transition is possible, if such an instance is reached (the non-existence of a legal transition from the blocking instance is ensured by the maximality condition in the definition).

Semantics with and without aborts. We next discuss a subtle difference between the semantics adopted here and that of [Abiteboul et al. 2008]. According to our semantics, if a prerun reaches an instance from which every transition leads to a violation of the static constraints, the prerun blocks forever in that instance, generating a blocking run. In contrast, the semantics of [Abiteboul et al. 2008] allows blocking runs only if no transition exists at all (whether leading to a valid instance or not). If there are possible transitions but they all lead to constraint violations, the prerun is discarded. Intuitively, this amounts to aborting the run. We refer to this as the semantics of runs with aborts, and to the one we follow in this paper as the semantics of runs (without aborts). Note that in our semantics, every prerun is extensible to a (possibly blocking) run, whereas this is not the case in the semantics with aborts. Furthermore, as shown next, in the semantics with aborts it is undecidable if a given prerun can be extended to an infinite run. This is a main motivation for our choice of the semantics without aborts. THEOREM 3.2. Let S be a BAXML schema and ρ a prerun of S. Under the semantics with aborts, it is undecidable whether ρ is the prefix of a run of S. Furthermore, this remains undecidable even for nonrecursive3 DTDs.

PROOF. The proof for arbitrary DTDs is trivial by the undecidability of satisfiability of static constraints [START_REF] David | Complexity of data tree patterns over XML documents[END_REF]]. The proof for nonrecursive DTDs is by reduction of the implication problem for functional and inclusion dependencies (FDs and IDs), known to be undecidable (see [START_REF] Abiteboul | Foundations of Databases[END_REF]).

Let R be a relation with k attributes, Γ a set of FDs and IDs over R, and F an FD over R. We construct a BAXML schema S and an initial instance I 0 such that Γ |= F iff there is a valid run from I 0 . We represent relation R with attributes A 1 • • • A k in the standard way, as a tree rooted at R. Relation R, together with some additional functions whose role will become apparent, is depicted in Figure 6. Clearly, this structure can be enforced by the DTD.

Static constraints can easily require satisfaction of the FDs in Γ and violation of F . In order to check that the inclusion dependencies of Γ are satisfied, we use one internal, non-continuous function f τ for each τ ∈ Γ. One occurrence of each f τ is attached to each tuple of R, as in Figure 6. The functions f τ always return the empty answer. Static constraints require the following:

(i) there is at most one occurrence of ?f τ for each τ , (ii) whenever ?f τ occurs, the ID τ is satisfied for the tuple to which ?f τ is attached.

The constraint (i) is expressed by conjunctions of negations of patterns as in (i) of Figure 7, and (ii) is enforced by the conjunction of patterns as in (ii) of the same figure, illustrating the case when

τ = R[A i ] ⊆ R[A j ].
Finally, the global DTD specifies a root r, under which one can find either a subtree rooted at R of the shape above, or one external, non-continuous function !h. Thus, the instance I 0 consisting of the root r with child !h is a possible

R T A1 x1 • • • A k x k ?fτ T A1 y1 • • • A k y k ?fτ i xi = yi (i) R ?fτ -→ R T Ai x ?fτ T Aj x (ii)
A i ] ⊆ [A j ]
initial instance. Note that every valid run of S must end in a blocking instance, in which no function calls occur.

Clearly, there exists such a valid run from I 0 iff the function h can return a tree R witnessing that Γ |= F .

WORKFLOW CONSTRAINTS

In this section, we introduce three ways of enriching the BAXML model with workflow constraints: (i) function call and return guards (yielding the GAXML model), (ii) an automaton model (yielding the AAXML model), and (iii) temporal constraints (yielding the TAXML model). Each corresponds to a very natural way of expressing constraints on the evolution of a system. We study and compare these mechanisms in the next sections.

We begin by considering an abstract notion of workflow constraint. A workflow constraint W over a BAXML schema S is a prefix-closed property of preruns of S. For a prerun ρ of S, we denote by ρ |= W the fact that ρ satisfies W . We denote by S|W the workflow specification defined by S constrained by W . A run of S|W is an infinite sequence ρ = {(I i , e i )} i≥0 such that: each finite prefix of ρ is a prerun of S that satisfies W, or there is a finite prefix (I 0 , e 0 ), ..., (I n , e n ) of ρ that is a maximal prerun of S satisfying W; and for each i > n, I i = I n and e i = block. In the first case the run is called nonblocking; in the second case it is called blocking.

Observe that nonblocking runs of S|W are particular nonblocking runs of S. Also, a sequence {(I i , e i )} i≥0 may be a blocking run of S|W but not a blocking run of S. (This is because all transitions that are possible according to S are forbidden by W .) The set of runs of S|W is denoted by runs(S|W ).

A main goal of the paper is to compare the descriptive power of different formalisms for specifying workflow constraints. To this end, we consider the workflow languages G (for call guards), A (for automata), and T (for temporal formulas), defined next.

Call and return guards

Recall the Mail Order example, in which processing an order requires executing some tasks in a desired sequence (order, bill, pay, deliver). Since tasks in BAXML are initiated by function calls, one convenient workflow specification mechanism is to attach guards to function calls. For instance, the guard of !Deliver, shown in Figure 8, might require that the ordered product must have been paid in the correct amount. Similarly, it is useful to control when the answer of an internal function may be returned. This can be done by providing return guards.

Let S = (Φ int , Φ ext , ∆) be a BAXML schema. A guard assignment over S is a pair γ = (γ c , γ r ), where:

γ c , the call guard assignment, is a mapping from the functions of S to Boolean combinations of relative patterns over S. A call to f can only be activated at node n of instance I = (T, eval) if γ c (f) holds on (T, n). -γ r , the return guard assignment, is a mapping from the functions of S which is true for external functions and a Boolean combination of tree patterns rooted at a f for each internal function f. The result of a call to f at node n of instance I = (T, eval) is returned only when γ r (f) is satisfied on eval(n). Return guards constrain only internal functions.

A prerun ρ = (I 0 , e 0 ), ..., (I n , e n ) of S satisfies γ = (γ c , γ r ), denoted ρ |= γ, if for each transition I i-1 ⊢ ei I i , if the transition results from a function call to !f at node u the guard γ c (f) holds in (I i-1 , u), and if the transition results from the return of an internal function call ?f at node u, γ r (f) holds in eval i-1 (u). Observe that these constraints involve consecutive instances only.

The set of all guard workflow constraints is denoted by G. A GAXML schema is an expression S|γ, for some γ ∈ G. Figure 8 shows call guards for some functions in the Mail Order example. The call guard of function Bill is given in Figure 2(b) (this checks that the ordered product is available). The call guard of Invoice is true. In the same example, the return guard of function Bill is: aBill Payment indicating that payment has been received, so billing is completed.

Main

Pattern automata

We next consider workflows based on automata. The states of the automaton are defined using pattern queries. The automaton has no final states, since BAXML (like AXML) does not have a built-in notion of successful computation.

A pattern automaton is a tuple (Q, q init , δ, Υ) where:

-Q is a finite set of states, q init ∈ Q, and each q ∈ Q has an associated set of variables X q ; -For each q ∈ Q, Υ(q) is a Boolean combination of parameterized patterns whose set of free variables equals X q ; -the transition function δ is a partial function from Q × Q such that δ(q, q ′ ) is a Boolean combination of equalities of variables among X q and X q ′ .

To simplify the presentation, we assume without loss of generality that X q and X q ′ have no variables in common.

Let A be the set of pattern automata. An AAXML schema is an expression S|A for a BAXML schema S and A ∈ A. A prerun ρ = {(I i , e i )} i≤n of S satisfies an automaton constraint A, denoted by ρ |= A, if there exists a sequence {(q i , ν i )} i≤n , where q 0 = q init and ν i is a valuation of X qi , such that for each i ≤ n:

(1)

I i , ν i |= Υ(q i ), (2) ν i (X qi ) ∪ ν i+1 (X qi+1 ) |= δ(q i , q i+1 ).
Intuitively, the state of such an automaton after reading a finite sequence ρ of instances is a pair (q, ν) where ν is a valuation of the variables in X q . Note that the automaton is non-deterministic both with respect to the state and the valuation of its variables.

Example 4.2. An automaton for our running example is represented in Figure 9. The edges represent the pairs for which δ is defined, and the patterns in Υ check the following:

-Υ(q init ) checks nothing. -Υ(p) checks that the call to Bill has been activated and the product is in the catalog: We note that in some specification models, such as state-charts [START_REF] Harel | Statecharts: A visual formulation for complex systems[END_REF]], states are defined in a hierarchical manner, i.e. entering a state may trigger a more refined state-transition sub-system. Other systems further extend this with recursion [START_REF] Alur | Analysis of recursive state machines[END_REF]. Although not done here, one could extend our formalism to capture such hierarchical or recursive states.

Past-Tree-LTL

Finally, we consider workflow constraints specified using temporal formulas. Intuitively, these state, given a particular history, whether a given transition is allowed. The language is a variant of Tree-LTL [Abiteboul et al. 2008] using only past LTL operators, that we call Past-Tree-LTL. It is obtained from classical propositional LTL (e.g., see [START_REF] Emerson | Temporal and modal logic[END_REF]) by interpreting each proposition as a parameterized tree pattern P ( X) where X is a subset of its variables, designated as global. All global variables are treated as free in the patterns and are quantified existentially at the end. The past temporal operators are X -1 (previously), S (since) and G -1 (always previously). The semantics of the different operators is inductively defined as follows:

-(I 0 , e 0 ), . . . , (I n , e n ) |= ϕ, where ϕ is a pattern iff I n satisfies ϕ.

-(I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 1 ∧ ϕ 2 iff (I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 1 and (I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 2 -(I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 1 ∨ ϕ 2 iff (I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 1 or (I 0 , e 0 ), . . . , (I n , e n ) |= ϕ 2 -(I 0 , e 0 ), . . . , (I n , e n ) |= ¬ϕ iff (I 0 , e 0 ), . . . , (I n , e n ) |= ϕ -(I 0 , e 0 ), . . . , (I n , e n ) |= X -1 ϕ iff (I 0 , e 0 ), . . . , (I n-1 , e n-1 ) |= ϕ -(I 0 , e 0 ), . . . , (I n , e n ) |= ϕSψ iff (I 0 , e 0 ), . . . , (I j , e j ) |= ψ for some j ≤ n and ϕ holds in (I 0 , e 0 ), . . . , (I k , e k ) for every k, j < k ≤ n -(I 0 , e 0 ), . . . , (I n , e n ) |= G -1 ϕ iff (I 0 , e 0 ), . . . , (I j , e j ) |= ϕ for each j, 0 ≤ j ≤ n.

In summary, a Past-Tree-LTL formula is of the form ∃Xψ(X) where ψ uses only the temporal operators X -1 and S, and X is the set of global variables of the parameterized patterns interpreting the propositions. The set of Past-Tree-LTL formulas is denoted by T. A TAXML schema is an expression S|θ for S a BAXML schema and θ ∈ T. A prerun ρ satisfies ∃Xψ(X) if ρ satisfies ψ(ν(X)) for some valuation ν of the global variables X in the active domain of ρ.

The choice to existentially quantify the global free variables appears natural for specifying workflow transition constraints. Observe that such variables are quantified universally in the language Tree-LTL of [Abiteboul et al. 2008], used to specify properties of all runs. However, the model checking approach of [Abiteboul et al. 2008] is based on checking unsatisfiability of the negation of Tree-LTL formulas, whose global variables then become existentially quantified.

Example 4.3. To illustrate Past-Tree-LTL constraints, consider the description of valid transitions in the MailOrder example. This can be specified by a Past-Tree-LTL conjunctive formula:

G -1 (ψ ?Bill ∧ X -1 (ψ !Bill ) =⇒ X -1 (ψ γc(Bill) )) ∧ G -1 (ψ ?Invoice =⇒ X -1 ψ ?Bill ) ∧ G -1 (ψ Payment =⇒ X -1 ψ ?Invoice ) ∧ G -1 (ψ Paid ∧ ψ !Deliver,!Reject =⇒ X -1 ψ ?Payment ) ∧ G -1 (ψ ?Deliver =⇒ X -1 ψ γc(Deliver) ) ∧ G -1 (ψ ?Reject =⇒ X -1 ψ γc(Reject) ) ∧ G -1 (ψ finish-Deliver =⇒ X -1 ψ ?Deliver ) ∧ G -1 (ψ finish-Reject =⇒ X -1 ψ ?Reject )
We detail next the formulas used above:

-The formula ψ γc(Bill) checks that the call guard of Bill is true: -Finally, the formula ψ finish-Reject checks that Reject has returned by checking that the function calls to Reject and Bill no longer appear in the document:

Checking workflow constraints

The following establishes the complexity of testing workflow constraints.

THEOREM 4.4. For a fixed BAXML schema S and a fixed W where W ∈ {G, A, T}, it is decidable in PTIME whether a given prerun ρ of S satisfies W .

PROOF. Let S|W be a workflow schema and ρ = (I i ), 1 ≤ i ≤ n be a prerun of S. Note first that we can check that I 0 verifies the constraints of S and those imposed on initial instances by W in PTIME with respect to |I 0 |. For γ ∈ G, it is clear that one can further check, for each i < n, whether the transition from I i to I i+1 satisfies γ in PTIME with respect to |I i | + |I i+1 |. Consider an automaton A = (Q, q init , δ, Υ). To check that ρ satisfies A, we define by induction on i auxiliary relations R i q for each state q ∈ Q as follows. For i = 0, all R q are empty except R qinit that contains all valuations ν of X qinit for which I 0 , ν |= Υ(q init ). For i > 0, R i q contains all valuations ν of Xq for which there exists a sequence (q j , ν j ), j ≤ i, where q 0 = q init , q i = q, ν = ν i , and for each j < i, ν j is a valuation of X qj , such that:

(1)

I j , ν j |= Υ(q j ), (2) ν j (X qj ) ∪ ν j+1 (X qj+1 ) |= δ(q j , q j+1 ).
It is clear that for each i, the relations {R i+1 q | q ∈ Q} can be computed from I i+1 and {R i q | q ∈ Q} in polynomial time. Moreover, the size of the relations R i+1 q remains polynomial in the number of data values occurring in the entire prefix (I j ), 0 ≤ j ≤ i + 1. Therefore, the set of relations {R n q | q ∈ Q} can be constructed in time polynomial in |ρ|. Finally, ρ satisfies A iff some relation R n q is nonempty for some q. Finally, consider T. Let θ be a Past-Tree-LTL formula ∃Xψ(X). We must check that for some valuation ν of X to data values in ρ, ρ satisfies θ ν = ψ(ν). Observe that θ ν has no global variables. Let θ 0 ν be a Past-LTL propositional formula from which θ ν is obtained by interpreting the propositions by Boolean pattern formulas. To each truth assignment of the propositions, one can assign a symbol. Let Σ be this set of symbols. There exists an automaton A 0 with alphabet Σ, that is equivalent to θ 0 ν . From A 0 it is straightforward to construct a tree-pattern automaton A ν such that S|θ ν and S|A ν have the same runs. Using the earlier result for automata, we can check that ρ satisfies A ν in polynomial time. Moreover, it can be seen that the polynomial bound is independent of ν. Since there are polynomially many ν (for fixed ψ), it can be checked in PTIME whether ρ satisfies ψ.

Remark 4.5. The complexity analysis in Theorem 4.4 assumes a fixed workflow schema. It is easily seen that the combined complexity (with respect to both prerun and schema) is upper-bounded by EXPTIME.

A more difficult decision problem is checking the existence of a valid transition extending the current prerun. Indeed, this is undecidable even for BAXML schemas with no workflow constraints (with either flavor of the abort semantics). The difficulty arises from the power of external functions. Indeed, without external functions it suffices to test all possible call activations and returns. However, the problem becomes decidable for bounded trees. THEOREM 4.6. (i) It is undecidable, given a BAXML schema S and a prerun ρ of S, whether ρ is blocking. (ii) It is undecidable, given a BAXML schema S with non-recursive DTD and a prerun ρ of S, whether ρ is blocking.

PROOF. (i)

The undecidability is due to the external functions. We have to test whether there is some returned data that would be valid for the static constraints. This is undecidable because of the undecidability of the satisfiability of Boolean combinations of tree patterns under arbitrary DTDs [START_REF] David | Complexity of data tree patterns over XML documents[END_REF]].

(ii) For each non-activated function call !f, it is sufficient to test it directly, and similarly for the return of an internal function call. Let ?f be an activated external function call. The problem of the possible return of ?f can be reduced to the satisfiability of a Boolean combination of patterns by an instance satisfying a non-recursive DTD, which is decidable [START_REF] David | Complexity of data tree patterns over XML documents[END_REF]]. First, the DTD of the answer of the function f is rewritten to take into account the sibling trees of the function call ?f and the DTD of the schema. The rewritten DTD τ ′ ensures in particular that ( * ) for a returned forest F , there exists a forest F ′ having the same multiset of the labels of roots as F and any tree of F ′ is isomorphic to a sibling of ?f. Intuitively, the construction of the Boolean combination of patterns is done by looking for patterns that can extend prefixes of patterns of the static constraints already mapped into the current instance. The extraction of the Boolean combination ϕ ′ from the static constraints is done as follows: Each pattern P is rewritten as a disjunction ∨ϕ P,P ′ (ν), where P ′ is a prefix of P and ν a valuation of the variables of P ′ . A formula ϕ P,P ′ (ν) is in the disjunction iff there is a mapping of P ′ (ν) in the instance I that can be extended to each node n of P not in P ′ but whose parent is in P ′ , such that n can be mapped to ?f. The definition of ϕ P,P ′ (ν) is the conjunction of subpatterns [n] P (ν). A pattern [n] P is defined as follows:

-If the incoming edge to n is a child edge, then [n] P is the subtree rooted at n.

-If the incoming edge to n is a descendant edge, then [n] P is a root labeled with * and its only subtree is the subtree rooted at n. The edge between the root and the subtree is a descendant edge.

If P and P ′ are equal then ϕ P,P (ν) is set to true.

The formula ϕ ′ is satisfiable for reduced trees under τ ′ iff the function ?f can return.

EXPRESSIVENESS

In this section we compare the expressive power of BAXML, GAXML, AAXML, and TAXML, using the framework developed in Section 2. We begin by comparing the languages relative to views retaining full information about the current BAXML document, that we refer to as identity views. We then consider a more permissive version allowing to hide some of the data and functions, thus providing more leeway for simulations.

Workflow system semantics. We begin by casting the semantics of BAXML, GAXML, AAXML, and TAXML in terms of the workflow systems described in Section 2. For each specification S (for BAXML) or S|W (for GAXML, AAXML and TAXML), the nodes of the workflow system are the finite prefixes of runs of S or S|W . The root is the empty prefix, and its state label is the empty instance. The state label for each node other than the root is the last instance in the prefix. For each non-root node ν, there is an edge labeled e from ν to node ν ′ if ν ′ extends ν with a single instance by event e that is a function call or the return of a such a call. The root has an outgoing edge to each node consisting of a prefix of length one, labeled by a distinguished event init. Thus, transitions from the root simply provide the initial instances of runs, and the infinite paths starting from children of the root correspond to the runs of S|W . Because of the semantics of blocking runs, each path is extensible to an infinite path.

Note that there are alternative choices of workflow system semantics, and different goals may require different choices. For example, for AAXML it may be natural to retain in the state, information on the current state of the associated automaton together with the valuation of its parameters. This would simplify defining views where such states are included in the observables.

Comparison with identity views

We first compare BAXML, GAXML, AAXML, and TAXML relative to the identity view on the states and events of the workflow system (denoted id), thus preserving full information on the system. Observe that if a language W 2 simulates W 1 with respect to (id, id), this means that for each W 1 in W 1 , there exists W 2 in W 2 , such that W 1 ∼ W 2 , i.e., W 1 and W 2 have exactly the same runs. So, this is a very strong requirement. Note also, that since id is the most refined possible view of a workflow system, existence of simulation with respect to id would imply, by Lemma 2.5, the existence of simulation with respect to any coarser view. Unfortunately (but not surprisingly), the three extensions of BAXML models are incomparable relative to the identity view.

Given workflow specifications W 1 and W 2 , we denote by W 1 ≡ W 2 the fact that W 1 and W 2 have the same sets of runs.

THEOREM 5.1. The workflow languages GAXML, AAXML and TAXML are incomparable relative to ֒→ (id,id) .

We prove the theorem by a sequence of lemmas. The first two state that GAXML ֒→ (id,id) {AAXML, TAXML} (by showing that there is a GAXML schema for which no AAXML or TAXML schema has the same set of runs). In both cases, we use the fact that, over data-free schemas (fixed vocabulary), the runs accepted by automata and by Past-Tree-LTL formulas are closed under equivalence with respect to homomorphism. (homomorphisms apply here just to the forests of the instances and ignore the mappings eval). Indeed, this follows from the fact that allowed transitions between instances depend in both cases only on the patterns satisfied by the instances, and satisfaction of patterns is preserved under homomorphism of data-free instances. Note that this is not the case for GAXML, as illustrated by the example constructed in the proof of the next lemma.

LEMMA 5.2. GAXML ֒→ (id,id) AAXML. In other words, there exists a GAXML schema S|γ for which there is no AAXML schema S ′ |A such that S|γ ≡ S ′ |A.

PROOF. We describe a GAXML schema S|γ for which no AAXML schema has the same set of runs. The DTD of S imposes that its initial instance consists of a tree of root r with five children labeled by function calls to some internal functions f 1 , ..., f 4 and end. The argument query of each f i yields f for some internal function f and its return guard is false. The argument query of f produces some internal function g and its return guard is also false. Fig. 10: Instances I, J and K.

Function g returns the empty message (its return guard is true). Function end has an empty argument query and a return guard that is false. In γ c , all call guards are true except for g that is: end must not be active. Consider a prerun ρ 0 of S|γ resulting from the following transitions:

(1) call all functions f i , 1 ≤ i ≤ 4;

(2) call all functions f in the workspaces of the f i ;

(3) call 2 of the functions g in the workspaces of the functions f;

(4) call function end.

Clearly, this sequence of transitions is allowed by S|γ. Let I be the resulting instance. Now consider two transitions from I:

(i) return one of the two running calls to g, yielding instance J;

(ii) activate one of the two calls !g, yielding instance K.

Note that transition (i) is allowed by S|γ whereas (ii) is not because the guard of g is false in I. Let ρ J and ρ K be the extensions of ρ 0 with transition (i) and (ii), respectively. Note that ρ J and ρ K are homomorphically equivalent. The instances I, J and K are represented in Figure 10. Now suppose that there is an AAXML schema S ′ |A equivalent to S|γ. Since ρ J is a prerun of S|γ, it must also be a prerun of S ′ |A. Since runs satisfying AAXML schemas are closed under homomorphic equivalence, ρ K must also be a prerun of S ′ |A. This contradicts the equivalence with S|γ, since ρ K is not a prerun of S|γ.

Finally, note that it is necessary to have four initial functions f 1 , . . . , f 4 , yielding four occurrences of g in I. Indeed, if there are only three initial functions (so three 3 g's in I) , it is easy to see that the instances K and J are no longer guaranteed to be homomorphically equivalent.

Observe that the proof does not use relative patterns in guards.

LEMMA 5.3. GAXML ֒→ (id,id) TAXML. In other words, there exists a GAXML schema S|γ for which there is no TAXML schema S ′ |θ such that S|γ ≡ S ′ |θ.

PROOF. This follows by a similar observation as above: the set of runs definable by a Past-Tree-LTL formula is closed under equivalence with respect to homomorphism (without data values). This is because the satisfaction of a Past-Tree-LTL formula by a prerun is determined by the patterns satisfied by each instance in the prerun, and homomorphic instances satisfy the same patterns. The details are straightforward and omitted.

The next two lemmas state that GAXML cannot simulate AAXML or TAXML. In both cases, we use the fact that the history of the computation is not recorded in the current instance.

LEMMA 5.4. AAXML ֒→ (id,id) GAXML. In other words, there exists an AAXML schema S|A for which there is no GAXML schema S ′ |γ such that S|A ≡ S ′ |γ.

PROOF. Consider the following AAXML schema S|A. The DTD of S enforces that the initial instance consists of one of the function calls !f or !g under the root, where f and g are non-continuous internal functions. There are no data values. A call to f returns !g and a call to g never returns (so all runs are blocking). The automaton A enforces that we start in a state q init (with formula true), move to q call-f (with formula stating that ?f is a child of the root), move to q end (with formula true). This imposes that if we start with f, we call f, receive !g, then call g and block; but if we start with g, we immediately block. Now suppose towards a contradiction that there exists a schema S ′ and a guard constraint γ so that S ′ |γ ≡ S|A. Observe that in the run starting from f under the root, we reach an instance I that consists only of g under the root and then g is called in I. Now use I as an initial instance. Then the guard of g allows calling g from I, a contradiction. LEMMA 5.5. TAXML ֒→ (id,id) GAXML. In other words, there exists a TAXML schema S|θ for which there is no GAXML schema S ′ |γ such that S|θ ≡ S ′ |γ.

PROOF. The proof is the same as for AAXML ֒→ (id,id) GAXML, where instead of the automaton A we use a constraint θ ∈ T stating that the initial instance has !f under the root.

LEMMA 5.6. TAXML ֒→ (id,id) AAXML. In other words, there exists a TAXML schema S|θ for which there is no AAXML schema S ′ |A such that S|θ ≡ S ′ |A.

PROOF. The proof is based on the fact that a Past-Tree-LTL formula can "remember" a data value even after it disappears from the instance, using an existentially quantified global variable, while this is not possible for an automaton (all parameters of a state must occur in the present instance). Specifically, consider a TAXML schema S|θ whose initial document consists of a single function call !f under root r. A call to f produces a workspace consisting of an external function call !g that returns a single data value. The function f returns a call to another external function !h that again returns a single data value. The Past-Tree-LTL formula θ imposes the following sequence of calls and returns:

(1) f is called (2) g is called (3) g returns a value u (4) f returns !h (5) h is called and returns the same value u returned in step (3). Now suppose that there exists an AAXM L schema S ′ |A describing the same sequence. The state of A after step (4) cannot have any parameters, since the current instance has no data value. Then A cannot impose that the data value returned in step ( 5) is the same as that in (3). Thus, no such automaton exists.

The next lemma uses the fact that LTL is weaker than automata on finite words [START_REF] Libkin | Elements of Finite Model Theory[END_REF]].

LEMMA 5.7. AAXML ֒→ (id,id) TAXML. In other words, there exists an AAXML schema S|A for which there is no TAXML schema S ′ |θ such that S|A ≡ S ′ |θ.

PROOF. We use the following AAXML schema S|A . The DTD states that the root is r and it has two children, namely !f or ?f and !g or ?g. The function f is a continuous internal function that returns an empty answer. The function g never returns. From q init , the automaton enforces that f is called, returns its answer, and is called again to get to a state q choice . In that state, one can either return f and go back to q init or call g and get to state q block . Consider the four possible instances of S. We denote them by the symbols a (children of r are !f, !g), b (they are ?f, !g), c (they are ?f, ?g), and d (they are !f,?g). Observe that the set of preruns of S|A is the prefix-closure L of the language {(ab) 2n c | n ≥ 0}. Note that L cannot be expressed by FO on words because it is not counter free [START_REF] Diekert | First-order definable languages[END_REF], so it can neither be expressed by LTL [START_REF] Libkin | Elements of Finite Model Theory[END_REF]]. Now suppose, towards a contradiction, that there exists a Past-Tree-LTL schema S ′ |θ equivalent to S|A. We show that we can construct from S ′ |θ an LTL formula ϕ that defines L. Apart from θ itself, the formula ϕ must capture the valid transitions among instances, as well as the DTD ∆ of S ′ . Thus, ϕ is the conjunction of the following LTL formulas: ψ θ obtained from θ by replacing each pattern p by the disjunction of the symbols corresponding to the instances satisfying p (for example, for the pattern stating the existence of ?f, the disjunction is b ∨ d), and replacing Past-LTL operators with LTL ones; ψ ⊢ is the conjunction of constraints on consecutive instances defining the transition relation ⊢ (for example, one such constraint is G(a → X(b ∨ d))); ψ ∆ Note that ∆ must allow instances a, b, c that appear in runs of S|A. Thus, ∆ defines either {a, b, c}, the set of instances of S ′ |θ, or {a, b, c, d}.

If ∆ defines {a, b, c}, then ψ ∆ is G(a ∨ b ∨ c). If ∆ defines {a, b, c, d}, then ψ ∆ is true. Let ϕ = ψ θ ∧ ψ ⊢ ∧ ψ ∆ .
It is easy to check that ϕ is an LTL formula defining L, contradiction.

This concludes the proof of Theorem 5.1.

Comparison with projection views

Given the negative result of Theorem 5.1, we next consider simulation relative to views allowing more leeway in the simulating system. Specifically, the view remains the identity on the simulated system, but allows the simulating system to use additional data and functions. We refer to the latter as a projection view and denote the class of projection views by π. Specifically, let S be a BAXML schema and Σ 0 (Σ 0 ⊂ Σ) and F 0 (F 0 ⊂ F) be subsets of the tags and functions of S (the visible symbols) such that, in every instance satisfying the DTD of S, whenever a node has tag a ∈ Σ 0 , none of its descendants has a label in Σ 0 or in F 0 . Note that, since the view used for the simulated schema is the identity, the visible tags and functions used in the simulation results are precisely those of that schema.

The projection4 π Σ0,F0 ([S]) is defined as follows. For a state I of [S] (and for any instance), the projection is obtained by removing all nodes whose label is a tag not in Σ 0 or a function not in F 0 and their descendants. We also remove the workspaces whose corresponding function calls have been projected out. The projection of an event !f(F ) is ǫ for f ∈ F 0 and !f(π Σ0,F0 (F )) for f ∈ F 0 , and similarly for ?f(F ). In addition, all projections preserve the special events init and block. The projection view is defined in the same way for BAXML augmented with constraints (GAXML, AAXML, and TAXML).

Our main result is that, with projection views, the powerful control mechanisms of GAXML can be simulated by BAXML alone. For AAXML and TAXML, we need a minor restriction forbidding the presence of sibling calls to the same external function, i.e. the occurrence of two sibling nodes labeled ?f, for the same external function f (this can be enforced by the DTD). We denote these restrictions by AAXML sib and TAXML sib . THEOREM 5.8. W ֒→ (id,π) BAXML for W ∈ {GAXML, TAXML sib , AAXML sib }.

PROOF. We describe the three simulations needed to establish the result.

Simulation of GAXML by BAXML

We present the simulation in two stages: first, we demonstrate that the return guards can be removed from GAXML schema without losing expressiveness. Then, we demonstrate that a GAXML schema where all return guards are true can be simulated by a BAXML schema. We denote the set of GAXML schemas whose return guards are set to true by GAXML no-ret . LEMMA 5.9. GAXML ֒→ (id,π) GAXML no-ret . PROOF. We explain how we can remove the return guards of GAXML schemas. Consider a GAXML schema S|γ. Due to Lemma 2.5 (Composition Lemma), and the fact that the set π of views is closed under composition, it is sufficient to show how to eliminate the return guards one function at a time.

Let f be an internal function of S|γ. Intuitively, we simulate the check of the return guard of a workspace of ?f using a function call !check-rg f in the same workspace, whose call guard checks the return guard of f. We wish to ensure the following property, while maintaining the requirements of w-bisimulation:

(+) the call to ?f can return only if the call to !check-rg f has been activated in its workspace (signaling satisfaction of the return guard) and no other transition visible in the workspace occurred in the meantime.

Enforcing (+) involves several subtleties, which we discuss in some detail in this first simulation proof. The same subtleties are addressed implicitly in the other simulations.

We explain how (+) is enforced in several stages. We begin with a first attempt, that will have to be refined in order to satisfy the requirements of w-bisimulation.

Recall that, by definition, the answer of a call to f cannot be returned as long as the workspace of the call to f contains active function calls. Consider the following modification of the GAXML schema S|γ:

(i) the set of functions is augmented with an internal, non-continuous function check-rg f with empty answer, whose call guard checks that the return guard of f holds, and that the workspace of the call to f contains no active function calls; (ii) the argument query of f is modified so that its initial workspace contains a call to !check-rg f ; (iii) for every function g, its call guard γ c (g) is replaced by γ c (g) ∧ α where α checks that, if !g occurs in a workspace of f, then !check-rg f also occurs in the same workspace (this can be done with relative patterns); (iv) the return query of f is augmented with the rule a f //!check-rg f -→ {error} (v) the set of constraints of S is augmented to forbid the occurrence of error. (vi) the return guard of f is set to true;

Let S 1 |γ 1 be the resulting GAXML no-ret schema. It easily seen that, whenever the answer of a call to f is returned in S 1 |γ 1 , the return guard of f in S|γ is satisfied. Indeed, (ii) ensures that !check-rg f occurs initially in the workspace of the call, (iv) and (v) ensure that the answer cannot be returned before !check-rg f is activated, the call guard of check-rg f ensures that the return guard of f in S|γ holds when check-rg f is activated, and (iii) together with the call guard of check-rg f ensure that no transition may occur in the workspace after check-rg f is activated.

While S 1 |γ 1 seems to satisfy the intuition of the desired simulation, it is not quite satisfactory. Consider the view V ∈ π for which the visible functions and tags are those of S, and consider the workflow systems [S|γ] and V ([S 1 |γ 1 ]). We would like to have a w-bisimulation relation B from [S|γ] to V ([S 1 |γ 1 ]). In particular, if [S|γ] has no blocking states, neither should V ([S 1 |γ 1 ]). However, the above construction may yield blocking states in [S 1 |γ 1 ] (so also in V ([S 1 |γ 1 ])), even if no such states occur in [S|γ]. This is due to the fact that the activation of !check-rg f nondeterministically freezes the workspace in its current state. Although the return guard of f is satisfied at that point, the constraints of S may prohibit the instance resulting from the return, thus inhibiting it. This may result in a blocking state in [S 1 |γ 1 ], even if no such state occurs in [S|γ].

To deal with the issue of blocking states, we must allow unblocking a workspace in which !check-rg f has been activated, and repeating the process. Note that we cannot simply make !check-rg f continuous, because the presence of !check-rg f prevents the return of the answer, by (iv). Instead, we can introduce an intermediate function, say rg-ok f , that is returned by check-rg f and can in turn generate another call !check-rg f . In more detail, let rg-ok f be an internal, non-continuous function, and modify check-rg f so that its answer returns the call !rg-ok f . The call guard of !rg-ok f is true and its answer returns a call !check-rg f . Let S 2 |γ 2 be the resulting schema. It is clear that S 2 |γ 2 prevents the undesired blocking encountered in S 1 |γ 1 .

However, we are not quite done, because the repeated trials yield in V ([S 2 |γ 2 ]) infinite sequences of silent transitions. These are due to infinite alternations of calls to !check-rg f and !rg-ok f , without any intermediate visible function call or return. This violates the definition of w-bisimulation for [S|γ] and V ([S 2 |γ 2 ]), since no such sequences exist in [S|γ] (in fact [S|γ] has no silent transitions at all). To circumvent this problem, we wish to ensure that some visible transition occurs between each return of the answer to ?check-rg f (yielding !rg-ok f ) and the next call to !rg-ok f . Since attempts at returning the answer to f need only be made when no visible active calls exist in the workspace, it is sufficient to require the occurrence of at least one visible function call return. To detect such returns, we use a new auxiliary function return, and modify the answer queries of all visible functions so that every answer contains a call to !return. To allow visible functions to be activated following the activation of !check-rg f , we remove the requirement imposed by (iii) above that their call guards require the presence of !check-rg f . However, now we must ensure that the answer of f is not returned until !check-rg f is again activated, checking that the return guard of f still holds. This can be done by inhibiting the return of the answer of f while !return is present, similarly to (iv)-(v) above. In more detail, we modify S 2 |γ 2 as follows:

(a) add the function return as an internal, non-continuous function returning the empty answer, and whose call guard requires the presence of !check-rg f ; (b) modify the return queries of all visible functions so that their answer includes a call !return; (c) restore the original guards of visible functions (undo (iii) above); (d) modify the call guard of rg-ok f to require the presence of !return; (e) augment the call guard of check-rg f to require the absence of !return or ?return. (f) add to the answer query of f the rule:

a f //!return f -→ {error}
Let the resulting schema be S 3 |γ 3 . Note that, due to (b), the new function return affects the entire instance, not just the workspaces of f. When it occurs outside a workspace of f, its call guard cannot hold, so the call is never activated. Its presence is however harmless because it does not cause transitions and is not visible in V ([S 3 |γ 3 ]).

We claim that S|γ and V (S 3 |γ 3 ) are now w-bisimilar. More precisely, let B be the relation from the nodes of [S|γ] to those of V ([S 3 |γ 3 ]) defined as follows. Recall that both [S|γ] and V ([S 3 |γ 3 ]) have as root the empty run, which we denote ρ ∅ . The relation B is the smallest relation satisfying the following:

-B(ρ ∅ , ρ ∅ ) -if B(s 1 , q 1 ) and s 1 e → s 2 , q 1 e → q 2 for some visible event e, then B(s 2 , q 2 ).

From the above discussion it follows that B is a w-bisimulation relation. This completes the proof. Example 5.10. To illustrate the construction in the previous proof, we consider the following simple example. Let S|γ be a GAXML schema, and suppose an instance I is reached that contains an activated call to a function f. Suppose the workspace of f consists of just one unactivated function call to a visible function, !g. We assume that the return guard of f and the call guard of g are satisfied by I. We next show that GAXML without return guards can be simulated by BAXML.

!check-rg f , !g ?check-rg f , !g !rg-ok f ,!g • • • return of f !rg-ok f , ?g !return, !rg-ok f !return, ?rg-ok f !return, !check-rg f ?return, !check-rg f !check-rg f return of return call of return return of rg-ok f call of rg-ok f return of g call of g return of check-rg f ?g, ?check-rg f ! return, ?check-rg f !return, !rg-ok f !return, ?rg-ok f !return, !check-rg f ?return, !check-rg f !check-rg f return of return call of return return of rg-ok f call of rg-ok f return of check-rg f return of g call of g call of check-rg f
LEMMA 5.11. GAXML no-ret ֒→ (id,π) BAXML.

PROOF. Let S|γ be a GAXML no-ret schema. We construct a BAXML schema S ′ that simulates S|γ. Intuitively, we check the guard of f by adding to the argument query of f additional rules that check satisfaction of each pattern of γ c (f) and insert a corresponding tag in the workspace, signaling satisfaction of the pattern. Specifically, for each pattern P of γ c (f), we add to the argument query of f a rule P → {sat P } where sat P is a new tag. Note that, if P is a relative pattern, self is mapped to the same node when it is viewed as the body of a relative query. Finally, the DTD of the workspace is modified to allow only subsets of tags sat P corresponding to truth assignments satisfying γ c (f). This ensures that !f can only be activated if γ c (f) is satisfied. Remark that this construction works only for internal functions, as external function calls do not produce a workspace. To deal with external functions, the schema is first modified to ensure that every new occurrence of an external call !f is accompanied by a sibling !lock f . This is done using the DTDs (including those of answers to external functions), as well as by modifying the answer queries of internal functions by adding to every occurrence of !f a sibling !lock f .

The function !lock f is internal, non-continuous, and returns the empty answer. It has several roles:

-checking satisfaction of the guard of f; this is done as above, using the workspace of lock f ; -checking that the static constraints would be satisfied after the activation of !f. This is done by rewriting the constraints in order to allow mapping ?f to ?f or to ?lock f and !f to !lock f .

Static constraints require that !f can only be activated if it has a sibling ?lock f , ensuring that its guard and constraints are true. In addition, ?lock f acts as a lock disallowing any action other than the activation of the sibling !f. Specifically, we must prevent the following actions as long as ?lock f is present:

-activation of another call !lock g for an external function g; this is prevented by having the call guard of each function lock g prohibit the existence of any other active call ?lock h in the instance. -activation of an internal function; to prevent this, we add a new, internal, non-continous function activated and modify the argument queries of all internal functions in order to force the inclusion of a call !activated in their answer. A constraint prohibits the simultaneous occurrence of !activated and ?lock f in the instance. The function activated returns the empty answer. -return of a function call; similarly to the proof of Lemma 5.9, we add a new internal, non-continuous function return and modify the return queries of internal functions and the return DTD's of external functions so that their answers contain a call !return. A constraint prevents ?lock f and !return from occurring simultaneously. The function return returns the empty answer.

Let S ′ be the resulting BAXML schema. Let V ∈ π be the projection view for which the visible tags and events are those of S (and recall that init and block, are always visible). As in the proof of Lemma 5.9, let B be the smallest relation from the nodes of [S|γ] to those of V ([S ′ ]) satisfying the following:

-B(ρ ∅ , ρ ∅ ) -if B(s 1 , q 1 ) and s 1 e → s 2 , q 1 e → q 2 for some visible event5 e, then B(s 2 , q 2 ).

A straightforward case analysis shows that B is a w-bisimulation relation from [S|γ] to V ([S ′ ]). The only non-trivial aspect of the simulation concerns the functions lock f . It is critical to note that every activation of !lock f leads to a successful call to !f (so a visible event). This ensures that no extraneous blocking occurs in S ′ , and also that there are no infinite chains of silent transitions. Thus, B is indeed a w-bisimulation.

In summary, we have shown that GAXML ֒→ (id,π) GAXML no-ret and GAXML no-ret ֒→ (id,π) BAXML By Lemma 2.6 it follows that GAXML ֒→ (id,π) BAXML. Since this is the first application of the lemma, we explain it in detail. The lemma is applied with

V 1 = V 2 = id and V = V 3 = π. Since π = id • π we have that GAXML ֒→ (V1,V2•V) GAXML no-ret and GAXML no-ret ֒→ (V2,V3) BAXML. By Lemma 2.6, GAXML ֒→ (V1,V3•V) BAXML. Since π • π = π it follows that GAXML ֒→ (id,π) BAXML.

Simulation of AAXML sib by BAXML

Let S|A be an AAXML sib schema with functions F 0 and tags Σ 0 . We outline the construction of a GAXML schema S ′ |γ that simulates S|A relative to projection views. Since GAXML can be simulated by BAXML relative to projection views, and since projection is coarser than the identity on GAXML, Lemma 2.6 implies that AAXML sib can be simulated by BAXML.

Without loss of generality, we can assume that the static constraints of S consist just of a DTD. Indeed, the data constraints can be easily pushed into the pattern automaton A. As described in the proof of Theorem 4.4, the satisfaction of an automaton A by a prerun can be checked incrementally by maintaining the states of the automaton reachable in the prerun, together with the valuations of their parameters. The simulation by a GAXML schema essentially implements the same incremental check. Thus, S ′ |γ must alternate the simulation of events of S|A (function calls and returns) with validity checks and updates of the state and valuation information of A. The simulation is quite intricate and we outline the main points, providing intuition on the more subtle aspects.

The representation and maintenance of the state and valuation information for A is straightforward. We use a subtree with root states, and one child !q for each state q of A. Valuations of Xq are kept in adjacent subtrees, each with root label V q . The current valuations are marked by a function !current (internal, noncontinuous, with empty answer). An evaluation of !q returns a new set of valuations, also subtrees with root V q , but now marked with another function !new. The update is completed by having the functions !current vanish and the functions !new turn into !current. One update round is controlled by a function update whose activation enables the update and blocks all transitions not involved in the update. Other locks ensure that update can be activated only when the simulation of one transition of S is completed. We can also enforce that the update round is performed only once between transitions.

The main difficulty in the simulation concerns the function calls and returns, and their timing relative to the update round outlined above. Specifically, the following raise technically intricate points:

(i) ensuring that validity of a function call or return is checked for each event (in particular, this requires preventing multiple transitions skipping intermediate validity checks and state/valuation updates) (ii) checking validity of a candidate event of S with respect to the DTD and A without actually carrying out the event (in particular, one must prevent infinite branches of ǫ-transitions caused by unsuccessful guesses of the next valid event)

The sequencing needed for (i) and (ii) is enforced by a locking mechanism implemented by auxiliary functions. Before outlining the main aspects of the simulation, we make some useful technical remarks.

Valid automata transitions vs. static constraints Given the current state/valuation information for A and a next instance I of S, validity with respect to A of the transition to I can be expressed in S ′ by a formula ϕ next . The formula ϕ next is the disjunction ∨ q,q ′ ψ next (q, q ′ ), where q and q ′ are states of A, and ψ next (q, q ′ ) checks that q is a current state, the formula Υ(q ′ ) holds, and the equality constraints between some valuation of Xq and a possible next valuation of Xq ′ provided by Υ(q ′ ) are satisfied. Note that ϕ next is not directly expressible as a static constraint in S ′ , because these are Boolean combination of independent patterns, whereas ϕ next uses parameterized patterns sharing free variables. To overcome this gap, some pre-processing is needed for each transition. Specifically, for a formula ϕ next with free variables X, candidate valuations for X are generated and the patterns in ϕ next are augmented so that X is bound in all patterns to the same valuation. The generation of the candidate valuations depends on the action leading to the transition (we omit the details). This reduces evaluation of ϕ next to evaluation of a Boolean combination of independent patterns, so a static constraint of S ′ . In the following, we will use for simplicity ϕ next as a static constraint, bearing in mind that its evaluation requires the above pre-processing phase. Parameterized queries used in the automaton A yield another difficulty for the initial state. To ensure that the initial document satisfies the parametrized query of the initial state, we assume that there is only one valuation of the initial state represented in the initial document. This way the parametrized query can be simulated by a Boolean combination of patterns. The other valuations are built at the beginning of the simulation by the activation and the return of a function call !init-valuation.

Rewriting patterns The patterns used in S|A have to be rewritten when used in S ′ |γ. Indeed, since an instance I ′ of S ′ contains the corresponding instance I in S|A, a pattern can be satisfied in I ′ and not in I. The main problem is due to descendant branches and the wildcard used in patterns. To resolve this, each tag in Σ 0 used in I ′ is adorned with a child labeled real. The patterns are rewritten using these markings, to ensure that each pattern of S|A used in S ′ |γ is mapped to nodes in I rather than to hidden nodes used in the simulation.

Rewriting queries

The simulation introduces new data values in the trees. These data values can be matched by patterns in the queries, such as q = * //$x. To avoid this, we first ensure by static constraints that each node labeled by a tag appearing in the projected trees has a child labeled real, as explained previously. Queries are rewritten in order to access only data values accessible using nodes having a child labeled real.

Extending GAXML with global return guards In our simulation, we allow return guards that can check a global property of the instance. This is an extension of GAXML, since in GAXML return guards of function calls are only able to check properties of the workspace. In our context, we can simulate global return guards. This is done by adding to the workspace of each function f using a global return guard γ r (f) a function check-return-guard f . The call guard of this function is γ r (f). The new local return guard of f simply checks that check-return-guard f has returned. This works in the context of our simulation because we only use it on reachable instances I of S|γ in which satisfaction of γ r (f) implies that the return of the corresponding call to f leads to the only valid transition. Note that otherwise, a reevaluation of check-return-guard would have to be done after each other valid transition by using a mechanism like in the proof of GAXML without return guard.

We next outline the simulation of the events of S|A, making use of the above observations. In all cases, the simulation involves the following steps:

(1) Acquire a lock for a function call or return. The lock initiates an attempt to carry out the associated event.

(2) Check that the event corresponding to the lock would result in a valid transition of S|A.

(3) In the affirmative, the locked event is carried out and the lock released. Otherwise, the lock is also released, but in a manner that prevents another locking attempt before a valid event occurs. This prevents infinite branches of ǫ-transitions.

We now describe the specific simulation used for the activation of a function call, the return of an internal function call, and the return of an external function call.

Activation of a function call

The activation of an internal function !f is controlled using a sibling function !lock f . As described above, this has a dual role: it acts as a lock, and it checks whether the activation of !f would result in a transition allowed by the automaton. If so, it returns a function call !activate-f. Otherwise, it returns !notactivate-f. The call !f cannot be activated unless !activate-f occurs as a sibling. The functions !lock f and !activate-f also prevent other transitions from occurring during the attempt to activate !f. To this end, one can guarantee that there is at most one node labeled ?lock f , (for some f) in an instance, i.e. at most one lock. This is enforced by the guard of lock f . Moreover, no active function call can return its answer while ?lock f , !activate-f, or ?activate-f occur. As described in the proof of Lemma 5.11 , it is easy to ensure that every occurrence of !f is always accompanied by a sibling !lock f following each visible transition.

To ensure that !f is activated whenever !activate-f is activated, the guard of activate-f ensures that this function cannot be called while it still has a sibling !f. The function call !notactivate-f ensures that !lock f cannot be called more than once between two valid transitions. It is activated during the maintenance phase and returns !lock f (needed for the next attempt to call !f, following another transition). The constraints impose that activate-f handshakes with the lock for the maintenance of the states and valuations.

Figure 12 summarizes the possible sequences of activations in the simulation of an internal call to f. The role of the function w f,a will be explained shortly. The nodes represent the functions that occur as siblings of the node labeled ?f or !f. . The possible sequences for an external call are the same except the function w f,a is replaced by certificate f,a .

Return of an internal function call

We describe the simulation in several stages. The basic locking mechanism is simple. The lock initiating an attempted return of a function call ?f is implemented using a function !lock w present in the workspace. If the call return to ?f would result in a valid transition, the lock is released and the result is returned. Otherwise, the lock is released and another function !wait is activated in order to inhibit any locking attempt until another transition has been successfully completed.

Checking validity of the call return is much more complex. It is carried out using the workspace of an auxiliary function check f,a that is a sibling to ?f (here a is the tag of the parent of ?f, needed to check the DTD). A difficulty is to make sure the activated occurrence of check f,a is indeed a sibling of the call ?f whose workspace is locked (recall that patterns cannot detect the link between a call and its workspace). Assume for the moment that this is achieved. Then check f,a works as follows. First, it generates in its workspace a copy of its sibling subtrees, (these are "almost" isomorphic copies of the originals, keeping sufficient information for checking validity, see below). This copy is initiated by the activation of copy-sibling appearing in the workspace of check f,a . Next, it generates in the same workspace the answer to the locked call ?f. In the following stage, four functions are used to test satisfaction or violation of the DTD (ok-dtd and notok-dtd) and the automaton constraint (ok-A and notok-A) by the result. Specifically, for the first two the test is done using the DTD of S ′ and for the last two using their guards. To test satisfaction of the automaton constraint using guards, the formula ϕ next has to be rewritten into a disjunction of formulas, each of which decomposes the patterns into a part that applies to the workspace of check f,a (mimicking the subtree rooted at the parent of the call ?check f,a , labeled a) and another to the rest of the instance. If the result is positive (the transition is valid) then a flag ok-return is turned on in the workspace of ?f. The guards and constraints

!f !lock f !f ?lock f !f !w f,a !activate-f ?f !w f,a !activate-f ?f ?w f,a !activate-f !f ?w f,a ?activate-f !f ?w f,a return of activate-f call of activate-f call of w f,a call of f return of lock f !f !notactivate-f return of lock f call of lock f
Fig. 12: Some of the actions for the simulation of the activation of the call to f then force the answer to the call ?f to be returned, and ?check f,a returns the empty answer. If the result is negative, the function !wait is activated in the workspace of ?f (see above), and These functions are used to allow a new check of this function after a valid transition as detailed be.

We next explain how to generate !check f,a as a sibling of the call ?f whose workspace is locked. The process starts at the time when !f is activated. We ensure that each function call !f has as a sibling a call !w f,a (where a is the tag of the parent of the function call). When the call to !f is made, its workspace includes a function !init that uniquely marks the most recent function call (and later vanishes). Additionally, a new identifier α is generated in the workspace of ?f (more on this in the next paragraph). Then the function !w f,a is called and copies the identifier α from the workspace of ?f marked by !init. Note that the only function call !w f,a without a sibling !f is the sibling of the most recently activated call ?f. Once the simulation of the call to !f is completed, !init vanishes but the workspaces of ?f and ?w f,a remain linked by the identifier α. When the return of the call ?f is simulated, the call ?w f,a sharing the same id α with the workspace of ?f returns as answer the desired function call !check f,a . If due to a lock the return of f is disallowed, the call to !w f,a has to be activated again. The function check f,a returns the function calls !w f,a and !reinitialize. The second function ensures that its sibling !f has as sibling !w f,a after the reinitialization.

The identifier α in the previous paragraph can easily be generated by an external function that returns a new value. If one wishes to avoid using external functions in the simulation, the identifier can be represented by a chain of calls to two internal functions, encoding the binary representation of an integer. The bookkeeping is more complicated in this case, since comparing identifiers is no longer an atomic operation. In particular, identifiers have to be destroyed and reconstructed (details omitted). Moreover, the identifiers have to be refreshed after each valid transition to ensure that the size of each instance of the simulation remains polynomial in the size of the current instance.

Recall that one of the roles of !check f,a is to copy the relevant sibling subtrees of ?f. We explain briefly how this is done. We enforce that each tag of Σ 0 has a child function call !copy-to. As remarked earlier, the copy performed loses some information. The loss concerns the exact number of sibling calls ?g to an internal function g. Indeed, it is not possible to fully replicate this information because of the limitations of patterns. Fortunately, multiple occurrences of sibling calls to the same function are not relevant when they occur as internal nodes in sibling subtrees of ?f. Thus, only one representative of such calls is copied. This does not affect the simulation, since trees with activated function calls cannot be merged, and patterns cannot count such occurrences. For calls ?g occurring as siblings of ?f, their number is relevant to satisfaction of the DTD after the call return, but only up to the maximum integer used in the DTD of S. The number of occurrences up to this maximum can be signaled using additional function calls whose activation is constrained by the DTD of S ′ . For example, the DTD may stipulate that a function !eq (?g=m) may be activated iff the number of occurrences of siblings ?g is m.

Copying a tree is done by mutually recursive calls between functions residing in the source tree (copy-to, in-progress, copy-values-to, done-to) and in the target tree (copy-from, copy-values-from, done-from). The copy is done in a depth-first manner. The copy-to indicates the parent node to copy. The function call !copy-from copies this node with child labeled !copy-from. The function call !in-progress indicates that copying is in progress for the subtrees of the parent node of this call. The function call copy-values-to indicates that the function calls and the sibling values of this function have to be copied. It implies that the subtrees are entirely copied, which is signaled by the function !done. The copy of the function calls is tricky, since copying the activated function calls has to be done before the others (to guarantee that partially copied subtrees are not merged). The function calls !done-from and !done-to are reinitialized to !copy-to after each valid transition.

Figure 13 summarizes the tree of actions done to check the return of a call. At each node, we represent the function calls siblings of the call ?f, the function calls in the workspace of ?f and the function calls in the workspace of check f,a when it is in the simulation.

Return of an external function call This is the most subtle part of the simulation. Observe first that it is not possible to take a lock using a marker returned by an external function call ?f, because two calls to ?f at different locations in the document may return exactly the same forest and be indistinguishable by the constraints of the GAXML schema. Moreover, it is not possible to take a lock prior to the return of ?f, because one cannot know if ?f can return an answer satisfying the constraints (recall that this is undecidable, see proof of Theorem 4.6). If a lock is taken when ?f cannot return, this leads to a blocking run in an instance of S ′ |γ whose projection in S|A is not blocking, which violates the definition of simulation. Instead, the idea of our simulation is to use, for every call ?f to an external function, an associated sibling call to an internal function certificate f,a such that:

(i) if ?f may return, then ?certificate f,a may return a flag !return f . The function !return f compels ?f to return and also acts as a lock preventing other transitions until the next cleaning stage. (ii) the call ?certificate f,a may remain activated until the next cleaning stage, in which case ?f is not allowed to return. During the cleaning stage, the call ?certificate f,a returns and is reactivated.

Note that, even if ?f can return, ?certificate f,a does not necessarily return, unless the return of ?f is the only possible next transition. Otherwise, the cleaning stage may be reached without a return of ?certificate f,a or ?f, by simulating some other transition. If ?certificate f,a does not return and the cleaning stage is not reached, then the run is blocking, both in S|A and in S ′ |γ.

We next elaborate on (i). To mimick ?f, the function certificate f,a uses in its workspace an external control function fake f . The workspace also contains additional information so that ?fake f may return in the context of the workspace iff ?f may return in the context of its original location. Specifically, the workspace contains a copy of the sibling subtrees of ?f (this is done as in the previous simulation). In addition, it contains information on the evaluation of the patterns in ϕ next on the portion of the current instance excluding the siblings of ?f. The partial evaluations of the patterns together with the siblings allow expressing within the workspace constraints on the return of ?certificate f,a that are equivalent to those on the return of ?f (the DTD and valid transition in A). This ensures that ?fake f may return iff ?f may return. If ?fake f returns, then ?certificate f,a returns the flag !return f as desired. To prevent multiple returns to ?fake f at different locations in the document, the answer to ?fake f contains a flag !return-fake-f that is not allowed to appear twice in the document. To ensure this, the workspace of ?certificate f,a also contains a unique id (generated by an external function). A constraint forbids two occurrences of !return-fake-f with distinct workspace id's. Note that the id technique could not be used to implement directly a lock for the return of ?f, because such an id could not be erased from the instance and this could lead to faulty simulations. Indeed, the id's could inhibit merging of subtrees whose projections would otherwise be merged.

(?f ?w f,a ), (!lockw, !wait) (?f ?w f,a ), (?lockw,!wait) (?f !check f,a ), (?lockw,!wait) (?f ?check f,a ), (?lockw, !wait), (!ok-dtd, !notok-dtd, !ok-A, !notok-A) (?f ?check f,a ), (?lockw, !wait), (?ok-dtd, !notok-dtd, !ok-A,!notok-A) (?f ?check f,a ), (?lockw, !wait), (ok-dtd, !notok-dtd, !ok-A,!notok-A) (?f ?check f,a ), (?lockw, !wait), (ok-dtd, !notok-dtd, ?ok-A,!notok-A) (?f ?check f,a ), (?lockw,!wait), (ok-dtd, !notok-dtd, ok-A,!notok-A) (?f ?check f,a ), (ok-return), (ok-dtd, !notok-dtd, ok-A,!notok-A) (?f ), (ok-return) (!return) return of f return of check f,a return of lockw return of ok-A call of ok-A (?f ?check f,a ), (?lockw, !wait), (ok-dtd, !notok-dtd, !ok-A,?notok-A) (?f ?check f,a ), (?lockw, !wait), (ok-dtd, !notok-dtd, !ok-A,notok-A) (?f ?check f,a ), (?lockw,?wait), (ok-dtd, !notok-dtd, !ok-A,notok-A) (?f !w f,a !reinitialize), (?lockw,?wait) (?f ?w f,a !reinitialize), (?lockw,?wait) (?f ?w f,a ?reinitialize), (?lockw,?wait) (?f ?w f,a ), (?lockw,?wait) (?f ?w f,a ), (?wait) return of lockw Finally, if ?certificate f,a does not return during the current round, its workspace is reconstructed during the cleaning stage in order to reflect changes in the instance.

Figure 14 summarizes the tree of actions performed to check the return of an external call. At each node, we represent the function calls occurring as sibling of the call ?f, then the function calls in the workspace of certificate f,a when it exists.

Example 5.12. We illustrate the main elements of the above simulation using a simple example. Consider the following AAXML schema S|A. Its static constraints consist of the following DTD:

r -→ |b| = 1 ∧ |c| = 1 b -→ |a| = 1 ∨ |!f| = 1 ∨ |?f| = 1
S has one internal function f, whose argument and return queries always produce a single node labeled a. The automaton A has three states, s 0 , s 1 , s 2 , with no associated variables. The initial state is s 0 and there are transitions from s 0 to s 1 and from s 1 to s 2 . The formula associated with the initial state s 0 checks for the presence of !f , the formula for s 1 checks for the presence of ?f and the formula for s 2 checks for the absence of ?f. Thus, the only possible sequence of events is the activation of !f and the return of ?f. We describe how the two transitions are simulated by the GAXML schema S ′ |γ with global return guards constructed in the proof. The initial AAXML instance is the following:

r b !f
The shape of the initial document for S|A is ensured by a pattern associated with s 0 (having the same tree representation as the instance above). The corresponding initial instance for the GAXML schema S ′ |γ is the following: This is enforced by the static constraints of S ′ . For readability, we omit in figures the function calls copy-to introduced in the full proof to facilitate copying trees in the simulation (they should appear under every visible node). Also, all visible nodes are circled. r real states

! s 0 ! s 1 ! s 2 ! init-valuation Vs 0 !current b real !f ! lock f
The simulation consists of the following steps.

(1) Call and return of !init-valuation. This function returns the valuations for the variables associated with s 0 .

In this example, it returns the empty valuation, since s 0 has no associated variables. r real states

! s 0 ! s 1 ! s 2 Vs 0 !current b real !f ! lock f
(2) Call and return of !lock f . This function takes a lock on the system and checks if the activation of !f is allowed by the constraints of S|A. In our example, the activation is possible and the call to lock f returns !activate-f. r real states

!s 0 !s 1 !s 2 Vs 0 !current b real !f !w f,b !activate-f (3) Call of !f. r real states !s 0 !s 1 !s 2 Vs 0 !current b real ?f !w f,b !activate-f af real a real !lockw !wait !init !identifier
(4) The next few steps prepare the return of the call ?f. First, a fresh identifier for the workspace is created by a call to the external function identifier. For more clarity, we use an integer to represent the identifier. (7) Call of activate-f. This internal function can return only if there is no function call to current and there is some function call to new. This completes the simulation of the activation of f. It is followed by the simulation of the transition of the automaton, from s 0 to s 1 . (16) Using the copied subtrees, the siblings of check f,b and the return of f built from the initial workspace, it is possible to check the correctness of the return of f for the DTD and the transition constraints. In our example, both are satisfied after the return. Then, !ok-dtd and ok-A are called and return ok-dtd and ok-A, respectively (details omitted). This completes the simulation of the two transitions.

simulated by AAXML sib or TAXML sib , it is enough to consider a BAXML schema that produces an instance with two sibling calls to the same external function. By definition, such a schema cannot be simulated by AAXML sib or TAXML sib .

For AAXML and TAXML, we have the following.

THEOREM 5.14. AAXML ֒→ (id,π) TAXML and TAXML ֒→ (id,π) AAXML.

PROOF. We first show that AAXML ֒→ (id,π) TAXML. Let S|A be an AAXML schema with functions F 0 and tags Σ 0 . The broad lines of the simulation of AAXML by TAXML are similar to the simulation of AAXML sib by GAXML. As in the latter case, the TAXML system must enforce an alternation of transitions and maintenance of the state/valuation information for A. This is done by a locking mechanism enforced by auxiliary functions, much like in the simulation by GAXML. We omit the similar details and focus on returns of external function calls.

Each function call notifies its return by a function call !safe-r that belongs to its answer (this can be enforced for external functions by their DTD). The function !safe-r works as a lock. To ensure that two sibling functions calls ?f do not return consecutively, the TAXML formula imposes that no two consecutive instances contain a function call !safe-r. In particular, this requires the activation of !safe-r f in the instance following its first occurrence. The validity of the return with respect to A is checked, as in the simulation by GAXML, by the constraint ϕ next , whenever !safe-r f occurs (note that ϕ next can be used directly in the Past-Tree-LTL formula).

We next show that TAXML ֒→ (id,π) AAXML. To this end, we use a variant of AAXML, denoted by AAXML * . The automaton model of AAXML * differs from AAXML as follows:

(i) the automaton is equipped with final states, and a prerun must lead to some final state in order to be accepted, (ii) the state variables are the same for all states and remain unchanged in each transition, and (iii) the state variables range over the active domain of the entire prerun which is the input to the automaton, rather than just the last instance leading to that state.

We first show that TAXML can be simulated by AAXML * , then show how AAXML * can be simulated by AAXML.

From TAXML to AAXML * Let ξ = ∃ Xϕ( X) be a Past-Tree-LTL formula. Recall that each such formula is obtained from a propositional Past-LTL formula φ with propositions P in which each proposition p ∈ P is replaced by a Boolean combination of parameterized patterns ψ p . Using a variant of the algorithm of [START_REF] Vardi | An automata-theoretic approach to linear temporal logic[END_REF] for finite words, one can construct a finite-state automaton A φ whose alphabet consists of the truth assignments to P , that is equivalent to φ. From this we can obtain an AAXML * automaton A ξ equivalent to ξ as follows.

-For each truth assignment σ to P , let γ σ be the Boolean combination of tree patterns obtained from the propositional formula ∧ σ(p)=1 p ∧ σ(p)=0 ¬p by replacing each p by ψ p -For each state q of A φ, A ξ has one state (q, σ) for each outgoing transition from q labeled σ, and transitions are induced by those in A φ. The state formula for (q, σ) is γ σ . The state variables (which are all the same) equal X. -The final states of A ξ are those of the form (q, σ) where q is final in A φ.

It is easily seen that the AAXML * automaton A ξ is equivalent to ξ.

From AAXML * to AAXML We explain informally the main points in the simulation of AAXML * by AAXML. Consider an AAXML * specification S * |A * . We describe an AAXML specification S|A that simulates it. Recall the differences (i)-(iii) between the AAXML * and AAXML automata. The simulation by S|A is similar to the maintenance of the set of reachable states and valuations, used in the simulation of AAXML by GAXML. Dealing with (i) and (ii) is straightforward. To account for the final states, S|A must check that at each transition, one of the reachable states is final. The fact that state variables are the same and do not change in A * is easily enforced in A using equalities among variables of consecutive states. The most delicate part of the simulation concerns (iii), i.e. the difference in the active domain semantics for the two models. Indeed, at any given transition in the prerun, state formulas are evaluated on the active domain of the entire prerun. This includes values occurring in past instances and values occurring in future instances (introduced by external functions). We discuss both in turn.

Dealing with past values is fairly straighforward. It is sufficient to ensure that at any point, the current active domain contains all values of previous instances in the prerun. To this end, we use a new internal, continuous function collect, whose role is to maintain the cumulative active domain of the instances in the prerun. More precisely, the DTD of S * is modified so that !collect or ?collect must occur under a node labeled values (a new tag) which in turn occurs under the root. The argument query of collect produces all data values in the current instance, and the answer query returns all data values in its workspace. The pattern automaton A * is modified as follows. For each state p that has at least one outgoing edge, we introduce two new intermediate states, p 1 and p 2 , with the same number of associated variables as p. The role of p 1 and p 2 is to force an activation of !collect, followed by a return of ?collect, before any other transition. The state formula of p 1 is Υ ′ (p)(X p /X p1 ) ∧ α 1 , where Υ ′ (p)(X p /X p1 ) is obtained from Υ(p) by modfiying each pattern in order to force all matchings to avoid the subtree rooted at values, and by replacing the variables X p with X p1 , and α 1 checks the existence of ?collect. There is an edge from p to p 1 and δ(p, p 1 ) makes all variables X p1 equal to X p . Similarly, the state formula of p 2 is Υ ′ (p)(X p /X p2 ) ∧ α 2 , where α 2 checks the existence of !collect (which means that the call to collect has returned) and δ(p 1 , p 2 ) makes all variables X p1 equal to X p2 . Finally, for each state q of A * such that δ(p, q) is defined, δ(p 2 , q) is obtained from δ(p, q) by replacing X p with X p2 . It is clear that the intermediate states ensure that the cumulative active domain of the prerun up to the current instance is found under the node labeled values after each visible transition is simulated.

It now remains to deal with new values introduced in future instances of the prerun, relative to the current instance. These may arise from answers to external function calls. We make use of the previous construction ensuring that the cumulative active domain of the prerun up to the current instance is maintained under the distinguished node labeled values. Handling future values is trickier, because the semantics requires taking these into account in previous transitions. Dealing with this requires augmenting the state/valuation maintenance algorithm. Specifically, S|A must decide if the current transition would be allowed had A * been run from the beginning on the active domain extended with the new values. In order to do this incrementally (without re-running the automaton on the extended domain), A must maintain some additional information summarizing the reachable states and valuations, where the latter include values outside the current prerun. In order to do this, the key observation is that a positive pattern with a free variable X cannot be satisfied for any value of X not in the current instance. Let @ be a new data constant, representing an arbitrary value outside the current active domain. Consider a valuation ν of the state variables X into the cumulative active domain augmented with @. Let us call a valuation indefinite if it maps at least one variable to @, and definite otherwise. We can define the satisfaction of a tree pattern P (ν(Y )) in a BAXML instance, where Y ⊆ X, as follows: if ν(Y ) is definite, then satisfaction is defined as usual; otherwise, P (ν(Y )) is not satisfied. This extends to satisfaction of Boolean combinations of tree patterns, so of state formulas. The maintenance algorithm is now be extended to keep states together with definite and indefinite valuations. When a transition from instance I and state p to instance J and state q is simulated, the following is done: (i) the set of definite valuations for p is augmented by adding, for each indefinite valuation ν of X p , all valuations ν • ν ′ , where ν ′ maps @ to any value in the active domain of J that is not in the cumulative active domain up to I; (ii) the maintenance algorithm computes in the usual way the set of possible definite valuations for q, using the set of definite valuations computed in (i) for p; (iii) a new set of indefinite valuations is computed for q, using J and Υ(q)(X q ).

Let S|A be the AXML schema implementing the extended maintenance algorithm. It is clear that S|A simulates S * |A * .

From the proof of Theorem 5.14 we have the following. COROLLARY 5.15. TAXML sib ֒→ (id,π) AAXML sib and TAXML sib ֒→ (id,π) AAXML sib .

PROOF. It can be checked that the simulations described in the proof of Theorem 5.14 preserve the sibling restriction on external functions.

The proofs of the above results provide insight into the simulations of the various languages, and in particular highlight the power of imposing control using static constraints. In terms of the cost of each simulation, several parameters can be considered: (i) the blowup in the schema size, (ii) the blowup in the instance size, (iii) the number of silent transitions needed to simulate a single transition. For the simulations considered here, the blowup in the schema size varies from polynomial to exponential, the blowup in the instance size from polynomial with respect to the instance to polynomial with respect to the entire prerun, and the number of silent transitions from constant to polynomial in the prerun (for fixed schemas). The costs for various simulations are spelled out in more detail in Figure 15.

The difficulty of simulating AAXML and TAXML with sibling external function calls by BAXML (or GAXML) lies in the fact that the constraints of AAXML and TAXML must be checked after every transition, and GAXML cannot prevent multiple returns from sibling external function calls that skip validity checks. Indeed, as shown below, this difficulty cannot be circumvented. THEOREM 5.16. W ֒→ (id,π) GAXML for W ∈ {TAXML, AAXML}.

Conversely, one may be interested in observing certain characteristics of the states in the tree of runs, ignoring event information. Once again, this can be captured by coarser views than (id, π), so the same simulation results hold.

BAXML AND TUPLE ARTIFACTS

In the previous section, we compare the expressiveness of several workflow languages centered around the common core provided by BAXML. In this section, we illustrate how views can be used to reconcile models that are otherwise incomparable. For this, we use the views framework to compare BAXML workflows with tuple artifacts workflows, a variant of IBM's Business Artifacts, which uses relational databases as its underlying model. The main result is that BAXML can simulate tuple artifacts. Indeed, tuple artifacts can be seen as views of BAXML. We will also see that tuple artifacts cannot simulate BAXML even with respect to coarse views retaining just the traces of service and function calls.

We first review informally the tuple artifact model, as presented in [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]. We denote the model by TA. We assume an infinite data domain D. An artifact system consists of a set of artifacts and a set of services acting on the artifacts. An artifact consists of an artifact tuple and a set of state relations. In addition, an artifact system has an underlying database shared by all artifacts and services, that is fixed throughout a run of the system.

Each service causes a modification of one or several current artifacts. Intuitively, the focus is on the evolution of the artifact tuples, while the state relations are used to carry auxiliary information needed by the services. A service consists of the following:

-a pre-condition, which is an FO formula on the set of artifacts of the system and the underlying database; -a post-condition, which is an FO formula on the set of artifacts and the database, defining, for each artifact tuple, the values allowed in the next instance; free variables range over the infinite domain D, so they may take new values not present in the current instance; -for each state relation, two FO formulas defining the sets of tuples to be inserted and deleted from the state. The formulas take as input the current artifact instance and the database, and are interpreted with active domain semantics. Thus, their result is always finite.

Services are applied non-deterministically. At any given time, a service can be applied to the current instance if its pre-condition holds and if the post-condition is satisfiable. Thus, there are two forms of non-determinism in a transition: one stemming from the choice of service, and another from the choice of values for the next artifact tuples, among those satisfying the post-condition. A run of an artifact system is a sequence of consecutive instances together with the name of the service applied at each transition. (For initial instance, we take any instance whose artifact states are empty.) As for BAXML, blocking runs are extended by repeating forever the last configuration, with the corresponding transitions labeled by the special event block. See [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF] for a detailed example of an artifact system.

The Tuple Artifact Model

We provide the definition of the tuple artifact model, adapted from [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]. A relational database schema D consists of a finite set of relation symbols with specified arities. The arity of relation R is denoted by arity(R). An instance, or interpretation, over a database schema, is a mapping associating to each relation symbol R of the schema a finite relation over D, of arity arity(R). We assume familiarity with First-Order logic (FO) over database schemas. Given a schema D, L D denotes the set of FO formulas over D. If ϕ(x) is an FO formula with free variables x, and ū is a tuple over D of the same arity as x, we denote by ϕ(ū) the sentence obtained by substituting ū for x in ϕ(x). Note that, since D is infinite, an FO formula ϕ(x) may be satisfied by infinitely many tuples ū over D (so may define an infinite relation). Finiteness and effective evaluation can be guaranteed by using the active domain semantics, in which the domain is restricted to the set of elements occurring in the given instance (sometimes augmented with a specified finite set of constants in D, which by default is empty). For an instance I, we denote its active domain by adom(I). Unless otherwise specified, we assume active domain semantics for quantified variables and unrestricted semantics for the free variables of a formula.

The artifact model uses a specific notion of class, schema and instance, defined next. We also refer to an artifact instance of class C as artifact instance, or simply artifact when the class is clear from the context or irrelevant.

Note that, according to (2) in Definition 6.6, services do not update the database contents (thus, the database contents is fixed throughout each run, although it may of course be different across runs). Instead, the data that is updatable throughout a run is carried by the artifacts themselves, as attribute and state relations. Note that, if desired, one can make the entire database updatable by turning it into a state. Also observe that the distinction between state and database is only conceptual, and does not preclude implementing all relations within the same DBMS.

We next define the notion of run of an artifact system Γ = A, Σ . An initial instance of Γ is an artifact instance over A whose states are empty. Definition 6.7. A prerun of an artifact system Γ = A, Σ is a finite sequence ρ = {(ρ i , σ i )} 0≤i≤n where each ρ i is an artifact instance over A and each σ i is a service, such that:

ρ 0 is an initial instance of Γ; -for each i > 0, ρ i-1 σi -→ ρ i .

We say that a pre-run is blocking if its last configuration has no possible successor. As for BAXML, blocking runs are extended by repeating forever the last configuration, with corresponding transitions labeled block. A run is an infinite sequence {(ρ i , σ i )} i≥0 in which either every finite prefix is a prerun, or the run is obtained by extending a blocking prerun by repeating forever the last configuration with transitions labeled block. For an artifact system, the associated workflow system is defined from the set of runs analogously to BAXML. In particular, the states are artifact instances, and the events are services causing state transitions or the special event block.

Workflow system semantics. The workflow system semantics of artifact systems is defined from its runs analogously to the semantics of BAXML, GAXML, AAXML, and TAXML (Section 5). For each artifact system Γ, the nodes of its associated workflow system are the finite prefixes of runs of Γ. The root is the empty prefix, and its state label is the empty instance. The state label for each node other than the root is the last instance in the prefix. For each non-root node ν, there is an edge labeled σ from ν to node ν ′ if ν ′ extends ν with a single instance obtained by application of the service σ. The root has an outgoing edge to each node consisting of a prefix of length one, labeled by a distinguished event init. Thus, transitions from the root provide the initial instances of runs, and the infinite paths starting from children of the root correspond to the runs of Γ. Because of the semantics of blocking runs, each path is extensible to an infinite path.

Simulation of Tuple Artifacts by BAXML

We denote the tuple artifact model by TA. More precisely, TA is the set of all artifact system specifications, with workflow system semantics.

In order to simulate TA with BAXML, we must define views that render the two compatible. For TA, we simply take the identity views id. For BAXML, we consider schemas of a special form, that represent the artifact instances. . A relation R with attributes A 1 , . . . , A m is naturally represented in BAXML by a subtree rooted at R, satisfying the DTD below, denoted by ∆ R :

R → |tup R | ≥ 0 tup R → ∧ m i=1 |A i | = 1 A i → |dom| = 1
Given an artifact instance, we refer to the contents of the artifact relations, consisting of single tuples, as the artifact tuples. Each service of the artifact system is modeled in BAXML by a corresponding function with the same name. The call of a service is captured in BAXML by a call to the corresponding function.

We define the class of views used in the simulation, denoted by V TA . Each view is defined relative to a set R of tags and a set F of function names. Intuitively, the tags in R are meant to label subtrees encoding relations, as above. We say that a BAXML workflow system is R-relational if for each R ∈ R there exists a DTD ∆ R of the above shape such that each BAXML instance labeling a non-root state of the workflow system contains exactly one occurrence of each tag R in R, and the subtree rooted at R satisfies ∆ R . The view V R,F in V TA is defined as follows. If the workflow system is not R-relational, then all state labels are mapped to ∅ and all edge labels are mapped to ǫ (these workflow systems are irrelevant because they are not used in the simulation). If the workflow system is R-relational, the view is defined as follows:

-BAXML instances labeling non-root states are mapped to the relational instance represented by the subtrees rooted at labels in R; -events consisting of calls to functions in F are mapped to the name of the function; -the init event is preserved; and, -all other events are mapped to ǫ. The main result is the following. THEOREM 6.8. TA ֒→ (id,V TA ) BAXML. In other words, for each TA system Γ there exists a BAXML schema S and a view V ∈ V TA such that [Γ] ∼ V ([S]).

PROOF. We show that TA can be simulated by GAXML. This suffices, because BAXML can simulate GAXML. In more detail, suppose that TA ֒→ (id,V TA ) GAXML. By Theorem 5.8, GAXML ֒→ (id,π) BAXML. By Lemma 2.6, (since V TA = id• V TA ) TA ֒→ (id,π•V TA ) BAXML. From the definitions of π and V TA , it is clear that π • V TA ⊆ V TA . Thus, TA ֒→ (id,V TA ) BAXML.

We sketch the simulation of TA by GAXML for artifact systems with only one artifact class with a single state and database relation, and a single service. This is sufficient to capture the salient elements of the simulation. As discussed in [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]], an arbitrary TA system can be easily represented by such a restricted system. Suppose the artifact system has an artifact tuple with k attributes A 1 , . . . , A k , a database relation DB, and a state relation S. The unique service has pre-condition π, postcondition ψ, and state formulas ϕ + S and ϕ - S . Relations will be represented in the simulating GAXML system in the standard way, by subtrees of bounded depth (see Section 6). The database relation is a fixed subtree in the main document, while the state and artifact tuple are represented in workspaces of function calls, which facilitates updating their values. More specifically, the state is represented and updated using the workspaces of two function calls that alternate between carrying the current state and computing the next state.

An application of the service requires simulating the following:

(1) evaluating the pre-condition π on the database, current state and current artifact tuple.

(2) evaluating the FO formulas ϕ + S and ϕ - S and generating the new S in the workspace of one of the two functions mentioned above.

(3) non-deterministically generating a new candidate artifact tuple and verifying satisfaction of the postcondition ψ.

The bookkeeping needed to enforce the above sequencing can be straightforwardly done with auxiliary functions. There are two delicate points: the evaluation of an FO formula, and simulating (3) so that all qualified next artifact tuples can be generated and failed attempts do not lead to spurious blocking or infinite chains of ǫ-transitions. Recall that in general there are infinitely many new candidate artifact tuples, because new values can come from the infinite domain D.

Evaluating an FO formula. We first elaborate on the evaluation of FO formulas. Recall that the formulas ϕ + S , ϕ - S , and π are interpreted with active domain semantics. Consider an FO formula written using ∧, ¬, ∃. The formula is evaluated by structural recursion on its syntax tree. Given standard representations of the result of two subformulas, it is easy to compute the relation obtained by applying ∧ and ∃. Applying ¬ is trickier. For conciseness, we illustrate how to compute the complement of a unary relation P with respect to the active domain (this can be easily extended to arbitrary arity). The relation P is represented by a subtree with root labeled P , satisfying the DTD P → |dom| ≥ 0.

The complement is constructed as follows. First, a call to a function !check P generates the current active domain, where each value is adorned with two functions !in-P and !not-in-P. More precisely, the argument query of !check P is shown in Figure 17 and its initial workspace is of the form shown in Figure 18. In this example, a data value is denoted by α i (the role of !p will be explained shortly). can simulate tuple artifacts whereas the converse is false. To compare these very different models, we used again the views framework to render them compatible. This illustrates the usefulness of the view-based framework to reconcile seemingly incomparable workflow models.

  Fig. 1: A BAXML document.

  Fig. 2: Two patterns

Fig. 3 :

 3 Fig. 3: Example of a relative query

  Example 3.1. We continue with our running example. The function Bill used in Figure1is specified as follows. It is internal and non-continuous. The argument query is the query in Figure3. The return query of Bill is: makes sense assuming that the function Invoice returns a tree of the form:

Fig. 6 :

 6 Fig. 5: An instance with an eval link

Fig. 7 :

 7 Fig. 7: (i) Pattern whose negation forbids two activated calls and (ii) ensuring satisfaction of [A i ] ⊆ [A j ]

Fig. 8 :Fig. 9 :

 89 Fig. 8: Call guards of Reject and Deliver.

  i) checks that the call to Invoice in the workspace of Bill has been activated: aBill ? Invoice -Υ(ie) checks that the call to Invoice in the workspace of Bill has returned a payment: aBill Payment -Υ(pe) checks that the call to Bill has returned a payment: Main Paid-Υ(d) checks that the call to Deliver is activated and the amount brought by Bill is the same as the price of the item that has been ordered. de) checks that the call to Deliver has been returned. r) checks that the call to Reject is activated and the amount brought by !Bill is different from the price of the item that has been ordered: re) checks that the call to Reject has been returned for the MailOrder (there is no active call to Reject): .

-

  ψ !Bill checks that the call to Bill is not activated: Main !Bill -The formula ψ ?Bill checks that the function call to Bill is activated: Main ?Bill -The formula ψ ?Invoice checks that the call to Invoice is activated: aBill ? Invoice -The formula ψ Payment checks that the call to Bill has been returned: aBill Payment -The formula ψ Paid checks that the call to Bill has been returned: Main Paid -The formula ψ !Deliver,!Reject checks that the calls to Deliver and Reject are not yet activated: Main !Reject !Deliver -The formula ψ ?Deliver checks that the call to Deliver is activated: Main ?Deliver -The formula ψ γc(Deliver) checks that the call guard of Deliver is true: ψ ?Reject checks that the call to Reject is activated: Main ?Reject -The formula ψ γc(Reject) checks that the call guard of Reject is true: The formula ψ finish-Deliver checks that Deliver has returned by checking that the function calls to Deliver and Bill no longer appear in the document:

Fig. 11 :

 11 Fig. 11: Tree illustrating some of the possible actions in the simulation of the return of the function f in Example 5.10

  Figure 11 gives an overview of the possible sequences of function calls and returns in the simulation of S|γ by S 3 |γ 3 .

  Fig.13: Some of the actions in the simulation of the return of the call to the internal function f

  A call of !w f,b copies the identifier of the workspace a f using the fact that !init occurs in it. The workspace of f is cleaned by activating and returning the function call !init.

Definition 6. 1 .

 1 An artifact class is a pair C = R, S where R and S are two relation symbols. An instance of C is a pair C = R, S , where (i) R, called attribute relation, is an interpretation of R containing exactly one tuple over D, and (ii) S, called state relation, is a finite interpretation of S over D.

Fig. 18 :

 18 Fig. 17: The query of check P acheck P

  In the general simulation, the function calls !s 0 , !s 1 , !s 2 are activated and returned to create new valuations for the associated variables. Since in our example there are no variables associated to states, the empty valuation corresponding to the state s 1 is represented by the subtree V s1 with the function call !new. The preceding valuations are marked as deleted. This is done by the call and return of the function current. In the example, the only such call occurs under the node labeled V s0 .(10) ?activate-f can return only if there are no function calls to current but there is some function call to new. The next steps simulate the return of ?f. The first step is the activation of !lock w in the workspace of f. The function call w f,b associated with f returns by using the identifier of the workspace of f and the fact that the workspace of f has an activated function call ?lock w . The function call check f,b is activated to check that the return of f would be compatible with the constraints given by S|A (the tag ā is an invisible clone of a). First, the sibling subtrees of check f,b are copied in its workspace using the function copy-to under each visible tag and the function copy-forest in the workspace of check f,b (recall that the functions copy-to are omitted in the figures for readability, but are present under every visible node). In our example, the forest is empty.

	r !current Vs 0 aw f,b identifier 1 (8) r real states !s 0 !s 1 !s 2 real states !s 0 !s 1 !s 2 Vs 0 !current aw f,b real Vs 1 !new identifier 1 (9) r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !new real aw f,b identifier r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !new real aw f,b identifier 1 (11) The simulation of the first transition is completed by calling and returning the function call !new in order to obtain b ?f ?w f,b ?activate-f af real a real !lockw !wait identifier 1 aactivate-f b real ?f ?w f,b ?activate-f af real a real !lockw !wait identifier 1 aactivate-f b ?f ?w f,b ?activate-f af real a real !lockw !wait identifier 1 aactivate-f b ?f ?w f,b af real a real !lockw !wait identifier 1 a function call !current. r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !current b real ?f ?w f,b af real a real !lockw !wait identifier 1 aw f,b identifier 1 (12) r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !current b real ?f ?w f,b af real a real ?lockw !wait identifier 1 aw f,b identifier 1 alock w (13) r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !current b real ?f !check f,b af real a real !lockw !wait identifier 1 alock w real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !current b real ?f ?check f,b af real a real !lockw !wait identifier 1 acheck f,b !ok-dtdd !notok-dtd !ok-A !notok-A !copy-forest ā identifier 1 alock w (15) r real states !s 0 !s 1 !s 2 Vs 0 Vs 1 !current b real ?f ?check f,b af real a real !lockw !wait identifier 1 !ok-dtd !notok-dtd !ok-A !notok-A ā identifier 1 (14) r acheck f,b alock w
	1

  The function call ?lock w returns the tag ok-return because of the presence of the labels ok-A and ok-DTD and using the common identifier found in the workspaces of ?f and ?check f,b . The function call ?f returns because of the presence of the label ok-return in its workspace and the absence of ?check f,b . The update of the state of the automaton begins as before. The function return plays the role of activate-f previously. It can return only if there is a call to new but no call to current. The functions !s 0 , !s 1 , !s 2 are called and returned to obtain an empty valuation of s 2 . The previous valuation is removed by calling and returning !current.

	(18) The function call ?check f,b returns.
				r							af
	real		states					b		real	a	ok-return	!wait	identifier
	!s 0	!s 1	!s 2	Vs 0	Vs 1	real	?f		real	1
					!current
	(19) r
	real		states						b
	!s 0	!s 1	!s 2	Vs 0	Vs 1	real	!return	a
					!current					real
	(20) r							areturn
	real		states						b
	!s 0	!s 1	!s 2	Vs 0	Vs 1	real	?return	a
					!current					real
	(21) r							areturn
	real		states						b
	!s 0	!s 1	!s 2	Vs 0	Vs 1	Vs 2		real	?return	a
				r		!new					real	af
	real (22) The function call ?return returns. states				b		real	a	!lockw	!wait	identifier
	!s 0	!s 1	!s 2	Vs 0 r	Vs 1	real	?f	?check f,b	real	1
	real		states	!current			b
	!s 0	!s 1	!s 2	Vs 0	Vs 1	acheck f,b Vs 2	real	a		alock w
		ok-dtdd	!notok-dtd	ok-A !new		!notok-A ā identifier real
	1 (23) The update of the state is completed by calling !new, which returns !current.
	r Vs 0 states (17) r real !s 0 !s 1 !s 2	Vs 1	Vs 2		real	b	a	af
	real		states			!current	b	real	real	a	ok-return	!wait	identifier
	!s 0	!s 1	!s 2	Vs 0	Vs 1	real	?f	?check f,b	real	1
					!current
						acheck f,b
		ok-dtdd	!notok-dtd	ok-A		!notok-A ā identifier
											1
										33

Composition is applied left-to-right.

There is no (I ′ , e ′ ) where (I 0 , e 0 ), ..., (In, en)(I ′ , e ′ ) is a prerun of S.

A DTD is recursive if there is a cycle in the graph that has an edge from tag a to b if the DTD allows b to label a child of a node labeled a.

Recall that [S] denotes the semantics of S, i.e. the workflow system it defines.

Recall that init and block are always visible events.

This work has been partially funded by the European Research Council under the European Community's Seventh Framework Programme (FP7/2007-2013) / ERC grant Webdam, agreement 226513. It also received partial support from the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599. V. Vianu was supported in part by the National Science Foundation under grant IIS-0916515. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that

Simulation of TAXML sib by BAXML

This follows from the simulation of AAXML sib by GAXML and from Theorem 5.14, noting that the simulation of TAXML by AAXML does not introduce sibling calls to the same external function.

This concludes the proof of Theorem 5.8.

Remark 5.13. Theorem 5.8 shows that BAXML and GAXML can simulate AAXML sib and TAXML sib with respect to projection views. The converse is obviously false. Indeed, to see that BAXML (or GAXML) cannot be

PROOF. We first show that there exists an AAXML schema with external functions that cannot be simulated by a GAXML schema relative to a projection view. Intuitively, if there are several sibling active function calls to the same external function, the GAXML schema is not able to impose that only one function call returns before the states of the automaton are updated and validity of the transition is ensured.

The AAXML schema S|A is the following. We describe the shape of a run. The initial instance is a tree rooted at r with one child labeled by a continuous function !g. The function !g returns an external, non-continuous function call !f. Repeated calls to g and f (in alternation) generate an unbounded number of sibling calls ?f. Each function f returns a label a. The automaton further imposes that no more than one answer to ?f be returned in a run.

We show that there is no GAXML schema simulating S|A. Assume towards a contradiction that there exists such a schema S ′ |γ. Let M be the maximum integer used in the DTD of S ′ . We exhibit a prerun that is valid for S ′ |γ, but whose projection is not valid for S|A. First, let ρ = (I 0 , e 0 ) • • • (I m , e m ) be a prerun for S|A in which I m has M + 1 occurrences of ?f and e m is the only return of a call ?f occurring in ρ. Let I be the instance resulting from the return of another call ?f of I m (let e be this event). Note that ρ is a valid prerun of S|A whereas ρ.(I, e) is not. Nonetheless, we show that ρ.(I, e) is the projection of a prerun of S ′ |γ. Since S ′ |γ simulates S|A and ρ is a prerun of S|A, there exists a prerun of S ′ |γ with a subsequence

In particular, I ′ im-1 contains M + 2 calls to ?f, I ′ im contains M + 1 calls to ?f, and (since calls ?f are visible), I ′ im is obtained from I ′ im-1 by the return of a call to ?f, consisting of some forest F . We claim that S ′ |γ allows the transition from I ′ im to I ′ in which another call to ?f returns the same forest F . Indeed, because in the BAXML semantics isomorphic subtrees are reduced, the two occurrences of F are merged so the only difference between I im and I ′ is that I im has M + 1 calls ?f whereas I ′ has M such calls. Since M is the maximum integer used in the DTD of S ′ , and I im satisfies the DTD, so does I ′ . Similarly, I im and I ′ satisfy the same tree patterns because the two instances are homomorphic to each other. Thus, I ′ satisfies all static constraints of S ′ . Since external function returns have no guards, the transition is valid in S ′ |γ. However, the projection of I ′ is I and, as we have seen, ρ.(I, e) is not a valid prerun of S|A. This contradicts the existence of S ′ |γ.

The fact that TAXML cannot be simulated by GAXML follows from the fact that AAXML can be simulated by TAXML (Theorem 5.14) and AAXML cannot be simulated by GAXML. The difficulty is the same as in the above proof.

The simulation results of this section relative to projection views are summarized in Figure 16 (single arrows indicate simulation only in one direction, and double arrows indicate mutual simulation).

Comparison with coarser views

We have focused in this section on simulation relative to projection views (id, π). The results obtained turn out to be quite powerful. Indeed, by Lemma 2.5, the positive results extend to any views that are coarser than projection views. For example, one may wish to focus on the sequence of events (function calls and returns, together with their arguments), ignoring state information. This information can be captured by composing the views in id and π with a view V that is the identity on events and maps every state to a fixed constant. By Lemma 2.5, the positive simulation results shown in Figure 16 continue to hold relative to (id • V, π • V ). Definition 6.2. An artifact schema is a tuple

where each C i = R i , S i is an artifact class, DB is a relational schema, and for all i = j, C i , C j , and DB have no relation symbols in common.

By slight abuse, we sometimes identify an artifact schema A as above with the relational schema

An instance of an artifact schema is a tuple of class instances, each corresponding to an artifact class, plus a database instance: Definition 6.3. An instance of an artifact schema

Again by slight abuse, we identify each instance

Let A be an artifact schema and DB A its relational schema. Given an artifact instance over A, the semantics of formulas in L A is the standard semantics on the associated relational instance over DB A .

We now define the syntax of services. It will be useful to associate to each attribute relation R of an artifact schema A a fixed sequence xR of distinct variables of length arity(R). Definition 6.4. A service σ over an artifact schema A is a tuple σ = π, ψ, S where:

where S is a state relation of A, ϕ + S (x) and ϕ - S (x) are L A -formulas with free variables x s.t. |x| = arity(S). As seen below, the formulas ϕ + S (x) and ϕ - S (x) are used to define updates to the state relation S when the service is applied. The formula ϕ + S (x) defines the tuples to be inserted, and ϕ - S (x) the tuples to be deleted (see below). If a formula is not provided for a state relation S, the set of tuples to be inserted or deleted is taken to be empty. Definition 6.5. An artifact system is a pair Γ = A, Σ , where A is an artifact schema and Σ is a non-empty set of services over A.

We next define the semantics of services. We begin with the notion of possible successor of a given artifact instance with respect to a service. Definition 6.6. Let σ = π, ψ, S be a service over artifact schema A. Let A and A ′ be instances of A. We say that A ′ is a possible successor of A with respect to σ (denoted by A σ -→ A ′ ) if the following hold:

(1) A |= π;

(2) A ′ |DB = A|DB (A and A ′ agree on all relations in DB);

(3) A, ν |= ψ, where ν is the valuation of the free variables of ψ mapping xR to ūR for each attribute relation R of A; (4) for each state relation S of A and tuple ū over adom(A) of arity arity(S),

where ϕ + S (ū) and ϕ - S (ū) are interpreted under active domain semantics, and are taken to be false if the respective rule is not provided. Thus, the new state relation S is obtained by inserting the tuples defined by ϕ + S and deleting those defined by ϕ - S , with deletion given priority over insertion in case of conflict, except for tuples previously in S, which are preserved in case of conflict. The functions in-P and not-in-P are internal. The call guard of in-P, shown in Figure 19, verifies that the value adjacent to the call is in P , whereas the guard of not-in-P checks that the value is not in P (so the guard of not-in-P is the negation of the guard of in-P). The functions in-P and not-in-P return, respectively, a label in and a label not-in. The role of the function !p is dual. First, its guard ensures that for each value, one of its siblings !in-P or !not-in-P has been called and has been returned. To this end, its guard forbids the presence of two siblings !/?in-P and !/?not-in-P. Second, its argument query computes the complement of P , by collecting the values with a sibling not-in. The argument query of p is shown in Figure 20.

Generating the new artifact tuple. Like the state, the artifact tuple is represented and updated using the workspaces of two functions that alternate between carrying the current value and computing the new value of the artifact tuple. Recall that generally there are infinitely many candidates for the next artifact tuple, since the free variables of the post-condition range over the infinite domain D. Observe that satisfaction of the post-condition is invariant under the following equivalence relation on k-tuples over D: a 1 , . . . , a k ≡ b 1 , . . . , b k iff for all i, j:

To each equivalence class corresponds a type specifying the values for the coordinates that belong to the active domain, and the equality type for the coordinates whose values are not in the active domain. It is straightforward to nondeterministically construct a relation containing one representative tuple for each equivalence class. Specifically, internal function calls are used to generate the values of the coordinates in the active domain, and external functions to generate values for the coordinates outside the active domain. The equality type for the latter is imposed by constraints. In addition, each tuple is adorned with a function call whose role is to evaluate the post-condition ψ for the tuple, returning ok in the affirmative and not-ok in the negative. Since ψ is in FO, this can be done similarly to the above. The functions evaluating ψ for each tuple are called non-deterministically, and a simple locking mechanism ensures that (i) the functions are evaluated completely one at a time, and (ii) function activations are blocked in the current round as soon as one of them returns ok. The new artifact tuple is the unique one marked ok. It can be easily checked that every candidate tuple can be generated in this manner by some computation path. If there is no such tuple, the artifact system blocks, and so does the simulation. Thus, BAXML can simulate TA. In fact, since the view used for TA is the identity, tuple artifacts themselves can be seen as views of BAXML systems. The simulation yields a BAXML schema polynomial in the TA schema, BAXML instances polynomial in the TA instances, and polynomially many silent transitions (with respect to the current instance), to simulate in BAXML one transition of TA.

Conversely, we will show that, in a strong sense, TA cannot effectively simulate BAXML. We use coarse views that retain just the names of function calls in BAXML and of service calls in TA (modulo a projection). Such views are natural because the traces of function and service calls largely capture the sequencing of events central to workflows. We will prove a strong negative result for such views. Intuitively, the problem in simulating BAXML with TA is due to the fact that BAXML can read a large structure (for example an entire relation represented as an XML document) by a single function call. On the other hand, tuple artifacts can only read one tuple at a time, so the simulation requires a loop. This loop may lead to an infinite sequence of ǫ-transitions (imagine a denial-of-service attack in which the attacker keeps sending new tuples). But if no such sequence of ǫ-transitions occurs in the BAXML system, this is not a correct simulation.

More precisely, the views we use are defined as follows:

States. For both BAXML and TA, all states are mapped to a constant state (so all information about the states is lost); Events. For BAXML, active calls ?g are mapped to ǫ and calls !g are mapped to g or to ǫ (so some function calls can be hidden); for TA, a service σ is mapped to σ or to ǫ (so again, some services can be hidden).

We denote the above class of views of BAXML systems by V fun and of TA systems by V serv .

Recall that the definition of simulation does not require effective construction of the simulating schema (even though all our positive simulation results are constructive). We can show that one cannot effectively construct a TA specification simulating a given BAXML schema, with respect to the above views. THEOREM 6.9. There is no algorithm that, given as input a BAXML schema W 1 and a view

). Moreover, this holds even for BAXML schemas of bounded depth.

PROOF. The proof is based on a reduction from the implication problem for functional and inclusion dependencies (FDs and IDs), known to be undecidable. Specifically, we consider instances of the implication problem of the form ∆ |= f , where ∆ is a set of FDs and IDs, and f an FD. We consider a BAXML schema S whose initial instance consists of a single external function !e under the root. The function returns a tree representing an arbitrary finite relation, of the form shown in Figure 6. Specifically, each tuple is adorned with one function !f τ for each ID τ in ∆.

Additionally, there is one function !g under the root R. The call guard of each f τ checks that the ID τ is violated for the sibling tuple. Satisfaction of the FDs in ∆, and violation of f, are ensured by static constraints. The guard of !g simply checks that the relation returned by the call to !e is non-empty.

We consider the view V S retaining all functions. It is easy to check that ∆ |= f iff there is a blocking run of S whose view under V S is ρ = init.e.g.( block) ω (we ignore the constant state). Indeed, since no function !f τ can be called, all IDs in ∆ are satisfied. Recall that satisfaction of the FDs in ∆ and violation of f are ensured by the constraints. Thus, the non-empty instance returned by e satisfies ∆ and violates f. Now suppose towards a contradiction that one can effectively construct, for each BAXML schema as above, a corresponding artifact system Γ with a view V Γ ∈ V serv so that V S ([S]) ∼ V Γ ([Γ]). By definition, the first event in both [S] and [Γ] is init. Also, in [S] there is a unique edge labeled init, leading to the node whose state is root/!e. Let T !e be the subtree of [S] rooted at that node. By definition of ∼, V S (T !e ) must be w-bisimilar to V (T ) for every subtree T ∈ T init , where T init consists of the subtrees of [Γ] whose roots have incoming edge init. In other words, Γ must simulate S regardless of its database. In particular, this must be the case for the empty database. Thus, let T ∅ be the subtree in T init corresponding to the empty database. From the above it follows that V S (T !e ) ∼ V Γ (T ∅ ).

Recall that ∆ |= f iff V S (T !e ) contains a path from the root labeled e.g.block. Since V S (T !e ) ∼ V Γ (T ∅ ), this happens iff V Γ (T ∅ ) contains a path from the root labeled ǫ * .e.ǫ * .g.ǫ * .block. By definition of ∼, since V S (T !e ) has no infinite branches of ǫ-transitions (in fact no ǫ-transitions at all), V Γ (T ∅ ) may not have infinite branches of ǫ-transitions. Also note that T ∅ is finitely branching, modulo isomorphism (this is because in artifact systems, each transition other than init generates only finitely many non-isomorphic states from each given state). It follows that from each given node, the set of lengths of ǫ-paths originating at that node is bounded (otherwise, an easy induction shows that there must be an infinite path of ǫ-transitions from that node). This allows to effectively generate a breadth-first expansion of V Γ (T ∅ ) (modulo isomorphism) until the first 3 non-ǫ transitions occur along all branches. This allows deciding if a path labeled ǫ * .e.ǫ * .g.ǫ * .block starting from the root exists in V Γ (T ∅ ), and provides a procedure for testing whether ∆ |= f . Remark 6.10. By Lemma 2.5 (applied to effective simulations), the negative result of Theorem 6.9 extends to any views that expose more information than those above.

CONCLUSION

This paper makes a dual contribution. First, it proposes a flexible framework for comparing distinct workflow models by means of views extracting a common set of observable states and events, and a natural notion of simulation. Second, it uses this framework to compare concrete languages capturing some of the main workflow specification paradigms: automata, temporal constraints, and pre-and-post conditions. These were first investigated using as a common core BAXML, where the integration of XML and embedded function calls allows to naturally support a wide range of datacentered tasks. We proved the surprising result that the static constraints of BAXML are alone sufficient to simulate the three apparently much richer workflow specification languages mentioned earlier. Beyond the specifics of the XML-based model, the results provide insight into the power of the various workflow specification paradigms, the trade-offs involved in choosing one over another, and the relation to static constraints. Finally, we compared BAXML to tuple artifacts, a variant of IBM's Business Artifact model using relational databases. We showed that BAXML