Pierre Bourhis
email: pierre.bourhis@univ-lille1.fr

Loïc Hélouët
email: loic.helouet@inria.fr

Rituraj Singh
email: rituraj.singh@irisa.fr

Zoltán Miklós
email: zoltan.miklos@univ-rennes1.fr

Data

Miklos

Zoltan

Data Centric Workflows for Crowdsourcing

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Crowdsourcing is a powerful tool to leverage intelligence of crowd to realize tasks where human skills still outperform machines [START_REF] Kucherbaev | Crowdsourcing processes: A survey of approaches and opportunities[END_REF]. It has been successful in contributive science initiatives, such as CRUK's Trailblazer 4 , Galaxy Zoo5 , etc. Most often, a crowdsourcing project consists in deploying a huge amount of work into tasks that can be handled by humans in a reasonable amount of time. Generally, tasks have the form of micro-tasks, which usually take a few minutes to an hour to complete. It can be labeling of images, writing scientific blogs, etc. The requester publishes the task on the platform with a small incentive (a few cents, reputation gain, goodies, etc.), and waits for the participation from the crowd. The micro-tasks proposed on crowdsourcing platforms are hence relatively simple, independent, cheap and repetitive.

The next stage of crowdsourcing is to design more involved processes still relying on the vast wisdom of the crowd. Indeed, many projects, and in particular scientific workflows, take the form of orchestrations of high-level composite tasks. Each high-level task can be seen individually as a data collection task, or as a processing of a large dataset, built as the union of results from independent easy micro-tasks. However, the coordination of these high-level tasks to achieve a final objective calls for more evolved processes. One can easily meet situations in which the result of a high-level task serves as entry for the next stage of the overall process: for instance, one may want to remove from a picture dataset images of poor quality before asking users to annotate them. Similarly, there are situations allowing parallel processings of datasets followed by a merge of the obtained results. A typical example is cross-validation of answers returned by different users.

As noted by [START_REF] Tranquillini | Modeling, enacting, and integrating custom crowdsourcing processes[END_REF], composite tasks are not or poorly supported by crowdsourcing platforms. Crowdsourcing markets such as Amazon Mechanical Turk6 (AMT), Foule Factory7 , CrowdFlower 8 , etc. already propose interfaces to access crowds, but the formal design and specification of crowd based complex processes is still in its infancy.

Many projects cannot be described as collections of repetitive independent micro-tasks: they require specific skills and collaboration among participants. They shall hence be considered as complex tasks involving a workflow within a collaborative environment. The typical shape of such complex tasks is an orchestration of high-level phases (tag a database, then find relevant records, and finally write a synthesis). Each of these phases requires specific skills, can be seen at its level as a new objective on its own, and can be decomposed into finer choreographies, up to the level of assembly of micro-tasks. The workflow of such processes is hence dynamic and shall consider users skills, availability, the data they produce, but also their knowledge about processes themselves. Within this setting, the challenges are the following: first, there is a discrepancy between the "project level", where clients of a crowd platform may have a good understanding of how to decompose their high-level projects into phases, and the micro-task level, where the power of existing crowdsourcing solutions can be used without knowing the high-level objectives of the projects. Thus transforming high-level phases into orchestrations of micro-tasks is also a difficult process. A second challenge is to exploit contributors skills and data collected along the orchestration, to improve the expressive power and accuracy of complex tasks. One possibility to allow higher-order answers to refine processes dynamically static orchestration of easy micro-tasks before execution of this low-level workflow. However, this solution lacks adaptability, and may miss some interesting skills of participants who cannot realize directly a particular task, but know how to obtain the result, or can bring data to enhance the information owned by the system. One can imagine for instance that collected data is used in real time to choose an orchestration and even the way tasks are decomposed. This calls for the integration of higher-order schemes in the implementation of complex tasks. In addition, clients may want guarantees on duration of their projects and on the returned results. It is hence interesting to consider termination and output correctness questions for complex tasks. Now, it is frequently admitted that the main difficulty to use crowdsourcing platforms is the lack of solutions to build these high level orchestrations. Running a complex process consists in, roughly speaking, refining a high-level task into a composition of finer grain subtasks with a divide and conquer strategy. Orchestration languages such as ORC [START_REF] Kitchin | A language for task orchestration and its semantic properties[END_REF][START_REF] Misra | Computation orchestration[END_REF], BPEL [START_REF] Andrews | Business process execution language for Web services (BPEL4WS)[END_REF][START_REF]Web Services Business Process Execution Language[END_REF], etc. already exist, and could easily serve as a basis for coordination of high-level tasks. However, in data-centric models involving human stake holders, skills, time, etc, one expects solutions to adapt a process at runtime depending on the data contents, on availability of workers, etc. Models such as ORC, BPEL, and many process algebras they are tailored for workflows which dynamics is fixed a priori and cannot evolve at runtime and do not fulfill this additional requirement. Some solutions for the design and monitoring of complex processes running on crowdsourcing platforms have been proposed. [START_REF] Sánchez-Charles | Crowdwon: A modelling language for crowd processes based on workflow nets[END_REF] propose a timed modeling language for complex tasks based on adaptive workflow net. A graphical net with deadline mechanism is presented to design, describe and visualize the flow of tasks at crowdsourcing platforms. Kulkarni et. al propose the Turkomatic tool which works on the principle of Price, Divide and Solve (PDS) [START_REF] Kulkarni | Collaboratively crowdsourcing workflows with turkomatic[END_REF]. The tool uses the power of crowd to decompose a complex task while the requester can monitor the decomposition workflow. Crowdforge is an interesting work which uses Map-Reduce technique to solve complex tasks [START_REF] Kittur | Crowdforge: Crowdsourcing complex work[END_REF]. It provides a graphical web interface and primitives (partition, map and reduce) to decompose complex tasks into sub-tasks and define dependencies among them. Zheng et. al [START_REF] Zheng | Crowdsourcing complex task automatically by workflow technology[END_REF] define a PDS framework based on refinement of state machines.

Providing tools to implement PDS solutions is already a progress for crowdsourcing. We advocate, however, that an implicit demand of a requester is that the orchestration of micro-tasks that will be performed to realize his complex process will terminate, and will return appropriate answers. Further, we propose to rely on human skills to propose at runtime correct and efficient decomposition of tasks. In this work, we define a workflow language where the relation between data input to a task and output by it is formally defined, and in which users can propose refinements of a task, in addition to their standard contribution to micro-tasks. These refinements depict the way to obtain an answer rather than the answer itself. We then address the question of termination and correctness of complex workflows defined with this formalism.

In this paper, we focus on the orchestration of complex tasks in a crowdsourcing environment, with higher order constructs allowing online decomposition of the tasks by crowdworkers. A complex task is defined as a workflow orchestrating sub-tasks. At the very beginning, a coarse description is provided by the process requester, possibly with input data and with requirements on the expected output. Tasks in a workflow receive input data, and output data once realized. At each step, crowdworkers can decide to realize a task with the provided inputs, or decompose the task and its inputs into orchestrations of smaller work units. We first propose a model called complex workflows, allowing for the definition of data-centric workflows with higher-order schemes allowing workers to refine tasks at runtime, and for the definition of constraints on inputs and outputs of the workflow. We then consider the question of termination: given a workflow, input data and a set of crowdworkers, allowed to transform input data or decompose tasks, is the workflow executable (or always executed) up to its end? We show that due to higher-order, complex workflows are Turing complete, and hence existence of a terminating run is not decidable. However, termination of all runs is decidable, and upon some sensible restrictions that forbid decomposition of the same type of task an arbitrary number of times, existential termination becomes decidable. As a third contribution, we consider proper termination, i.e., whether a complex workflow terminates and returns data that comply with the client's requirements. Related Work : Realization of complex tasks on crowdsourcing platforms is still a recent topic, but some works propose solutions for data acquisition and management or deployment of workf lows, mainly at the level of micro-tasks [START_REF] Garcia-Molina | Challenges in data crowdsourcing[END_REF][START_REF] Li | Crowdsourced data management: A survey[END_REF]. Crowdforge uses Map-Reduce techniques along with a graphical interface to solve complex tasks [START_REF] Kittur | Crowdforge: Crowdsourcing complex work[END_REF]. Turkit [START_REF] Little | Turkit: tools for iterative tasks on mechanical turk[END_REF] is a crash and rerun programming model. It built on an imperative language, that allows for repeated calls to services provided by a crowdsourcing platform. A drawback of this approach is that clients may not have the programming skills needed to design complex orchestrations of platform services. Turkomatic [START_REF] Kulkarni | Collaboratively crowdsourcing workflows with turkomatic[END_REF] is a tool that recruits crowd workers to help clients planning and solving complex jobs. It implements a Price, Divide and Solve (PDS) loop, that asks crowd workers to divide a task into orchestrations of subtasks, and repeats this operation up to the level of micro-tasks. A PDS scheme is also used by [START_REF] Zheng | Crowdsourcing complex task automatically by workflow technology[END_REF] in a model based on hierarchical state machines. States represent complex tasks that can be divided into orchestrations of sub-tasks. Both approaches require monitoring of workflows by the client, which is cumbersome and does not match with the goal of providing a high-level service. The PDS oriented solutions have been validated empirically on case studies, but formal analysis of tasks realization is not the main concern of these works.

Several formal models and associated verification techniques have been proposed in the past for datacentric systems or orchestration of tasks. We do not claim exhaustiveness, and mainly refer in the rest of this section to a few papers with models or objectives seems the closest to our model and verification solution. Workflow nets [START_REF] Van Der Aalst | Soundness of workflow nets: classification, decidability, and analysis[END_REF] is a variant of Petri nets dedicated to business processes. They allow parallel or sequential execution of tasks, fork and join operations to create or merge a finite number of parallel threads. Tasks are represented by transitions. Workflow nets mainly deal with the control part of business processes, and data is not central for this model. As already mentioned, orchestration models originally built for business processes such as ORC [START_REF] Kitchin | A language for task orchestration and its semantic properties[END_REF][START_REF] Misra | Computation orchestration[END_REF] or BPEL [START_REF] Andrews | Business process execution language for Web services (BPEL4WS)[END_REF][START_REF]Web Services Business Process Execution Language[END_REF] are not a priori tailored for dynamic orchestrations nor for handling datasets manipulations (they are more centered on the notion of transaction than on the notion of datasets transformations). Data-centric models and their correctness have also been considered in many papers. Guarded Active XML [START_REF] Abiteboul | Static analysis of active XML systems[END_REF] (GAXML for short) is a specification paradigm where services are introduced in structured data. The model is defined as structured data that embed references to service calls. Services can modify data when their guard is satisfied, and replace a part of the data by some computed value that may also contain references to service calls. Though GAXML does not really address crowdsourcing nor tasks refinement, if services are seen as tasks, the replacement mechanism performed during calls can be seen as a form of task refinement. This model is very expressive, but restrictions on recursion allows for verification of Tree LTL (a variant of LTL where propositions are replaced by statements on the structured data). More recently, [START_REF] Abiteboul | Collaborative data-driven workflows: think global, act local[END_REF] has proposed a model for collaborative workflows where peers have a local view of a global instance, and collaborate via local updates. With some restrictions, PLTL-FO (LTLT-FO with past operators) is de-cidable. Business artifacts were originally developed by IBM [START_REF] Nigam | Business artifacts: An approach to operational specification[END_REF], and verification mechanisms for LTL-FO were proposed in [START_REF] Damaggio | Artifact systems with data dependencies and arithmetic[END_REF][START_REF] Koutsos | Process-centric views of data-driven business artifacts[END_REF] for subclasses of artifacts with data dependencies and arithmetic. LTL-FO formulas are of the form ∀x 1 , . . . , x k , φ where φ is an LTL formula including FO statements. Variables are always universally quantified. [START_REF] Deutsch | Verification of communicating data-driven web services[END_REF] consider verification of LTL-FO for systems composed of peers that communicate asynchronously over possibly lossy channels and can modify (append/remove records from local databases). Unsurprisingly, queues makes LTL-FO undecidable, but bounding the queues allows for verification. The way data is handled in business artifacts is close to our model, and as for complex workflows, allows for data inputs during the lifetime of an artifact. However, artifacts mainly consider static orchestrations of guarded tasks, described as legal relations on datasets before and after execution of a task, and does not consider higher-order constructs such as runtime tasks refinement. Further, LTL-FO verification focuses mainly on dynamics of systems (termination, reachability) but does not address correctness. [START_REF] Babak | Verification of relational data-centric dynamic systems with external services[END_REF] considers Data-centric dynamic systems (DCDS), i.e. relational databases equipped with guarded actions that can modify their contents, and call external services. This work proposes verification techniques for fragments of First-Order µ-calculus, and show decidability for run-bounded systems, in which external services cannot be repeatedly called with arguments returned by former service calls. Run boundedness is undecidable, but weakly-acyclic DCDS enjoy this property.

The model proposed in our paper is a workflow with higher-order constructs that refine tasks by new workflows, dependencies between data input and output by a task, and in which causal flows among tasks indicate how data in passed from one stage of the computation to the other. [START_REF] Beeri | Querying business processes[END_REF] proposes a verification scheme for a similar model depicting business processes with external calls. The business processes are recursive functions that can call one another, and the verification that is performed is defined using a query language. This language specifies shapes of workflow executions with a labeled graph and transitive relations among its nodes. A query Q is satisfied by a workflow W if there is an embedding of Q into the unfolding of W . While this model addresses the shape of executions, it is more focused on the operational semantics of workflows. A contrario, our verification scheme does not address the shape of control flow, but rather the contents of data manipulated by the workflow, i.e. it is more concerned by the denotational semantics of the specification, and on the question of termination.

This paper is organized as follows: Section 3 introduces our model. Section 4 defines its operational semantics, and section 6 addresses the termination question. Section 7 considers proper termination of complex workflows, before conclusion. For readability reasons, some technical proofs are only sketched, but their full versions are provided in appendix.

Motivation

Our objective is to provide tools to develop applications in which human actors are involved to resolve tasks or propose solutions to complete a complex task. The envisioned scenario is the following: a client provides a coarse grain workflow depicting important phases of a complex task to process data, and a description of the expected output. The tasks can be completed in several ways, but cannot be fully automated. It is up to a pool of crowdworkers to complete them, or to refine the tasks up to the fine grain level where high-level tasks are expressed as orchestrations of basic simple tasks.

A simple example: the actor popularity poll

To illustrate the needs for complex workflows, refinement, and human interactions, we give a simple example. A client (for instance a newspaper) wants to rank the most popular actors of the moment, in the categories comedy, drama and action movies. This ranking is a sent to a crowdsourcing platform as a high-level process decomposed into three sequential phases: first a collection of the most popular actors, then a selection of the 50 most cited names, followed by a classification of these actors in comedy/drama/action category. The ranking ends with a vote for each category, that asks contributors to associate a score to each name. The client does not input data to the system, but has some requirements on the output: the output is an instance of a relational schema R = (name, cites, category, score), where name is a key, cites is an integer that gives the number of cites of an actor, category ranges over {drama, comedy, action} and score is a rational number between 0 and 10. Further, for an output to be consistent, every actor appearing in the final database should have a score and a number of cites greater than 0. Form this example, one can notice that there are several ways to collect actors names, several ways to associate a category tag, to vote, etc. but that the clients needs are defined in terms of high-level tasks, without information on how the crowd will be used to fulfill the demand. This simple sequential task orchestration is depicted in Figure 1. The workflow starts from and empty input dataset D ∅ , and should return the desired actor popularity data in a dataset D ranked .

The model proposed in section 3 is tailored to realize this type of application with the help of workers registers on a platform who can either provide their experience on how to decompose difficult tasks, or input their knowledge and opinion on the platform.

A real field example: the SPIPOLL initiative

We provide a real field example, where managing task decomposition, orchestration, and workers contributions are key issues. We study the SPIPOLL initiative9 , a participatory science project. The project aims at collecting quantitative data on pollination, flowering insects to measure the diversity and network structure of pollination in France. This task is not trivial for several reasons. First of all, collecting information on insects requires a huge workpower to collect significant samples throughout the whole country. Second, the project lacks workpower to sort, classify, huge datasets , and then derive conclusions from the observed populations. While volunteers can help sorting pictures of insects, some rare taxons can only be recognized by experts. The objective of SPIPOLL is to organize a collaborative work involving ordinary people, trained volunteers and experts in order to build significant datasets and extract information on pollinating insects populations. We believe that this project can benefit from advances in data centric crowdsourcing platforms, and in particular for the design and automation of complex data acquisition procedures. Roughly speaking, the high-level description of SPIPOL tasks is: acquire data (pictures), classify them, and publish the results. The result of classification should be a set of images with location and time tags, together with a taxon chosen among a finite set of species. The data acquisition and classification protocols specified by SPIPOLL fits well with the core idea of complex tasks. The protocol proposed by SPIPOLL is following. Volunteers stand for a certain duration (usually 20 minutes) in a place frequented by insects (bushes, flower beds,...) and take pictures of insects pollinating on a flower in this place. Once this phase is completed, the observer uploads his pictures on a server. This first phase results in huge collections of pictures, but not all of them are exploitable. The obtained result after the first phase is a dataset which records are of the form of R = {image, place, time}. Data collected from various sources are used as inputs for a second phase. In this second phase, workers have to classify pictures according to their quality, i.e. identify images that will help finding a correct identification for the represented insect. As the images are collected from diverse and unknown observers, there is need to rank and tag the respective image based on their quality, i.e. associate with each image a tag quality = {poor, average, good, best}. Generally, for these tasks, considering the bias among the workers, a typical image is given to k different workers. The workers give their opinion and tag each of the obtained images.

The third phase aggregates the result obtained in the second phase and gives a final verdict for each picture. Majority voting technique are widely used to reach the common consensus among the workers.

The fourth phase removes images with poor quality from the dataset. The fifth phase, categorizes the insect images with sufficient quality obtained as input from the fourth phase into different species category, category = {category 1 , category 2 , . . . , category l }. Similar to the second phase, an image is distributed to n unique workers who are asked to tag a category to the insect image. The output of this phase serves as input for a sixth phase that aggregates the result by majority voting to obtain the f inal category for each picture, and then passes the result for the final assessment. The final assessment for each image is performed by the experts or scientists for validation and then the obtained results are published. These types of complex tasks can be often found when there is need of data collection, data cleaning and then processing the data based on human intelligence.

The SPIPOLL example raises several observations on the realization of complex tasks in a crowsourcing environment. First, one can note that some of the tasks need to be completed sequentially, and on the other hand some tasks can be executed in parallel. For example, in the Spipoll case study, images can be only be annotated after they have been collected by observers. As a result, the first phase and the second phase can only be executed sequentially. However, images can be annotated in parallel (second, fifth phase) by different sets of workers. Another remark is that some recurrent orchestration patterns appear, such as dataset distribution, tagging and aggregation. These work distribution patterns are typical examples where crowdsourcing platforms are particularly adapted to improve quality and delays in data analysis. The dataset obtained from the observers can be large and annotating such big datasets is usually a task that cannot be performed by a single worker. Most often, volunteer contributors in crowdsourcing platforms spend little amounts of time on the platform. Hence the annotation phase needs to be decomposed, for instance by splitting large datasets into several chunks of reasonable size. These small chunks of data are then distributed and tagged in parallel by several workers, before aggregation. In this setting, refinement of a heavy tasks into several smaller concurrent easy tasks saves a lot of time.

Another lesson learned from the SPIPOLL case study is that some tasks may require special skills, such as expertise on insects to be completed. The validation task in the above example requires specialized people to judge the validity of proposed taxons. Hence, the system should consider the expertise of the worker in allocating tasks. Another thing to note that the example depicted here is data-centric, i.e. the role of each high-level or low-level task is to manipulate and transform data (select, tag,...) One can also observe that all tasks do not require human intelligence, and some of them can be easily performed by machines. As for example, consensus between the workers are performed by applying majority voting techniques. Other tasks such as selection of best pictures are roughly speaking SQL queries and can be automated. Thus, the system is a mixture of human and machine powered intelligence. Generally, machine powered tasks are deterministic in nature and human doable tasks comes with uncertainty.

As already mentioned, the output of one task can be needed as input to another task, which leads to causal dependencies among tasks. In addition, the execution of one task may affect the output of another task. An erroneous output of one task can jeopardize the execution of several successive tasks and in the long run may also halt the whole process. Hence, there needs verification techniques to ensure consistency and guaranteed output for each of the task execution.

Problems for Complex Workflows

Many existing crowdsourcing applications collect the result of hundreds of micro-tasks, and then aggregate the obtained answers to produce an output. In this simple setting, there is no doubt on the termination of the application : once enough data is collected, the aggregation phase can most of the time be reduced to an automated statistical analysis of returned answers. If incentives and difficulty are properly set, the data collection will terminate in a reasonable amount of time.

In more complex processes requiring refinement of tasks and calling for particular competences, offering the capacity to refine complex tasks may cause undesired behaviors in a workflow: workers can introduce deadlocks, unbounded recursion,... Even with very limited refinement capacities, it is hence not guaranteed that an application always terminates, if it terminates when appropriate data is used as input, etc. When a complex workflow terminates, another question is whether the data forged during the execution of the workflow satisfies the requirements set by the client of the application (in the case of the actor poll, for instance, every listed actor must have a number of cites greater than 0). In the rest of the paper, we formalize complex workflows, and address termination questions. More precisely, given a complex workflow and a set of workers, we will address the following problems:

-(universal termination) Does the workflow terminates for every possible input to the system ? -(existential termination) Is there at least one input for which at least one execution of the workflow terminates ? -(universal proper termination) for a given requirement on the produced output data (resp. on the relation between input data and output data), does the workflow terminates for every possible input to the system ? -(existential proper termination) for a given requirement on the produced output data (resp. on the relation between input data and output data), is there a particular input and at least one execution for which the workflow terminates ?

Universal termination provides a guarantee that a complex workflow will terminate and return a result for any input. This can be seen as a termination guarantee. Existential termination can be considered as a sanity check: a complex workflow that has no valid execution never terminates, regardless of input data, and should hence be considered as ill-formed. Universal proper termination guarantees that a workflow terminates and that it computes data that conforms to the client's requirement. Existential proper termination is also a sanity check, showing that a workflow is able to produce correct data for at least one of its executions.

Complex Workflows

In this section, we formalize the notion of complex workflow, and give its semantics through operational rules. This model is inspired by artifacts systems [START_REF] Damaggio | Artifact systems with data dependencies and arithmetic[END_REF], but uses higher-order constructs (task decomposition), and deals with human resources within the system (the so-called crowdworkers). The context of use of the complex workflow is the following : we assume a client willing to use the power of crowdsourcing to realize a complex task that needs human contribution to collect, annotate, or organize data.

We furthermore assume that this client can reward contribution of human stakeholders up to a certain budget, that he can input data to the system, and that he may have a priori knowledge on the relation between the contents of his input and the plausible outputs returned after completion of his complex task. In its simplest form, this type of application can be an elementary tagging task for a huge database. This type of application was met in citizen science initiatives such as Galaxy zoo 10 , but several types of applications such as opinion polls, citizen participation, etc. can be seen as complex crowdsourcing tasks.

Workflow ingredients

A complex workflow is defined as an orchestration of tasks, specified by a client to process input data and return an output dataset. Tasks that can be accomplished by either humans, i.e. workers if they require human skills or be automated tasks that can be executed by machines. Additionally, worker's task can be an atomic or a complex task.

A simple competence model. We assume a fixed and finite pool U of workers, and an a priori finite list of competences comp. Each worker u ∈ U can complete or refine some tasks according to its skills. We hence define a map sk : U → comp. Notice that sk(u) is a set, i.e. a particular competence c ∈ sk(u) needs not be exclusive. We adopt this simplistic model of workers competences for clarity of the model, but more evolved representations of skills exists and could be easily integrated to the model. For instance, [START_REF] Mavridis | Using hierarchical skills for optimized task assignment in knowledge-intensive crowdsourcing[END_REF] proposes a hierarchy of competences to reflect a natural ranking of the expertise. However, in this paper, we do not consider skills classification nor management of competences, and just view skills of a worker as a set of keywords.

During the execution of a complex workflow, we will consider that each worker is engaged in the execution of at most one task. A task t is a work unit designed to transform input data into output data. It can be a high-level description submitted by a client of the crowdsourcing platform, a very basic atomic task that can be easily accomplished by a single worker (tagging images, for instance), a task that can be fully automated, or a complex task that still requires an orchestration of subtasks to reach its objective. We define a set of tasks T = T ac T cx T aut where T ac is a set of atomic tasks that can be completed in one step by a worker, T cx is a set of complex tasks which need to be decomposed into an orchestration of smaller subtasks to produce an output, and T aut is a set of automated tasks that are performed by a machine (for instance some database operation (selection, union, projection, etc.) executed as an SQL query). Tasks in T aut do not require contribution of a worker to produce output data from input data, and tasks in T ac and T aut cannot be refined. We impose constraints on skills required to execute a task with a map T cs : T → 2 comp , depicting the fact that a worker u is allowed to realize or refine task t if it has the required competences, i.e., if T cs (t) ∩ sk(u) = ∅. This competence model is not essential for the (un)decidability results presented hereafter in the model. One could indeed consider that every worker has all competences, and can perform any task within the system. Within this setting, one needs not define workers competences, nor attach skills constraints to tasks. However, for practical use of a crowdsourcing platform, one usually wants to obtain the best possible results, which calls for a clever management of skills, incentives, etc.

Let us now explain how task refinement is modeled. Let t ∈ T cx be a complex task, and let C t = T cs (t) be the set of competences allowing a worker to complete successfully t. As already explained, we advocate that crowdsourcing platforms should allow higher-order answers. So, we assume that, as soon as a worker u owns one appropriate skill to solve task t, he is able to refine it: either he already knows a very generic way to decompose tasks of this kind, or the platform allows any higher-order answer depicted as a finite workflow to complete the task. In the first case, the workflow to complete t is fixed a priori (it can be for instance a generic map-reduce pattern to distribute data and aggregate results). In the second case, the higher-order answer belongs to a finite set of possible workflows (for instance workflows of bounded size assembling nodes which labels belong to a finite alphabet of tasks). Such possibility is already in use in the world of crypto trading (platforms such as Kryll allow users to define simple trading bots using a block diagram language [?]). In the following, we hence assume that a competent worker possesses several finite orchestrations depicting appropriate refinements of t. We will denote by P rof ile(t, u) this finite set of finite workflows. Let us illustrate refinement with an example. Assume a task t ∈ T cx which role is to tag a (huge) dataset D in . Then, P rof ile(t, u) contains a workflow that first decomposes D in into K small tables, then inputs these tables to K tagging tasks in T ac that can be performed by humans, and finally aggregates the K obtained results. Note that a profile in P rof ile(t, u) needs not be a workflow of large size, and may even contain workflows with a single node. In this case, the refinement simply replaces t ∈ T cx by a single atomic tagging task t ∈ T ac , meaning that u thinks that the task is easy, and wants it to be realized by a single worker.

Let us consider the following example: a complex task t like asks to rank large collections of images of different animals with a score between 0 and 10. The relational schema for the dataset D used as input for t like is a collection of records of the form P icdata(nb, name, kind) where nb is a key, name is an identifier for a picture, kind the species represented on the picture obtained from former annotation of data by crowdworkers. A worker u can decide to divide dataset D into three disjoint datasets containing pictures of cats, pictures of dogs, and pictures of other animals. The contents of these datasets can be ranked separately, and then the results of ranking aggregated. Figure 2 represents a possible profile to refine task t like . A task t like is rewritten in a workflow with four nodes. Node n 0 is an occurrence of an automated tasks that splits the original dataset into datasets containing pictures of dogs, cats, and other animals. Nodes n 1 , n 2 , n 3 are occurrences of tagging tasks for the respective animal kinds, and node n f is an occurrence of an automated task that aggregates the results obtained after realization of preceding tasks.

In addition to the notion presented above, crowdsourcing platforms often consider incentives, i.e. the benefit provided to the worker for performing a particular task. Incentive mechanism can be intrinsic (Self motivation, Gamification, Share Purpose, Social cause, etc.) as well as extrinsic (Tailor rewards, Bonus, Promote Workers, etc.) [START_REF] Daniel | Quality control in crowdsourcing: A survey of quality attributes, assessment techniques, and assurance actions[END_REF]. In this paper, we leave this notion of incentives apart, and consider that all workers are equally eager to perform all tasks that are compatible with their competences. One shall however keep in mind that setting incentives appropriately is a key issue to complete successfully a workflow: associating high rewards to important or blocking tasks is a way to maximize the probability that these tasks will be realized by a worker.

Workflows

Definition 1 (Workflow). A workflow is a labeled acyclic graph W = (N, -→, λ) where N is a finite set of nodes, representing occurrences of tasks, -→⊆ N × N is a precedence relation, and λ : N → T associates a task name to each node of W . A node of W is a source iff it has no predecessor, and a sink iff it has no successor. We require that a workflow has at most one sink node, denoted n f .

In the rest of the paper, we will consider that U and T are fixed, and we will denote by W the set of all possible workflows. Intuitively, if (n 1 , n 2 ) ∈-→, then an occurrence of task named λ(n 1 ) represented by n 1 must be completed before an occurrence of task named λ(n 2 ) represented by n 2 , and that data computed by n 1 is used as input for n 2 . We denote min(W ) the set of sources of W , by succ(n) the set of successors of a node n, and by pred(n) its predecessors. The size of W is the number of nodes in N and is denoted |W |. We assume that when a task in a workflow has several predecessors, its role is to aggregate data provided by preceding tasks, and when a task has several successors, its role is to distribute excerpts from its input dataset to its successors. With this convention, one can model situations where a large database is to be split into smaller datasets of reasonable sizes and sent to tagging tasks that needs to be completed by workers. We denote by W \ {n} the restriction of W to N \ {n}, that is, a workflow from which we remove node n and all edges which origins or goals are node n. We assume some well-formedness properties of workflows:

-Every workflow has a single sink node n f . Informally, we can think of n f as the task that returns the dataset computed during the execution of the workflow. -There exists a path from every node n of W to the sink n f . The property prevents from launching tasks which results are never used to build an answer to a client. for every workflow W = (N, -→, λ) ∈ P rof ile(t, u), the labeling λ is injective. This results in no loss of generality, as one can create copies of a task for each node in W , but simplifies proofs and notations afterwards. Further, W has a unique source node src(W ).

Definition 2 (Refinement). Let W = (N, -→, λ) be a workflow, W = (N , -→ , λ ) be a workflow with a unique source node n src = src(W ) and a unique sink node n f and such that N ∩N = ∅. The replacement of n ∈ N by W in W is the workflow

W [n/W ] = (N [n/W ] , -→ [n/W ] , λ [n/W ]
), where:

-

N [n/W ] = (N \ {n}) ∪ N -→ [n/W ] =→ ∪{(n 1 , n 2 ) ∈→| n 1 = n ∧ n 2 = n} ∪ {(n 1 , n src ) | (n 1 , n) ∈→} ∪ {(n f , n 2 ) | (n, n 2 ) ∈→} -λ [n/W ] (n) = λ(n) if n ∈ N, λ (n) otherwise
To illustrate the notion of refinement, consider the example of Figure 3. In the workflow at the left of the Figure, node n 1 is replaced by the profile of Figure 2 for taks t like . The result is the the workflow on the right of Figure 3.

Data

The data in complex workflow refer to data provided as input to the system by a client, to the data conveyed among successive tasks, and to data returned after completion of a workflow, that is returned to the client. We use a standard relational model to represent data [START_REF] Codd | Relational completeness of data base sublanguages[END_REF], i.e., data is organized in datasets, that follow relational schemas. We assume finite set of domains dom = dom 1 , . Complex workflows manipulate data, either automatically via automated tasks, or with the help of workers. Seen as data transformations, tasks can be seen as mechanisms that apply F O queries to datasets, add new tuples from a given domain to an existing dataset, add a new field to every record in a dataset, etc. Execution of a task t = λ(n) in a workflow builds on input data to produce output data. The data input to node n with k predecessors is a list of datasets

D in = D in 1 , . . . D in k .
For simplicity, we consider that predecessors (resp. successors of a node) are ordered, and that dataset D in i input to a node is the data produced by predecessor n i . Similarly, for a node with q successors, the output produced by a task will be D out = D out 1 . . . D out q . As for inputs, we will consider that dataset D out i is the data sent to the i th successor of node n. The way output data is produced by task t = λ(n) and propagated to successor nodes depends on the nature of the task. If t is an automated task, the outputs are defined as a deterministic function of inputs, i.e., D out = f t (D in ) for some deterministic function f t . Consider for instance the example of Figure 2, and in particular node n 0 that represents an automated task which automatically splits a dataset into three smaller datasets D cats , D dogs , D oth . Datasets D, D dogs , D cats , D oth use the relational schema rs = P icdata(nb, name, kind). Further, dataset D dogs can be obtained as a simple restriction of D to tuples such that kind = "dog". This is easily encoded as an SQL formula. Conversely, D and D dogs satisfy the FO formula ∀nb, n, k, (P icdata(nb, n, k) ∈ D ∧ k = "dog") ⇔ P icdata(nb, n, k) ∈ D dogs . We will allow automated tasks executions only for nodes which inputs are not empty. In the rest of the paper, we will consider that automated tasks perform simple SQL operations : projections on a subset of attributes, selection of records that satisfy some predicate, record insertion or deletion.

To simplify workflow refinements, we will consider particular split nodes, i.e. have a single predecessor, a fixed number k of successors, and are attached a task t ∈ T aut that transforms a non-empty input D in into a list D out = D out 1 . . . D out k . Note that D out needs not be a partition of D in nor to define distinct output datasets. To refer to the way each D out i is computed, we will denote by spl (i) t , the function that associates to D in the i th output produced by a split task t (i.e. spl ). Consistently with the non-empty inputs requirement the input dataset to split cannot be empty to execute such splitting task. Similarly, we will consider join nodes, whose role is to automatically aggregate multiple inputs from D in . Such aggregation nodes can simply perform union of datasets with the same relational schema, or a more complex join. Consider a node n with several predecessors n 1 , . . . n k , and a single successor s. Let D in = D 1 .D 2 . . . D k , where all D i 's have the same relational schema. Then we can define a join node by setting

f t (D in ) = i∈1..|D in | D i .
Consistently with the non-empty inputs requirement, none of the the input datasets is empty when a join is performed.

For an atomic task t ∈ T ac attached to a node n of a workflow and executed by a particular worker u, data D in comes from preceding nodes, but the output depends on the worker. Hence, execution of task t by worker u produces an output D out chosen non-deterministically from a set of possible outputs F t,u (D in ). We will however allow for the modeling of some a priori knowledge and of constraints on the values chosen by workers. For the rest of the paper, we will assume that the legal contents of F t,u (D in ) is defined as a first order formula (possibly with arithmetic constraints) φ t,in,out that holds for datasets

D in = D in 1 . . . D in k and D out = D out 1 . . . D out k if D out ∈ F t,u (D in ).
Consider again the example of Figure 2, and in particular node n 1 that represents an occurrence of an atomic task which goal is to rank pictures of dogs. This task starts from a dataset D dogs that uses relational schema P icData(nb, name, kind) and outputs a dataset D dogs,ranked with relational schema P icData(nb, name, kind, rank) where rank is an integer in [0, 10]. We can relate tuples in D dogs and D dogs,ranked with the following formula:

∀nb, n, k, P icData(nb, n, k) ∈ D dogs ⇔ ∃r, r ∈ [0, 10] ∧ P icData(nb, n, k, r) ∈ D dogs,ranked
As r can take only a finite number of integer values, we can still express this formula with with relational statements and boolean connectives. In the case of split and merge operations, one can still define FO formulas relating datasets before and after the execution of a particular node. Consider the example of Figure 3(left), and in particular node n 3 . Let us assume that this node performs the disjoin union of tuples in datasets D 1 , D 2 produced by execution of tasks attached to nodes n 1 and n 2 , and that both D 1 , D 2 contain tuples of the form P icData(nb, n, k, r). Let D 3 be the dataset produced by node n 3 . Then the FO formula expressing the fact that D 3 is the disjoint union of D 1 and D 2 is:

∀nb, n, k, r, P icData(nb, n, k, r) ∈ D 1 ∧ P icData(nb, n, k, r) ∈ D 2 ⇔ P icData(nb, n, k, r) ∈ D 3
Still on the example of Figure 2(left), assume that t 2 produces a dataset D 2 that is a selection of pictures by a separate pool of workers, represented by tuples of the form Selection(nb, score), where nb is the unique identifier of a picture, and that the role of task t 3 is to keep pictures that were both choosen in D 1 and D 2 , and keep the maximal score attached to each picture in any of the datasets. Then, the relation among input

D 1 , D 2 and D 3 is : ∀nb, n, k, r, nb , s, P icData(nb, n, k, r) ∈ D 1 ∧ Selection(nb , s) ∈ D 2 ∧ nb = nb ⇔ P icData(nb, n, k, r ) ∈ D 3 ∧ [(r > s ∧ r = r) ∨ (r ≤ s ∧ r = s)
The dependencies between input data and output data of a particular task can hence be captured by F O formulas (with some arithmetic constraints): either tasks apply SQL-like queries and the relation between input and outputs can be captured by First-Order logic [START_REF] Codd | Relational completeness of data base sublanguages[END_REF]. We will show in section 6 that these dependencies can be used to prove feasibility of a particular execution of a complex workflow, even when manipulated data are not precisely known.

Operational semantics

In section 4, we have introduced all ingredients to define formally complex workflows and their semantics:

Definition 3. A Complex Workflow is a tuple CW = (W 0 , T , T cs , U, sk, P)
where T is a set of tasks, U a finite set of workers, P : T × U → 2 W associates to pairs (t, u) of complex tasks and workers a set P rof iles(t, u) = P(t, u) of possible workflows that u can use to refine t, sk defines workers competences, and T cs gives the competences needed to refine a task. W 0 is an initial workflow, that contains a single source node n i and a single sink node n f .

Intuitively, in a complex workflow, W 0 is an initial high-level description provided by a requester. The rest of the description is the execution environment for this complex process: it defines a finite set of users, their skills, and their knowledge in terms of task decomposition.

The execution of a complex workflow consists in realizing all its tasks, following the order given by the dependency relation -→ in the orchestration. At each step of an execution, the remaining part of the workflow to execute, the assignments of tasks to workers and the data input to tasks are memorized in a configuration. Execution steps consist in updating configurations according to operational rules. They assign a task to a competent worker, execute an atomic or automated task (i.e. produce output data from input data), or refine a complex task. Executions end when the remaining workflow to execute contains only the final node n f .

An assignment for a workflow W = (N, -→, λ) is a partial map Ass : N → U such that for every node n ∈ Dom(Ass), T cs (λ(n)) ∩ sk(Ass(n)) = ∅ (worker Ass(n) has competences to complete task λ(n)). We furthermore require map Ass to be injective, i.e. a worker is involved in at most one task. We say that u ∈ U is free if u ∈ Ass(N ). If Ass(n) is not defined, and u is a free worker, Ass ∪ {(n, u)} is the map that assigns node n to worker u, and remains unchanged for every other node. Similarly, Ass\{n} is the restriction of Ass to N \ {n}.

A data assignment for W is a function Dass : N → (DB {∅}) * , that assigns a sequence of input datasets to nodes in W . For a node with k predecessors n 1 , . . . n k , we have Dass(n) = D 1 . . . D k . A dataset D i can be empty if n i has not been executed yet, and hence has produced no data. We denote by Dass(n) [i/X] the sequence obtained by replacement of D i by X in Dass(n). Definition 4 (Configuration). A configuration of a complex workflow is a triple C = (W, Ass, Dass) where W is a workflow depicting remaining tasks that have to be completed, Ass is an assignment, and Dass is a data assignment.

A complex workflow execution starts from the initial configuration C 0 = (W 0 , Ass 0 , Dass 0 ), where Ass 0 is the empty map, Dass 0 associates dataset D in provided by client to n init and sequences of empty datasets to all other nodes of W 0 . A final configuration is a configuration C f = (W f , Ass f , Dass f ) such that W f contains only node n f , Ass f is the empty map, and Dass f (n f ) represents the dataset that has to be returned to the client, and that has been assembled during the execution of all nodes preceding n f . The intuitive understanding of this type of configuration is that n f needs not be executed, and simply terminates the workflow by returning final output data. Note that due to data assignment, there can be more than one final configuration, and we denote by C f the set of all final configurations.

We define the operational semantics of a complex workflow with the following 4 rules. Rule 1 defines the task assignment to free workers, Rule 2 defines the execution of an atomic task by a worker, Rule 3 defines the execution of an automated task, and Rule 4 formalizes refinement.

Rule 1 (Worker Assignment): A worker u ∈ U is assigned a task t = λ(n) if t ∈ T aut . The rule applies if u is free and has the skills required by t, and if node n is not already assigned to a worker. Note that a task can be assigned to an user even if it does not have input data yet, and is not yet executable.

n ∈ Dom(Ass) ∧ u ∈ coDom(Ass)∧ sk(u j ) ∩ T cs (λ(n)) = ∅ ∧ λ(b) ∈ T aut (W, Ass, Dass) → (W, Ass ∪ {(n, u)}, Dass) (1)
Consider for instance the application of rule R 1 described in Figure 4. Configurations are represented by the contents of dashed rectangles. Workflow nodes are represented by circles, tagged with a task name representing map λ. The dependencies are represented by plain arrows between nodes. Worker assignments are represented by dashed arrows from a worker name u i to its assigned task. Data assignment are represented by double arrows from a dataset to a node. The left part of Figure 4 represents a configuration C with four nodes n 1 , n 2 , n 3 and n f . The predecessors of n 1 and n 2 have been executed. Node n 1 represents occurrence of a task of type t 1 and is attached dataset D 1 . Let us assume that D 1 is a database containing bee pictures, and that task t 1 cannot be automated (t 1 ∈) and consists in tagging these pictures with bee names, which requires competences on bee species. Let us assume that worker Smith is currently not assigned any task and has competences on bees. Then sk(Smith) ∩ T cs (t 1 ) = ∅ and rule R 1 applies. The resulting configuration is configuration C at the right of the Figure, where the occurrence of t 1 represented by node n 1 is assigned to worker Smith.

Rule 2 (Atomic Task Completion): An atomic task t = λ(n) can be executed if node n is minimal in the workflow, it is assigned to a worker u = Ass(n) and its input data Dass(n) does not contain an empty dataset. Upon completion of task t, worker u publishes the produced data D out to the succeeding nodes of n in the workflow and becomes available.

n ∈ min(W ) ∧ λ(n) ∈ T ac ∧ Ass(n) = u ∧ Dass(n) ∈ DB * .∅.DB * ∧ ∃D out = D out 1 . . . D out k ∈ F λ(n),u (Dass(n)), Dass = Dass \ {(n, Dass(n))}∪ {(n k , Dass(n k ) [j/D out k ] ) | n k ∈ succ(n) ∧n is the j th predecessor of n k } (W, Ass, Dass) λ(n) ---→ (W \n, Ass\{(n, u)}, Dass ) (2)
Consider the example of Figure 5. We start from a configuration in which worker Smith has to tag images stored in a dataset D 2 . We assume that the relational schema for D 2 is a tuple R(id, pic) where id is a key and pic a picture. We also assume that tags are species names from a finite set of taxons, e.g. T ax = {Honeybee, Bumblebee, M asonbee, ..., U nknown}. Worker Smith performs the tagging task, which results in a dataset D 3 with relational schema R (id, pic, tag). One can notice that no information is given of the way worker Smith tags the pictures in D 2 , the only insurance is that for every tuple R(id, pic), there exists a tuple R (id, pic, t) in D 3 where t ∈ T ax. Notice that application of this rule may results in several successor configurations, as each tag attached to a tuple is a non-deterministic choice of the worker realizing the task. Rule 3 (Automatic Task Completion): An automatic task t = λ(n) can be executed if node n is minimal in the workflow and its input data does not contain an empty dataset. The difference with atomic tasks completion is that n is not assigned an user, and that the produced outputs are a deterministic function of task inputs. Consider the example of Figure 6. We resume from the situation in Figure 5, i.e. with two nodes n 2 , n 3 remaining to be executed before n f , and with a dataset composed of tagged images attached to node n 3 . Let us assume that task t 3 is an automated task that consists in pruning out images with tag "unknown". This task can be realized as a projection of D 3 of tuples R (id, pic, t) such that t = "U nknown". As a result, we obtain a dataset D 4 , used as input by node n f such that ∀R (id, pic, t) ∈ D 3 ∧ t = "unknown", ∃R (id, pic, t) ∈ D 4 and the task can be realized by simple SQL query.

n ∈ min(W ) ∧ λ(n) ∈ T aut ∧ Dass(n) ∈ DB * .∅.DB * ∧D out = f λ(n),u (Dass(n)) = D out 1 . . . D out k , Dass = Dass \ {(n, Dass(n))}∪ {(n k , Dass(n k ) [j/D out k ] ) | n k ∈ succ(n) ∧n is the j th predecessor of n k } (W, Ass, Dass) λ(n) ---→ (W \n, Ass, Dass ) (3)

Rule 4 (Complex Task refinement):

The refinement of a node n with t = λ(n) ∈ T cx by worker u = Ass(n) replaces node n by a workflow W s = (N s , -→ s , λ s ) ∈ P rof ile(t, u). Data originally accepted as input by n are now accepted as input by the source node of W s . All newly inserted nodes have empty input datasets.

t = λ(n) ∈ T cx ∧ W s ∈ P rof ile(t, Ass(n)) ∧Dass (min(W s )) = Dass(n) ∧∀x ∈ N s \ min(W s ), Dass (x) = ∅ |P red(x)| ∧Ass = Ass\{(n, Ass(n))} (W, Ass, Dass) ref (n) ----→ (W [n/Ws] , Ass , Dass ) (4) n1 t1 n2 t2 n3 t3 n f C D1 D2 Smith R4 n 1 t5 n 2 t6 n 3 t7 n 4 t8 n2 t2 n3 t3 n f C D1 D2 Fig. 7. Application of semantic rule R4
Consider the example of Figure 7. Let us assume that Worker "Smith" is assigned task t 1 and that this task is a complex tagging task (for instance workers are asked to find names of rare species). In such situation, Smith can decide to replace the task by a simple single-worker tagging mechanism, or by a more complex workflow, that asks a competent worker to tag pictures, then separates the obtained datasets into pictures with/without tag "Unknown", and sends the unknown species to an expert ( for instance an entomologist) before aggregating the union of all responses. This refinement lead to a configuration C , shown in the right part of Figure 7, where n 1 is a tagging task, n 2 is an automated task to split a dataset, n 3 is a tagging tasks which requires highly competent workers and n 4 is an aggregation task. In our model, we assume that refinement is always performed by a competent worker, owning an appropriate profile to handle the refinement.

Note that the definition of a complex task is very subjective and varies from one worker to another. Classifying tasks as complexor not a priori should not be seen as a limitation, as refinement is not mandatory: a worker can replace a node n with another node labeled by task t ∈ T cx by a node labeled by an equivalent task t ∈ T ac ∪ T aut if this possibility appears in her profile. This allows to model situations where a worker refines a task because she thinks it is too complex to be handled by a single person.

We will say that there exists a move from a configuration C to a configuration C , or equivalently that C is a successor of configuration C and write C C whenever there exists a rule that transforms C into C .

Definition 5 (Run).

A run ρ = C 0 .C 1 . . . C k of complex workflow CW with workers U is a finite sequence of configurations such that C 0 is an initial configuration, and for every i ∈ 1 . . . k, there exists a move from C i-1 to C i . A run is maximal if C k has no successor. A maximal run is terminated iff C k is a final configuration, and it is deadlocked otherwise. In the rest of the paper, we denote by Runs(CW, D in ) the set of maximal runs originating from initial configuration C 0 = (W 0 , Ass 0 , Dass 0 ) (where Dass 0 associates dataset D in to node n i ). We denote by Reach(CW, D in ) the set of configurations that can be reached from C 0 . Along a run, the datasets in use can grow, and the size of the workflow can also increase, due to decomposition of tasks. Hence, Reach(CW, D in ) and Runs(CW, D in ) need not be finite. Even when Reach(CW, D in ) is finite, a complex workflow may exhibit infinite cyclic behaviors.

Moves in executions of complex workflows consists in workflow rewriting, computation of datasets, and appropriate transfer of datasets from one task to another. Complex tasks and their refinement can encode unbounded recursive schemes. For instance, consider a simple linear workflow composed of three nodes :

n i , n f , n 1 where n 1 is attached task λ(n 1 ) = t 1 such that -→= {(n i , n 1 ), (n 1 , n f )}.
Let us assume that our system has a single user, and that this user has a decomposition profile (t 1 , W t1 ) where W t1 is a workflow with three nodes w 1 , w 2 , w f , such that λ(w 1 ) = t 2 and λ(w 2 ) = t 1 and where -→= {(w 2 , w 1 ), (w 1 , w f )}. Then, after application of rule R1 (assigning user 1 to the node that carries task t 1 ) and R4 (replacing t 1 by W t1 ), one obtains a larger workflow that still contains an occurrence of task t 1 . One can repeat these steps an arbitrary number of times, leading to configurations which workflow parts are growing sequences of nodes labeled by sequences of task occurrences of the form λ(n i ).t k restriction, complex workflows define transitions systems of arbitrary size, with growing data or workflow components, and with cycles.

Data and First order

We have introduced the standard data representation via relational schemas in section 3.3, i.e. a representation of records by tuples of the form rn(a 1 , . . . , a n ), where rn is a relation name and a 1 , . . . a n attributes that fulfill the constraints of the legal domain of relation rn. As detailed in section 4, a client of a complex workflow can give constraints to reduce the range of legal input data, or constraints on expected outputs of a complex workflow. Similarly, we show in section 6 that deciding termination needs to consider properties of datasets contents during configuration changes. In the rest of the paper, we will use First Order Logic (FO) to address properties of datasets.

Decidability for FO fragments

Definition 6 (First Order). A First Order formula (in prenex normal form) over a set of variables X is a formula of the form φ ::= α(X).ψ(X) where α(X) is an alternation of quantifiers and variable names in X, i.e. sentences of the form ∀x 1 ∃x 2 , ... called the prefix of φ and ψ(X) is a quantifier free formula called the matrix of φ. ψ(X) is a boolean combinations of atoms of the form R i (x 1 , . . . x k ), P j (x 1 , . . . x n ), where R i (x 1 , . . . x k )'s are relational statements, and P j (x 1 , . . . x n )'s are predicates, i.e. boolean function on x 1 , . . . x n .

In the rest of the paper, we consider variables that either have finite domains or real valued domains, and predicates specified by simple linear inequalities. In particular we will consider equality of variables, i.e. statements of the form x i = x j . This class of constraints in well known, and deciding whether there exists an assignment satisfying such constraint can be done in polynomial time [START_REF] Khashiyan | Polynomial algorithms in linear programming[END_REF]. When a constraint over n variables is an expression of the form x i -x j ≤ c ∧ x i ≤ c where x i , x j are variables, and c a constant, it can be encoded as differential bound matrix (DBM), and emptiness of the domain represented by such a DBM where variables a real valued can be checked in O(n 3 ).

Letting X 1 = {x 1 , . . . x k } ⊆ X we will often write ∀ → X 1 instead of ∀x 1 .∀x 2 . . . ∀x k . Similarly, we will write ∃ → X 1 instead of ∃x 1 .∃x 2 . . . ∃x k . Given an FO formula in prenex normal form, we will use w.l.o.g. formulas of

the form ∀ → X 1 ∃ → X 2 . . . ψ(X) or ∃ → X 1 ∀ → X 2 . . . ψ(X)
, where ψ(X) is quantifier free matrix, and for every i = j, X i ∩ X j = ∅. Every set of variables X i is called a block. By allowing blocks of arbitrary size, and in particular empty blocks, this notation captures all FO formulas in prenex normal form. We denote by φ [t1/t2] the formula obtained by replacing every instance of term t 1 in φ by term t 2 . Each variable x i in X has its own domain Dom(x). A variable assignment (for a fixed set of variables X) is a function µ that associates a value d x from Dom(x) to each variable x ∈ X. Given a variable assignment µ, we say that φ hold under µ, and write µ |= φ iff φ evaluates to true under assignment µ.

Definition 7 (satisfiability).

A variable free formula is satisfiable iff it evaluates to true. A formula of the from ∃x, φ(x) is satisfiable if and only if there is a way to choose a value for x such that φ(x) is satisfied, i.e. there exists a value d x ∈ Dom(x) such that φ(x) [x/dx] is satisfiable. A formula of the form ∀x, φ(x) is true if and only if, for every possible choice of a value

d x ∈ Dom(x) for x, φ(x) is satisfiable, i.e φ(x) [x/dx] is satisfiable.
It is well known that satisfiability of first order logic is undecidable in general, but it is decidable for several fragments. The universal fragment of FO is the set of formulas of the form ∀ -→ X 1 φ, where φ is quantifier free. Similarly, the existential fragment of FO contains only formulas of the form ∃ -→ Y 1 φ. Consider again our setting, where predicates in FO formula can be encoded by relations and boolean predicates that are linear inequalities. Then checking satisfiability of the existential/universal fragment of FO can be done non-deterministically in polynomial time.

Proposition 1. Let X be a set of variables of the form X = X b X r where variables from X b take values from finite domains and variables from X r take values in R. Then, satisfiability of formulas of the form

φ ::= ∃ -→ X . i∈1..I R i (X) ∧ j∈1..J P j (X) is NP-complete.
Proof. Let us first show that the problem belongs to NP. Let us consider an existential formula φ ::= ∃ -→ X .ψ where ψ contains positive relational statements of the form φ R+ ::= R 1 (X), . . . R k (X), and negative relational statements of the form φ R-::= ¬R 1 (X), . . . ¬R k (X), and predicates of the form P 1 (X), . . . P J (X). For each R i (x 1 , . . . , x q ) in φ R+ , with relational schema rn i and legal domain Dom i , we define Ldom i as the constraint (x 1 , . . . x q ) ∈ Dom i . One can choose nondeterministically in polynomial time a value d x for each bounded variable x in X b .

Then one can choose non-deterministically which relational statements and predicate hold, by guessing a truth value v j ∈ {true, f alse} for each relation R i ∈ 1..I (Resp. predicate P j , j ∈ 1..J). Now, for each pair of choices where rn(x 1 , . . . x q ) holds and rn(x 1 , . . . x q ) does not, we verify that the designed tuples are disjoint, i.e. that ¬(x 1 = x 1 ∧ • • • ∧ x q = x q ). We call φ RxR the formula that is the conjunction of such negations. The size of φ RxR is in O(r.|φ 2 |) where r is the maximal arity in a relational schema of the complex workflow. We can then verify that the guess of truth value for atoms yields satisfaction of φ, i.e. check that φ [Ri,Pj /true,f alse,vj ] evaluates to true. In case of positive answer, it suffices to check that with the truth value choosen for atoms, the formula φ RxR ∧ i∈1..k

Ldom i ∧ vi=true P i ∧ vi=f alse
¬P i is satisfiable, which can be done in polynomial time. Now, for the hardness proof, one can easily encode a SAT problem with an FO formula over boolean variables. Checking satisfiability of a universally quantified formula can be done in the same way, as ∀Xφ is satisfiable iff ∃X, ¬φ is not.

One needs not restrict to existential or universal fragments of FO to decidability of satisfiability. A well known decidable fragment is (F O 2 ), that uses only two variables [START_REF] Mortimer | On languages with two variables[END_REF]. However, as this fragment forbids in particular atoms of arity greater than 2, which is a severe limitation when addressing properties of datasets.

The BS fragment of FO is the set of formulas of the form ∃ → Y 1 .∀ → X 2 .ψ, where ψ is quantifier free, may contain predicates, but no equality. The Bernays-Schonfinkel-Ramsey (BSR) fragment of F O [START_REF] Bernays | Zum entscheidungsproblem der mathematischen logik[END_REF] extends the BS fragment by allowing equalities in the matrix ψ. Satisfiability of a formula in the BS or BSR fragment of FO is NEXPTIME-complete [START_REF] Harry | Complexity results for classes of quantificational formulas[END_REF]. Algorithms to check satisfiability for a fragments of FO can be obtained by transforming formulas from that class into an equivalent or equisatisfiable formulas of a decidable subclass. Two FO formulas φ and ψ are equivalent iff, for every variable assignment µ, µ |= φ iff µ |= ψ. They are equisatisfiable iff an assignment µ such that µ |= φ exists iff an assignment µ such that µ |= ψ exists. Transformation of this type are usually expensive, and result in a blowup of the size of considered formulas.

Recent results [START_REF] Sturm | Deciding first-order satisfiability when universal and existential variables are separated[END_REF] exhibited a new fragment, called the separated fragment of FO, defined as follows: Let V ars(A) be the set of variables appearing in an atom A. We say that two sets of variables Y, Z ⊆ X are separated in a quantifier free formula φ(X) iff for every atom A of φ(X), V ars(A)∩Y = ∅ or V ars(A)∩Z = ∅.

A formula in the Separated Fragment (SF ) of F O is a formula of the form ∀ → X 1 .∃ → Y 2 . . . . ∀ → X n .∃ → Y n φ, where → X 1 • • •∪ → X n and → Y 1 • • •∪ → Y n are separated.
The SF fragment is reasonably powerful and subsumes the Monadic Fragment [START_REF] Löwenheim | Über möglichkeiten im relativkalkül[END_REF] (where predicates can only be unary) and the BSR fragment. Every separated formula can be rewritten into an equivalent BSR formula (which yields decidability of satisfiability for SF formulas), but at the cost of an n-fold exponential blowup in the size of the original formula. Satisfiability of a separated formula φ is hence decidable [START_REF] Sturm | Deciding first-order satisfiability when universal and existential variables are separated[END_REF], but with a complexity in O(2 ↓n |φ| ).

A recent and interesting extension of F O 2 called F O 2 BD allows atoms of arbitrary arity, but only formulas over sets of variables where at most two variables have unbounded domain. It was demonstrated that F O 2 BD formulas are closed under computation of weakest preconditions for a set of simple SQL operations [START_REF] Itzhaky | On the automated verification of web applications with embedded SQL[END_REF]. In the rest of the paper, we will show classes of complex workflows for which termination and proper termination are decidable. All the results demonstrated in our paper would hold in a F O 2 BD setting. However, complex worklfows handle imprecise worker inputs, and imprecise values of such fields are better captured with unbounded domains.

We will show hereafter that the universal fragment of FO suffices to encode conditions needed for basic operation to produce an empty dataset. Similarly, we will show that the universal fragment sufficed to encode the weakest preconditions required to satisfy an universal formula. This will be of particular importance to prove decidability of termination.

Closure of FO classes

In section 6, we will give an algorithm to check termination of a complex workflow with bounded recursion. Roughly speaking, this algorithms searches a reachable configuration C bad where emptiness of a dataset D could stop an execution. Once such a configuration is met, it remains to show that the statement D = ∅ is compatible with the insertion, projections, unions of datasets performed during the execution before reaching C bad . This is done by computing backward the weakest preconditions ensuring D = ∅ along the followed run, and checking that each condition is satisfiable. Definition 8. Let C -→ C be a move from configuration C to C of a complex workflow. Let m be the nature of this move (an automated task realization, an user assignment, a refinement,...). We denote by wp[m]ψ the weakest precondition required for C such that ψ holds in C after move m.

Weakest precondition were introduced in [START_REF] Dijkstra | Guarded commands, nondeterminacy and formal derivation of program[END_REF] as a way to prove correctness of programs. In a program written in an imperative language, if the property ψ is an inequality of the form ψ 1 ::= x ≤ 10 and m the instruction x := x + 1, then wp[x := x + 1]ψ 1 is the property x ≤ 9. Calculus of weakest precondition was also proposed to verify web applications with embedded SQL [START_REF] Itzhaky | On the automated verification of web applications with embedded SQL[END_REF].

Proposition 2. Let CW be a complex workflow, r be the maximal arity of relational schemas in CW and ψ be an FO formula. Then for any move m of CW , wp[m]ψ is effectively computable, and is of size in O(r.|ψ|).

Proof (sketch). The effect of moves on the contents of datasets can be described as sequential composition of basic operations that are projections of datasets, insertions of records or fields, unions or joins of dataset. Let D 1 , . . . D k be the datasets that have to satisfy ψ. If some D i is obtained as a projections of a dataset D i , then D i contains only records of D i satisfying some predicate P . The precondition will hence be obtained by a simple replacement in ψ of any statement of the form rs(

-→ x ) ∈ D i by rs( -→
x ) ∈ D i ∧ P . If D i is obtained after insertion of a fresh record in some dataset D i then every statement rs( -→

x ) ∈ D i can be replaced by a subformula (rs(

-→ x ) ∈ D i ∨ In( -→
x )) where In( -→ x ) represents constraints on legal values of inputs in a dataset with the same relational schema as D i . Note that In(

-→
x ) is a quantifier free boolean combination of predicates.

Similarly, if some dataset D i is obtained as the union of two datasets D 1 , D 2 , the precondition for ψ should consider, for every statement of the form rs( -→

x ) ∈ D i , cases where rs( -→

x ) belongs to D 1 and cases where rs( -→ x ) belongs to D 2 . These two cases are exclusive, and as tuples identified by -→

x have to appear in at least one dataset (either D 1 or D 2 ) we simply replace atoms of the form rs(

-→ x ) ∈ D i by the disjunction rs( -→ x ) ∈ D 1 ∨ rs( -→
x ) ∈ D 2 . We also replace negative statements rs(

-→ x ) ∈ D i by conjunction rs( -→ x ) ∈ D 1 ∧ rs( -→ x ) ∈ D 2 . The size of the obtained formula is hence in O(2.

|ψ|).

If some D i is obtained by creation of a field for each record in dataset D i , then relational statement rs(

-→ x ) ∈ D i is replaced by another statement rs( -→ y ) ∈ D i ∧ P ( -→ y ) where -→ y is a subset of -→
x , and P ( -→ y ) is a quantifier free predicate indicating constraint on -→ y obtained after variable elimination when -→

x takes legal values imposed by relational schema of D i (i.e. it satisfies Ldom i -see proof of Proposition 1-) and satisfies the constraints of relational schema of D i .

For joins, relation of the form rs( -→ X i ) are transformed in statements of the form rs(

-→ Y i )∧rs( -→ Z i )∧y 1 = z 1 ,
where

y 1 ∈ -→ Y i and z 1 ∈ -→
Z i . This may multiply the size of the formula by r. We refer interested readers to appendix A.5 for details on the construction of weakest preconditions.

Computing a weakest precondition is mainly a syntactic replacement of a set of relational statements, or a disjunction of such replacements, that changes the number of variables. However, it does not change the number of quantifier blocks nor their ordering, and it does not introduce new quantifiers when replacing an atom. We hence easily obtain the following corollary:

Corollary 1. The existential, universal, BSR and SF fragments of FO are closed under calculus of a weakest precondition in Complex Workflows.

Termination

Complex workflow use the knowledge and skills of crowd workers to complete a task starting from input data provided by a client. However, a workflow may never reach a final configuration. This can be due to particular data input by workers that cannot be processed properly by the workflow, to infinite recursive schemes appearing during the execution, to deadlocked situations due to missing worker competences. It is hence important to detect whether some/all runs of a system eventually reach a final configuration in C f .

In this section we address the questions of existential and universal termination. We first show that existential termination is undecidable, regardless of the inputs specified for a workflow. We then show that decidability and complexity of universal termination depends on the power allowed to specify inputs of the workflow.

Existential termination

Definition 9 (Deadlock, Termination). Let CW be a complex workflow, D in be an initial dataset, D in be a set of datasets. CW terminates existentially on input D in iff there exists a run in Runs(CW, D in ) that is terminated. CW terminates universally on input D in iff all runs in Runs(CW, D in ) are terminated. Similarly, CW terminates universally (resp. existentially) on input set D in iff CW terminates universally (resp. existentially) on every input D in ∈ D in .

When addressing the termination question for a set of inputs D in , we describe D in symbolically with a decidable fragment of FO (e.g. the existential, universal, BSR or separated fragment of FO introduced in section 5). Termination questions are meaningful for clients and workflow designers. Existential termination ensures that an answer to a client (an output dataset D out ) can be returned. This is an essential sanity check for a particular input D in : if a complex workflow never returns an answer when using D in as input, then this dataset can be the cause of the problem. If a complex workflow CW does not terminate for a set of inputs D in depicting possible entries provided by a client, then CW can be considered as ill-formed. Similarly, universal termination provides guarantees on the correctness of CW . If CW terminates for all inputs, then every input of a client will be processed and the computed answer returned. This does not yet means that the computed data is always correct, but at least that the execution of a workflow will terminate for this input or all legal inputs provided by the client. We will show in this section that existential termination is undecidable, and universal termination is in co -N EXP T IM E.

Theorem 1. Existential termination of complex workflows is an undecidable problem.

Proof (sketch). Complex workflows can simulate any two counters machine. The encoding proceeds as follows: each instruction i of the counter machine is encoded as a specific task t i , that can be refined by only one worker u i . The workflow W i chosen for refinement by u i is then executed until it contains a single node representing the next instruction. Counters are encoded as the number of occurrences of specific tags c 1 , c 2 in a field of a dataset. When simulating a zero test and decrement instruction i, worker u i has to guess whether the value of a counter is zero or not (this is encoded as a choice of a particular workflow to refine t i ). If the worker does the wrong guess, the execution deadlocks. Otherwise, the execution always proceeds to the next instruction. More details on the encoding are provided in Appendix A.1.

The question of termination for a set of initial datasets is also undecidable (it suffices to write D in = {D in } to get back to the former termination question).

Remark 1. Notice that the undecidability of existential termination does not arise from complex manipulation of data by workers nor by automated tasks. This undecidability occurs as soon as higher order operations are allowed, and distribution of datasets to successor nodes is allowed for non-empty datasets only.

Universal Termination

Universal termination is somehow an easier problem than existential termination. We show in this section that it is indeed decidable for many cases and in particular when the datasets used as inputs of a complex workflow are explicitly given or are specified in a decidable fragment of F O. We proceed in several steps. We first define symbolic configurations, i.e. descriptions of the workflow part of configurations decorated with relational schemas depicting data available as input of tasks. We define a successor relation among these symbolic configurations. We then define the class of non-recursive complex workflows, in which all executions are finite, and give a bound K Tcx on the length of executions in non-recursive specifications. The next step is to show that given a symbolic executions ρ S of length n, and a description of inputs, the complexity of checking whether there exists an execution ρ that coincides with ρ S is at least in 2EXP T IM E. This proof builds on the iterative calculus of weakest preconditions needed to allow a particular run. The complexity originates mainly from the growth of formulas depicting weakest preconditions at each iteration. Deciding universal termination builds on the same construction. We show that recursive specifications do not terminate universally (they either deadlock or continue forever). This gives a bound on the length of runs that have to be considered for recursion-free complex workflows, and allows to prove that the complexity of universal termination is at least in co -2EXP T IM E.

Let us first define symbolic configurations. Roughly speaking, a symbolic configuration describes the status of workflow execution as in standard configurations (see defn. 4) but leaves the data part underspecified.

Definition 10 (symbolic configuration). Let CW = (W 0 , T , T cs , U, sk, P) be a complex workflow with database schema DB. A symbolic configuration of CW is a triple C S = (W, Ass, Dass S ) where W = (N, → , λ) is a workflow, Ass : N → U assigns workers to nodes, and Dass S : N → (DB) * associates a list of relational schema to nodes of the workflow.

For every node n that is minimal in W , the meaning of Dass S (n) = rs 1 , . . . rs k is that task attached to node n takes as inputs datasets D 1 . . . D k where each D i conforms to relational schema rs i . Notice that it is sufficient to know λ(n) to obtain Dass S (n). A symbolic configuration C S j = (W j , Ass j , Dass S j ) is the successor of a symbolic configuration C S i = (W i , Ass i , Dass S i ) iff one of the following situation holds:

there exists u ∈ U and n ∈ W i , Ass -1 i (u) = ∅, W j = W i , Dass S = Dass S and Ass j = Ass i {(n, u)} there exists n ∈ min(W i ) such that t = λ(n) is an automated task (resp. an atomic task) manipulating datasets D 1 , . . . D q , with successors n 1 , . . . n k , W j = W i \ {n} Dass S assigns to each successor n j the relational schema corresponding to f t (D 1 , . . . D q ) (resp. F t (D 1 , . . . D q )). there exists n ∈ W i , λ(n) is a complex task, and Ass(n) = u, W j is the workflow obtained by replacement of n in W i by a workflow W new ∈ P(λ(n), u). Dass S assigns to the copy of minimal node n j of W new the relational schemas in Dass S i (n).

We denote by SC(C S i ) the set of successor configurations of symbolic configuration C S i .

Definition A deadlocked symbolic configuration represents a situation where a workflow progress is blocked due to shortage of competent users to execute tasks. These configurations should be avoided to terminate the execution of a complex workflow. A potential deadlock is a symbolic configuration from which absence of data in a particular dataset may stop an execution. We use the term potential deadlock because one cannot know from a symbolic configuration whether a particular dataset D i is empty. We will show in this section that one can decide whether a potential deadlock situation in C S represents a real and reachable deadlock, by considering how the contents of dataset D is forged along the execution leading to C S .

Definition 12 (Symbolic execution). A symbolic execution is a sequence ρ

S = C S 0 m1 -→ C S 1 m2 -→ . . . m k -→ C S k
where each C S i is a symbolic configuration, and:

-C S 0 = (W 0 , Ass 0 , Dass S ) where W 0 , Ass 0 have the same meaning as for configurations, and Dass S associates to the minimal node n 0 in W 0 the relational schema of Ass 0 (n 0 ). -C S i+1 is a successor of C S i .

One can associate to every execution of a complex workflow

ρ = C 0 m1 -→ C 1 . . . C k a symbolic execution ρ S called its signature. We can compute ρ S = C S 0 m1 -→ C S 1 m2 -→ . . . m k -→ C S k
, by replacing data assignment in each C i = (W i , Ass i , Dass i ) by a function from each node n to the relational schemas of the datasets in Dass i (n). It is not true, however, that every symbolic execution is the signature of a plain execution of CW , as some moves might not be allowed when a dataset is empty (this is for instance the case for tasks that split data into several subsets, and require the split input to contain tuples). A natural question when considering a symbolic execution ρ S is whether this signature corresponds to an actual run of CW . The proposition below shows that the decidability of this question depends on assumptions on the inputs of CW . Proposition 3. Let CW be a complex workflow, D in be a dataset, D in be an FO formula with n in variables, and ρ S = C S 0 . . . C S i be a symbolic workflow. Then deciding if there exists a run ρ with input dataset D in and signature ρ S is in 2EXP T IM E. Checking if there exists a run ρ of CW and an input dataset

D in that satisfies D in with signature ρ S is -undecidable in general. -in 2EXP T IM E if D in is in the universal/existential fragment of FO, or in the BSR fragment of FO, -n in -f oldEXP T IM E in the size of D in if D in is in the separated fragment of FO Proof.
We check feasibility of ρ S , that is starting from C S i , check that all conditions met along a run with signature ρ S to reach a configuration C i that is compatible with C S i are met at each step, and allow for existence of configurations C 0 , C 1 , . . . C i-1 . First notice that the actual run with signature ρ S performs the same sequence of moves as in ρ S , and that the question of existence of a run ρ with signature ρ S only questions satisfiability of constraints on data computed at each step of this run, not the sequence of moves along ρ. Second, one can notice that if ρ S contains a deadlock, it is necessarily the last symbolic configuration of the run. So one needs not check existence of a deadlock separately when checking feasibility of ρ S . A third remark is that semantic rules that affect users to tasks or perform a refinement do not consider data contents. Hence, if the move from C i-1 to C i is an user assignment or a refinement, then it is necessarily feasible as long as C i-1 is reachable. The only cases where data can affect execution of a step along a run is when an automated task or an atomic task has to process empty data. For each of these steps, one has to check that the inputs of an executed task are not empty, i.e. suppose that

D 1 = ∅ ∧ • • • ∧ D k = ∅.
Non-emptiness of a dataset D k at some configuration C i-1 is a property that depends on previous steps in the execution. For instance, if the move from C i-2 to C i-1 realizes the projection of a dataset, i.e. filters records in a dataset D k to keep only those that satisfy some predicate P , then the precondition that must hold at C i-2

is ψ i-2 ::= ∃ -→ X P (X). Similarly, if the move C i-2 mi-1 -→ C i-1 is
a transformation of records, a transformation of some dataset that adds new fields, a join of two datasets, the formula ψ i-2 is an existential FO formula.

This generalizes to the whole signature. Let ψ k be an FO formula that has to be satisfied by configuration C k in a run compatible with signature ρ S . There exists a sequence of moves

C 0 m1 -→ C 1 . . . m k -→ C k iff the sequence C 0 m1 -→ C 1 . . . m k-1 -→ C k-1 ends in a configuration C k-1 such that C k-1 |= wp[m k ]ψ k (

by definition of weakest precondition). If wp[m

k ]ψ k is not satisfiable, then the move from C k-1 to C k always ends with datasets that do not fulfill ψ k . One can decide whether wp[m k ]φ k is satisfiable, as ψ k is in a decidable fragment of FO, then by Prop. 1, one can effectively compute wp[m k ]ψ k and the obtained formula belongs to the same FO fragment as ψ k . Now, in addition to the weakest preconditions for ψ k to hold, one may have to assume that several datasets are non-empty at stages k -1. Adding a statement D i = ∅ at several steps of the signature just adds an existential conjuct, to all ψ i s are in the existential fragment of FO, which is preserved by weakest precondition computation (Prop. 1). Now, one can build inductively all weakest preconditions ψ k-1 , ψ k-2 , . . . , ψ 0 that have to be satisfied respectively by configurations C k-1 , . . . , C 0 . If any of these preconditions is unsatisfiable, then there exists no run with signature C S 0 . . . C S k leading to a configuration that satisfies ψ k , and hence ρ S is not the signature of an actual run of CW . One can notice also that, according to Prop. 1, the size of ψ 0 can be in O(r k ) where r is the maximal arity of relational schemas of the complex workflow. Hence, checking all preconditions for a run of size k compatible with ρ S can have a complexity that is in O(2 r k ).

Assume that ψ k-1 , ψ k-2 , . . . ψ 0 are satisfiable. It remains to show that the input(s) of the complex workflow satisfy the weakest precondition for the execution of ρ S , i.e. satisfy ψ 0 . Then, when the input is a single dataset D in , it remains to check that D in |= ψ 0 to guarantee existence of a run with signature C S 0 . . . C S k that starts with input data D in and leads to a configuration C k . This can be done in

O(|D ψ0 in |), that is in O(|D in | r k ).
As the complexity of checking satisfiability of weakest preconditions ψ k . . . ψ 0 is in EXP T IM E in the size of the largest formulas, the overall complexity is in 2EXP T IM E.

Similarly, if D in is given as a FO formula, the complexity depends on the considered fragment used to specify D in . In general, if D in is given as a FO formula, it is undecidable if D in ∧ ψ 0 is satisfiable. If D in is an existential/universal formula, then the complexity is exponential in the size of D in and also exponential in the size of ψ 0 . Assuming that |D in | ≤ 2 k we have a 2EXP T IM E complexity. If D in is in the BSR fragment, then checking satisfiability of D in is in 2EXP T IM E, and so the overall process is in 2EXPTIME. Last if D in is in the separated fragment, then checking its satisfiability is n in -fold exponential in the size of D in , so the overall process of checking realizability of ρ S has an n in -fold exponential complexity.

An execution ρ = C 0 . . . C k of a complex workflow terminates iff the reached configuration is of the form C k = (W f , Ass f , Dass f ) where W f contains only the final node of a workflow. Checking termination hence amounts to checking whether one can reach such a configuration. A run that does not terminate is a run that either ends in a configuration that is not final and from which no rule can be applied, or an infinite run. A move from C i to C i+1 leaves the number of nodes unchanged (application of worker assignment rule R 1 ), decreases the number of nodes ( execution of an atomic task (R2), or of an automated task (R3)), or refines a node in W i (application of rule R 4 ). Only in this latter case, the number of nodes may increase. The set of possible transformations of W and Ass occurring from C is bounded. Further, semantic rule R4 is the only rule that creates new nodes in the workflow part of a configuration. So when the number of occurrences of rule R4 in a run is bounded, the number of applications of rules R1,R2,R3 and hence the size of (symbolic) executions is also bounded. Complex workflows that can exhibit infinite runs are hence specification with recursive rewriting schemes. Definition 13. Let t be a complex task. We denote by Rep(t) the task names that can appear when refining task t, i.e.

Rep(t) = {t | ∃u, W, n, sk(u) ∩ T cs (t) = ∅ ∧ W ∈ P rof ile(t, u), n ∈ W ∧ λ(n) = t }. The rewriting graph of a complex workflow CW = (W 0 , T , T cs , U, sk, P) is the graph RG(CW ) = (T cx , -→ R ) where (t 1 , t 2 ) ∈-→ R iff t 2 ∈ Rep(t 1
). Then CW is recursion-free if there is no cycle of RG(CW ) that is accessible from a task appearing in W 0 .

When a complex workflow is not recursion free, then some executions may exhibit infinite behaviors in which some task t i is refined infinitely often. Clearly, this prevents termination. Such an infinite rewriting loop can be either stopped because it appears in a sequence of moves that deadlocks, or be executable, hence preventing reaching final configurations in which all tasks have been executed. We claim without proof the following property: Proof. Building RG(CW ) can be done in O(|P(T cx , U)|). Checking existence of a cycle in RG(CW ) that is accessible from some task in W 0 can be done in polynomial time in the size of RG(CW ), for instance using a DFS algorithm, than runs in time at most |T cx | 2 .

In executions of recursion free CWs, a particular task t can be replaced by a workflow that contains several tasks t 1 , . . . t k that differ from t. Then, each t i can be replaced by workflows combining other tasks that are not t nor t i , and so on... For simplicity, we assume that W 0 and all workflows in profiles have nodes labeled by distinct task names. We can easily prove the following: Proposition 6. Let C = (W, Ass, Dass) be a configuration of a recursion free complex workflow CW . Then there exists a bound K Tcx on the size of W , and the length of a (symbolic) execution of CW is in O(3.K Tcx ) Proof (sketch). We assume, without loss of generality, that all workflows in all profiles have nodes labeled by distinct task names, and the initial workflow has a single node. Let d be the maximal number of new occurrences of complex tasks that can be rewritten in one refinement (i.e. the maximal number of complex tasks that appear in a profile). Each rewriting adds at most d -1 complex tasks to the current configuration. The number or rewriting is bounded, as CW is recursion free. For a given node n appearing in a configuration C k along a run, one can trace the sequence of rewriting P ast(n) performed to produce n. As a task t = λ(n) is replaced by a workflow W t during refinement only if none of the tasks labeling nodes of W t appears in the past of n. Hence, the number of nodes in a configuration is at most K Tcx = d Tcx . Now, for a given configuration, the number of applications of rules R1,R2, and R3 is bounded, and reduces the number of nodes in the workflow part of the configuration. Proposition 7. A complex workflow terminates universally iff the following conditions hold: i) it is recursion free ii) it has no (symbolic) deadlocked execution iii) there exists no run with signature C S 0 . . . C S i where C S i is a potential deadlock, with D k = ∅ for some D k ∈ Dass(n j ) and for some minimal split node n j of W i .

Proof. If CW has recursive task rewriting, then there is a cycle in the rewriting graph RG(CW ) that is accessible from a task t 0 = λ(n 0 ) appearing in W 0 . Hence, there is an infinite run ρ ∞ = C 0 a1 -→ C 1 r1 -→ C 2 . . . of CW which moves are only user assignments (a move) to a node of the current workflow at configuration C i followed by a rewriting (r moves) that creates new instances of tasks, such that the sequence of rewritten task follows the same order as in the cycle of RG(CW ). Similarly, if CW terminates, then all runs are finite, and infinite runs of the form ρ ∞ cannot exist.

If CW can reach a deadlocked configuration, then by definition, it does not terminate. If all runs of CW terminate, then from any configuration, there is a way to reach a final configuration, and hence no deadlock is reachable.

Condition i) can be easily verified, by checking existence As soon as the symbolic execution tree is finite, checking condition ii) is a simple exploration of symbolic configurations to find deadlocks. Checking condition iii) is more involved, as it requires assumptions on data. Let C S i be a reachable symbolic configuration, and let n j be a node that is attached a split task in W i . We want to check if there exists an actual run Π = C 0 . . . C i with signature C 0 . . . C i such that one of the input datasets D k in sequence Dass i (n j ) is empty. Let rs j = (rn k , A k ) be the relational schema of D k , with A j = {a 1 , . . . , a |Aj | }. Then, emptiness of D k can be encoded as a FO formula of the form ψ i ::= x 1 , . . . x |Aj | , rn k (x 1 , . . . x |Aj | ) ∈ D k . For ψ i to hold in configuration C i , inputs of minimal nodes in W i-1 may have to satisfy some constraint ψ i-1 . Depending on the nature of the move from C i-1 to C i , the preconditions on inputs at step i -1 differ. Let m i denote the nature of move from C i-1 to C i . We denote by wp[m i ]ψ i the weakest precondition needed on inputs of minimal nodes in C S i-1 such that ψ i holds on C S i . We can show (Proposition ??) that all needed constraints can be encoded as first order formulas, and that all preconditions, regardless of the type of move, can be effectively computed. Now, to check that a symbolic run with signature ρ S = C S 0 . . . C S i violates condition iii), we need to compute inductively all preconditions needed to reach a configuration where this split operation fails. We start from the assumption that some input D k is empty when trying to execute the split in C i , and compute backwards the conditions ψ j = wp[m j+1 ]ψ j+1 needed at each step j ∈ i-1 . . . 1 to eventually reach a situation where D k = ∅ at step i. If any condition computed this way (say at step j < i) is unsatisfiable, then there is no actual run with signature ρ S such that D k is an empty dataset. If one end weakest precondition calculus on configuration C S 0 with a condition ψ 0 that is satisfiable, and satisfied by D in , then such a run exists. We have proved in Proposition 4 that one can effectively compute the weakest precondition of an FO property, and furthermore that the universal, existential, BSR, and separated fragment of FO were closed under weakest precondition calculus. Now, emptiness of a dataset D k with relational schema rs k = (rn k , A k ) can be encoded with the separated formula φ

∅ D k ::= x 1 , . . . x |A k | , rn k (x 1 , . . . x |A k | ) ∈ D k .
This means that condition iii) in Proposition 7 can be effectively checked. Then proof of Proposition 3 immediately gives a non-deterministic algorithm to check existence of a deadlock during an execution of a workflow.

Theorem 2. Let CW be a complex workflow, D in be an input dataset, and D in be an FO formula. Universal termination of CW on input D in is in co-2EXP T IM E. Universal termination of CW on inputs that satisfy D in is:

-undecidable in general -in co -2EXP T IM E if D in is in the universal fragment of FO, or in the BSR fragment of FO, -n in -fold exponential in the size of D in if D in is in the separated fragment.

Proof (sketch).

Complex workflows terminate iff they have bounded recursive schemes, and if they do not deadlock. Condition i) can be verified in O(|T cx | 2 ) (see proposition 5).

If CW is recursion free, then condition ii) can be verified non-deterministically by guessing a symbolic execution C S 0 . . . C S k of length at most 3.K Tcx . If this execution deadlocks, then there is an execution of CW that does not terminate, and we can safely conclude that CW does not terminate universally (for any input). Absence of deadlocks can hence be checked in EXP T IM E.

If this execution contains a potential deadlock at symbolic configuration C S i , then C i is a configuration from which a particular dataset D must be split and must be empty to cause a deadlock. Before concluding that C S i can be a real deadlock, one has to check whether that there exists an actual real execution C 0 . . . C i such that property D = ∅ holds at C i . We can show that the precondition ψ i-1 that needs to hold at C i-1 in order to obtain an empty dataset D at step C i are either of the form D = ∅ for some D (this is the case if the move from C i-1 to C i just adds a field to D to obtain D) of a FO formula in the universal fragment. Then one can repeat the following steps at each step k ∈ i -1, i -2, . . . up to C S 0 :

compute ψ k = wp[m k ]ψ k+1 . We know that this weakest precondition can be computed, and that ψ k is still an universal formula of size in O(r.|ψ k+1 |) (see proposition 1). -Check satisfiability of ψ k . If the answer is false, then Fail: one cannot satisfy the conditions required to have D = ∅ at step i, and hence there is no execution with signature C S 0 . . . C S i that deadlocks at C i , the randomly chosen execution is not a witness for deadlock. If the answer is true, continue If the algorithm does not stop before step k = 0, then the iteration computes a satisfiable formula ψ 0 of size in O(r i ). It remain to show that inputs of the complex workflow meet the conditions in ψ 0 .

Let us assume that the universal termination question is considered for a single input dataset D in , one Conversely, if the universal termination question is considered for a several input datasets described with a FO formula D in , one has to check that no contradiction arises when requiring existence of an input D in that satisfies both D in and ψ 0 . This can be done by checking the conjunction D in ∧ ψ 0 . Now, the formula is of size |D in | + |ψ 0 |, and more importantly falls in the class of D in . Hence, this last step is a combination of an NP-problem over a formula of size in O(r i ), and of a satisfiability problem which complexity is in O(2 |Din| ) for universal FO formula, doubly exponential in |D in | for BSR. Letting n in denote the number of variables in D in , the complexity of the last step is n in -fold exponential in the size of D in for separated formulas. As for the unique input case, if the answer is true, then C S 0 . . . C S i witnesses existence of a non-terminating execution.

has to check that D in |= ψ 0 . As ψ 0 is in universal i.e.
Hence, one can witness existence of a non-terminating run in O(K Tcx .2 r K Tcx + C in ) where C in is the cost required to check satisfiability of the constraint on inputs, that is in co -2EXP T IM E (in K Tcx ) if D in in the universal fragment, or in the BSR fragment ( the complexity of checking ψ i . . . ψ 0 and D in is in 2 -EXP T IM E ), and co -n -f oldEXP T IM E for the BSR fragment.

Last if D in is specified in an undecidable fragment of F O, then one cannot conclude whether there exists a legal input that satisfies D in and ψ 0 .

One can notice that the algorithms to check universal termination of CWs are non-deterministic, and that in the worst case, one may have to explore all symbolic executions of size at most 3•K Tcx . All these executions can be grouped in a common structure, i.e. a symbolic execution tree representing possible sequences of moves starting from the initial configuration. Definition 14 (Symbolic Execution Tree). The Symbolic execution tree (SET for short) of a complex workflow CW = (W 0 , T , T cs , U, sk, P) is a pair B = (V, E), where E ⊆ V × V is a set of edges, V is a set of symbolic configurations of the form C S i = (W i , Ass i , Dass S ), where W i = (N i , -→ i , λ i ) and Ass i : N i → U are the usual workflow and worker assignment relations, and Dass S associates a sequence of relational schemas to minimal nodes of

W i . (C S i , C S j ) ∈ E if C S j ∈ SC(C S i ).
Each path of the tree defines a symbolic execution. The symbolic execution tree of a complex workflow is a priori an infinite structure, but for recursion free CWs, the tree is of bounded depth, and bounded degree. One can hence perform an exhaustive search for deadlocks and potential deadlocks in the symbolic execution tree of recursion free workflow to exhibit a witness for non-termination. Let C S i = (W i , Ass i , Dass i ) be a potential deadlock symbolic configuration. Let S = {n 1 , . . . , n k } ⊆ min(W i ) be the set of minimal nodes that represent data splitting, i.e. that are assigned to a worker and have several successors in W i . Let Π = C S 0 . . . C S i be the path from the root of the tree to a potential deadlock C S i . Even if vertex C S i has a successor C S k , obtained by executing a task attached to some node n j ∈ S), it can be the case that Dass i assigns an empty input to n j in an actual run of CW with signature Π. Hence, some of the tasks execution moves depicted in B may not be realizable. If executing task λ(n j ) is the only possible action from C S i and if a run with signature Π ends in a configuration where Dass i (n j ) is of the form D 1 . . . . ∅ . . . D q then the run is deadlocked. However, if all runs with signature Π end with data assignments that affect non-empty sequences of datasets to all nodes of S, then C S i will never cause a real deadlock. Note also that when C S i is a potential deadlock, there exists necessarily a path C S i .C S i+1 . . . C S i+h in B where the only actions allowed from C S i+h is the execution of the incriminated minimal tasks that needs non-empty inputs. First of all, assume that a path in B exists from C S 0 to some vertex C S k where a dataset D k has to be split. As explained in the proof of Theorem 2, the property that D k = ∅ is expressible in the universal fragment of FO, so one can check satisfiability of a sequence of weakest preconditions up to ψ 0 for every potential deadlock vertex in the tree. If none of the potential deadlocks allows to prove existence of a run leading to a configuration where an empty dataset has to be split, then in all executions, split actions can occur safely and never deadlock a run. Then, as all other operation have no precondition on the contents of datasets, if a path C S 0 . . . C S dead to a deadlock vertex C S dead exists after verifying that potential deadlocks

Algorithm 1: Universal Termination Decision

Data: A complex workflow CW = (W0, T , Tcs, U, sk, P) are harmless, then a run with signature C S 0 . . . C dead exists (for any input dataset). Algorithm 1 shows how to decide universal termination for a particular input D in . This algorithm can be easily adapted to address termination for a set of inputs D in .

Result: A verdict ∈ {T ERM, N O -T ERM } 1 If CW has unbounded recursion Return NO-TERM 2 Build the symbolic execution tree B = (V, E) of CW 3 V split = {(W, Ass, Dass S ) ∈ V | W has splittable nodes} 4 for v ∈ V split do 5 ρv = C0 a 0 -→ C1 . . . a k-1 -→ C k = v //path from v0 to v 6 for n ∈ split nodes of min(Wi) do 7 W P ::= wp[a k-1 ]( D k ∈Dass S (n) D k = ∅) 8 for i = k -1..1

Termination with a guaranteed bound

Undecidability of existential termination has several consequences: As complex workflows are Turing complete, automatic verification of properties such as reachability, coverability, boundedness of datasets, or more involved properties written in a dedicated logic such as LTL FO [START_REF] Damaggio | Artifact systems with data dependencies and arithmetic[END_REF] (a logic that address both properties of data and runs) are also undecidable. However, one can notice that in the counter machine encoding in the proof of Theorem 1, instructions execution, require refinements, recursive schemes and split nodes (in particular to encode zero tests). So, infinite runs of a counter machine can be encoded only if rule 4 can be applied an infinite number of times. Obviously, recursion-free CWs cannot encode counter machines, and have a bounded number of signatures, as their runs are of length at most 3.K Tcx . This immediately gives us the following corollary: Corollary 2. Let CW be a recursion-free complex workflow, which runs length is bounded by 3.K Tcx . Let D in be a dataset, and D in an FO formula. One can decide in 2 -EXP T IM E (in K Tcx ) whether CW terminates existentially on input D in . If D in is in the existential, universal or BSR fragment of FO, then existential termination of CW is also in 2EXP T IM E. As it is sufficient to exhibit non-deterministically terminating run of size at most 3.K Tcx .

Proof. The proof follows the same line as for Theorem 2: one has to find non-deterministically a signature of size at most 3.K Tcx . When such a signature ρ S is found it remains to compute |ρ S | weakest preconditions ψ |ρ S | , . . . ψ 0 , imposing at each step that inputs of automated or split tasks are not empty. After this verification, it remains to show that inputs satisfy ψ 0 . Existential termination is hence decidable for recursion-free CWs, provided the description of inputs belongs to a decidable fragment of FO. One can notice that the decision procedure is doubly exponential in the length of runs (that is in K Tcx ). This bound can itself be exponential (see proof of prop. 4), but in practice, one can expect refinements to stop only in a few steps, as refinements are supposed to transform a complex task into an orchestration of simpler subtasks). With this assumption, K Tcx remains a simple polynomial in the number of complex tasks. Another way to bound recursiveness in a complex workflow is to limit the number of refinements that can occur during an execution. We can slightly adapt the semantics of Section 4, and in particular rule R 4 , and replace it by a restrictive decomposition (RD) rule. Intuitively, the (RD) rule refines a task as in rule R 4 , but forbids decomposing the same task an unbounded number of times. Rule 4' (Restricted task refinement): Let T = {t int , t 2 , ..., t f } be a set of tasks of size n. Let KD = (k 1 , k 2 , ..., k n ) ∈ N n be a vector constraining the number of refinements of task t i that can occur in a run ρ. In the context of crowdsourcing, this seems a reasonable restriction. Restrictive decomposition RD is an adaptation of rule R4 that fixes an upper bound k i on the number of decomposition operations that can be applied for each task t i in a run. We augment configurations with a vector S ∈ N n , such that S[i] memorizes the number of decompositions of task t i that have occurred. Rules 1-3 leave counter values unchanged, and rule 4 becomes:

∃n ∈ min(W ), ∃u = Ass(n), t i = λ(n) ∈ T cx ∧ S[i] ≤ k i ∧∃W s = (N s , -→ s , λ s ) ∈ P rof ile(t i , u) ∧Ass = Ass \ {(n, Ass(n))} ∧ Dass (min(W s )) = Dass(n) ∧∀x ∈ N s \ min(W s ), Dass (x) = ∅ |P red(x)| ∧W = W [n/Ws] ∀j ∈ 1 . . . |T |, S [j] = S[j] + 1 if j = i, S[j] otherwise (W, Ass, Dass, S) split(ti)
-----→ (W , Ass , Dass, S ) [START_REF] Bernays | Zum entscheidungsproblem der mathematischen logik[END_REF] Following the RD semantics, each task t i can be decomposed at most k i times. To simplify notations, we choose a uniform bound k ∈ N for all tasks, i.e. ∀i ∈ 1..n, k i = k. However, all results established below extend to a non-uniform setting. We next show decidability of existential termination under the RD semantics. First, we give an upper bound on the length of runs under RD semantics. Let k be a uniform bound on the number of decompositions, CW = (W 0 , T , T cs , U, sk, P) be a complex workflow with a set of tasks of size n, and C 0 = (W, Ass 0 , Dass 0 ) be its initial configuration. Proposition 8. Let ρ = C 0 . . . C q be a run of a complex workflow under RD semantics allowing at most k refinements of each task. The length of ρ is bounded by

L(n, k) = 3 • k • n 2 + 3 • |W 0 | Proof (Sketch).
Configurations can only grow up to a size smaller than C(n, k) = k.n 2 + |W 0 | via rule R4, and rules R1-R3 can be applied only a finite number of times from each configuration.

Under RD semantics, a symbolic execution tree B is necessarily finite and of bounded depth. A run terminates iff it goes from the initial configuration to a final one. If such run exists, then there exists a path in B from the initial vertex to a final vertex with signature Π = V 0 . . . V n . Further, if this path visits a potential deadlock and executes a splitting task λ(n) for some split node n j , then every dataset used as input of n j must be non-empty. To show that this path is realizable, it suffices to show existence of a run with signature Π that ends in a configuration C n satisfying property φ ::= true. Proposition 3 shows how to compute backwards the weakest preconditions demonstrating existence of such run of CW . An immediate consequence is that existential termination of complex workflows is decidable under restricted decomposition semantics, with the same complexity as for recursion-free specifications. Theorem 3. Let CW be a complex workflow with restricted decomposition semantics. Then:

-Existential termination of CW for a single input D in or for a set of inputs D in described with the universal, existential, or BSR fragment of F O is in 2EXPTIME. -Universal termination of CW for a single input D in or for a set of inputs D in described with the universal, existential, or BSR fragment of F O is in co -2EXP T IM E.

Proof. Under restricted decomposition semantics, the length of a run is bounded by 3

• k • T 2 cx + 3 • |W 0 |.
We can reuse the techniques of Theorem 2 to find a witness symbolic run that is the signature of a run that does not terminate, and of corollary 2 to find a witness symbolic run that is the signature of a run that terminates.

Proper Termination

Complex workflows provide a service to a client, that inputs some data (a dataset D in ) to a complex task, and expects some answer, returned as a dataset D out . We assume the client sees the crowdsourcing platform as a black box, and simply asks for the realization of a complex tasks that need specific competences. However, the client may have requirements on the type of output returned for a particular input. We express this constraint with a First Order formula ψ in,out relating inputs and outputs, and extend the notions of existential and universal termination to capture the fact that a complex workflow implements client's needs if some/all runs terminate, and in addition fulfill requirements. This is captured by the notion of proper termination.

Definition 15. A constraint on inputs and outputs is an FO formula ψ in,out ::

= ψ in,out E ∧ ψ in,out A ∧ ψ in,out

AE

, where ψ in,out E is a conjunction of existential formulas addressing the contents of the input/output dataset, i.e. constraints of the from ∃x, y, z, rn(x, y, z) ∈ D in ∧ P (x, y, z), ψ in,out A is a conjunction of universal formulas constraining all tuples of the input/output dataset, of the form ∀x, y, z, rn(x, y, z) ∈ D in ⇒ P (x, y, z) where P is a predicate on values of x, y, z.

ψ in,out AE is a conjunction of formulas relating the contents of inputs and outputs, of the form ∀x, y, z, rn(x, y, z) ∈ D in ⇒ ∃(u, v, t), φ(x, y, z, u, v, t) Definition 16 (Proper termination). Let CW be a complex workflow, D in be a set of input datasets, and ψ in,out be a constraint given by a client. A run in Runs(CW, D in ) terminates properly if it ends in a final configuration and returns a dataset D out such that D in , D out |= ψ in,out . CW terminates properly existentially with inputs D in iff there exists a run Runs(CW, D in ) for some D in ∈ D in that terminates properly. CW terminates properly universally with inputs D in iff all runs in Runs(CW, D in ) terminate properly for every D in ∈ D in Proper termination considers correctness of the computed outputs in addition to termination of runs. In general, termination of a run does not guarantee its proper termination. A terminated run starting from an input dataset D in may return a dataset D out such that pair D in , D out does not comply with constraints ψ in,out imposed by the client. For instance, a run may terminate with an empty dataset while the client asked for an output with at least one answer. Similarly, a client may ask all records in the input dataset to appear with an additional tag in the output. If any input record is missing, the output will be considered as incorrect. Obviously, a CW that does not terminate cannot terminate properly, and setting ψ in,out ::= true recasts the proper termination question into Proper termination can be immediately brought back to a termination question, by setting ψ in,out = true. We hence have the following corollary.

Corollary 3. Existential proper termination of a complex workflow is undecidable.

In this section, we show that proper termination can be handled through symbolic manipulation of datasets, that give constraints on the range of possible values of record fields, and on the cardinality of datasets. We handle execution symbolically, i.e. we associate a symbolic data description to inputs of every node which task is executed, and propagate the constraints on this data to the output(s) produced by the execution of the task. As for termination, weakest preconditions can be built. However, universal termination is decidable only with some restrictions on the fragment of FO used to constrain relation between inputs and outputs. Theorem 4. Let CW be a complex workflow, and ψ in,out be a constraint. Then:

existential and universal proper termination of CW are undecidable, even under RD semantics.

if ψ in,out is in a decidable fragment of FO, then -existential proper termination is decidable under RD semantics -universal proper termination is decidable.

Proof. Let us first prove the undecidability part: It is well known that satisfiability of F O is undecidable in general, and in particular for the AE fragment with formulas of the form

∀ → X∃ → Y , φ(X, Y ). Hence ψ in,out
AE can be a formula which satisfiability is not decidable. One can take an example of formula ψ unsat which satisfiability is not decidable. One can also build a formula ψ id that says that the input and output of a workflow are the same. One can design a workflow CW id with a single final node which role is to return the input data, and set as client constraint ψ in,out = ψ unsat ∧ ψ id . This workflow has a single run, both under standard and RD semantics. Then, CW id terminates properly iff there exists a dataset D in such that D in |= ψ unsat , i.e. if ψ unsat is satisfiable. Universal and existential proper termination are hence undecidable problems.

For the decidable cases, one can apply the technique of Theorem 2. One can find non-determinisitically a run ρ S that does not terminate and check that it is feasible, or a run ρ S that terminates and check whether it satisfies ψ in,out .

Let us first consider universal termination. For this, one can compute a chain of weakest preconditions ψ n , ψ n-1 , . . . ψ 0 that have to be enforced to execute successfully CW and terminate in node n. In particular, ψ n ::= true. Similarly, one can compute at each step, a weakest precondition ψ in,out i needed at step i so that ψ in,out holds. If at one stage, ψ i or ψ in,out i is not satisfiable, then ρ S is not the signature of an actual run of CW that terminates properly, and we have found a witness of non-proper termination. We have assumed that ψ in,out was specified in a decidable fragment of F O. As computing the weakest precondition of a property in the existential, universal, BSR, SF fragment of FO gives a property in the same fragment, all ψ i 's and ψ in,out i 's are in a decidable fragment of FO. Then, the complexity will depend on the considered fragment, and on the fragment of FO used to specify inputs. As for universal termination, if inputs and ψ in,out are specified with the universal and existential fragments, then universal proper termination is in co -2EXP T IM E. If ψ in,out is in SF, then checking proper universal termination is co -K -f old-exponential time, where

K = r K Tcx .
Then, one has to check satisfiability of ψ proper,n ::= ψ i ∧ ψ in,out . So, if ψ in,out is written in a decidable fragment, then so is ψ proper,n . Hence, existential proper termination is decidable for complex workflows executed under restricted decomposition if ψ in,out is expressed in a decidable fragment of FO.

The prooof and complexities for existential termination follow the same lines, yielding 2EXP T IM E complexity when ψ in,out is written with the existential, universal, fragments of FO, 3 -EXP T IM E complexity for when ψ in,out is written in the BSR fragment (as checking a BSR formula in in NEXPTIME []) and K -f old-exponential for SF formulas.

At first sight, restricting to the existential, universal, BSR, or SF fragments of FO can be seen as a limitation. However, the existential fragment of FO is already a very useful logic, that can express non-emptiness of outputs: property ∃x 1 , . . . , ∃x k , rn(x 1 , . . . x k ) ∈ D out expresses the fact that the output should contain at least one record. Similarly, one can express properties to impose that every input has been processed. For instance, the property ψ valid in,out ::= ∀x 1 . . . x k , rn(x 1 , . . . x k ) ∈ D in =⇒ ∃y 1 . . . y q , rn(x 1 , . . . x k , y 1 , . . . y q ) ∈ D out Formula ψ valid in,out asks that every input in D in is kept and augmented by additional information. This formula can be rewritten into another formula with a single alternation of quantifiers of the form ∀x 1 . . . x k , ∃y 1 . . . y q , ¬rn(x 1 , . . . x k ) ∈ D in ∨ rn(x 1 . . . x k , y 1 . . . y q ) ∈ D out This latter formula is in BSR form.

Last, one can also consider formulas in which ψ in,out EA is of the form ∀x 1 , . . . x k ∃y 1 , . . . , y q φ as soon as every atom in φ that is not separated contains only existential variables that take values from a finite domain. Then ψ in,out AE can be transformed into an equivalent universal formula which matrix is a boolean expression on separated atoms

Conclusion

We have proposed data centric workflows for crowdsourcing applications. The model includes a higherorder operation, that allows splitting of tasks and datasets to decompose a workflow into orchestration of simple basic tasks. This gives complex workflows a huge expressive power. On this model, universal termination is decidable. If requirements on inputs and outputs are expressed with separated FO, universal proper termination is decidable too. Existential termination is not decidable in general. With the reasonable assumption that tasks cannot be decomposed an arbitrary number of times, existential termination and existential proper termination (with separated FO requirements) are decidable.

Several questions remain open: satisfiability of separated FO is n-fold exponential [START_REF] Sturm | Deciding first-order satisfiability when universal and existential variables are separated[END_REF], which makes the SF fragment a priori unusable. However, preconditions used in the termination decision procedures are all existential or universal formulas, and SF formulas only originate from input descriptions. Hence, the complexity of termination should be in 2EXP T IM E for most cases. One can should also consider that the length of runs to consider is a priori exponential, but that a reasonable crowdsourcing platform will probably not give too much refinement power to its workers. We can hence expect K Tcx to be rather small. So far, we do not know whether the complexity bounds are sharp. Beyond complexity issues, complex workflows raise other problems such as synthesis of appropriate pricing (find incentives that maximize the probability of termination), or synthesis of schedulers to guarantee termination with appropriate user assignment. Other research directions deals with the representation and management of imprecision. So far, there is no measure of trust nor plausibility on values input by workers during a complex workflow execution. Equipping domains with such measures is a way to provide control techniques targeting improvement of trust in answers returned by a complex workflow, and tradeofs between performance and accuracy of answers... dataset on records with cname = C x or cname = ⊥, and forwards the obtained dataset to node n Cx∪⊥ q . On the other hand, it creates a copy of the input dataset and forwards it to node n id q . The role of task t Cx∪⊥ q is to perform a boolean query that returns {true} if the dataset contains a record R(k, C x ) and {f alse} otherwise, and forwards the result to node n btest q . Task t btest q selects records with value {f alse} (it hence returns an empty dataset as the result of the boolean test was {true}). Task t id q forwards its input to node n done q . Task t done q received input datasets from n btest q and n id q and forwards the input from n id q to node n q . One can immediately see that if the dataset input to n div q contains an occurrence of C x then one of the inputs to n done q is empty and hence the workflow deadlocks. Conversely, if this input contains no occurrence of C x , then this workflows reached a configuration with a single node n q labeled by task t q , and with the same input dataset as n q .

One can see that for every run ρ = C 0 . . . C k of the two counter machine, here C k = (q, v 1 , v 2 ) there exists a single non-deadlocked run, and that this run terminates of configuration (W, ass, Dass) where W consists of a single node n q labeled by task t q , and such that Dass(n q ) contains v 1 occurrences of records of the form R(k, C 1 ) and v 2 occurrences of records of the form R(k, C 2 ). Hence, a two counter machine terminates in a configuration (q f , v 1 , v 2 ) iff the only non-deadlocked run of the complex workflow that encodes the two counter machine reaches a final configuration.

n div q t div q n Cx q t Cx q n Cx∪⊥ q t Cx∪⊥ q n ⊗ q t ⊗ q n dec q t dec q n q t q Wq,NZ Wq,Z n div q t div q n Cx∪⊥ q t Cx∪⊥ q n id q t id q n btest q t btest q
n done q t done q n q t q Fig. 9. Encoding of Non-zero test followed by decrement (left), and Zero Test followed by state change (right).

A.2 Proof of Proposition 7

Lemma 1. Let B be a tree with a potential deadlock V i with successors v i,1 , . . . v i,k corresponding respectively to splitting of nodes n 1 , . . . n k in the workflow part of node V i . Then a run Π with signature V 0 . . . V i such that D k = ∅ for some D k ∈ Dass(n j ) does not terminate.

Proof. If a node n j in a configuration C i is labeled by a complex task and is already assigned a competent user, then assignment of this node and input data will not change in any successor during execution. So, if this node cannot split and distribute data due to the fact that D k = ∅, it will never be able to split this data later in an execution that starts with prefix that has signature Π.

This lemma has useful consequences: for a potential deadlock, it is sufficient to detect that one input dataset D nj for a split node is empty to claim that there exists an execution with a signature that has V 0 . . . V i as prefix, and that deadlocks. Proposition 7: A complex workflow terminates universally iff the following conditions hold: i) Its symbolic execution tree is finite (there is no unbounded recursion) ii) There exists no path V 0 . . . V i in the symbolic execution tree such that V i is a deadlock iii) there exists no run with signature V 0 . . . V i where V i is a potential deadlock, with D k = ∅ for some D k ∈ Dass(n j ) and for some minimal split node n j of W i .

Proof. First, notice that all runs of a complex workflow have their signature in the Symbolic execution tree, as application of a rule never considers data contents, but only the structure of a workflow. Hence, even when some execution of a splitting task could be prevented by empty inputs, the symbolic execution tree contains edges symbolizing the effects of this splitting action on the workflow. If all runs of a complex workflow CW terminate, then CW has no infinite run and no deadlocked run. As a consequence, its symbolic execution tree is finite, and contains no deadlock nodes. As executions of CW never meets deadlocks, one cannot find a run with signature V 0 . . . V i where V i = (W i , Ass i , Dass S i ) and is such that W i has a minimal split node with an empty input dataset. Hence conditions i), ii), iii) are met.

Let us now assume that CW does not terminate. It means that this complex workflow either allows unbounded runs, or reaches deadlocks. If CW has an unbounded run ρ ω , then the workflow allows an unbounded recursive schemes, i.e. situations where successive refinement of a node n labeled by a task t leads to replace n by a subgraph that still contains a node n with task t. Further, as ρ ω is an effective execution of CW , every rule applied in the execution of this run also applies during the construction of a symbolic execution tree, and hence this tree contains an infinite path (which violates condition i). If an execution of CW ends in a deadlocked configuration, then it means that either no rule applies from this configuration, or that the only next possible action is the execution of a split node that cannot be performed due to an empty input dataset. As nodes of the symbolic execution tree only differ from real configurations with their data, the first case means that the symbolic execution tree also contains a deadlock node from which no semantic rule applies (hence violating condition ii). For the second case, the deadlocked run ends in a configuration C i . It has a signature V 0 . . . V i , and there exists a input dataset D = ∅ that prevents a minimal node from being executed (hence violating condition iii).

A.3 Proof of Theorem 2

Theorem 2 : Universal termination of a complex workflow is a decidable problem.

Proof. First we can show that complex workflows terminate only if they have bounded recursive schemes, and do not deadlock. Let us assume that a complex workflow has unbounded recursive schemes, and that none of the task executions or refinement is ever deadlocked. Then, there exists a task t and an infinite run ρ = ρ 1 .ρ 2 . . . such that every ρ i terminates with a refinement of task t. Under the assumption that the system does not deadlock during this infinite runs, such an infinite recursive scheme occurs only if t can be rewritten through successive refinement steps into a workflow that contains a new occurrence of task t. This can be checked from the list of tasks and profiles. We build a graph RG = (T , -→ T , T 0 ) where T 0 is the set of tasks that appear in W 0 , (t, t ) ∈-→ T iff there exists a worker u, a workflow W t = (N t , -→ t , λ t ) in P(t, u) and a node n ∈ N t such that λ(n) = t . An edge (t, t ) means that one can rewrite t into a workflow that contains t . If RG contains a cycle that is accessible from T 0 , then the complex workflow contains a recursive scheme. If an infinite runs containing an infinite number of rewritings does not deadlock, then the workflow does not terminate. If all runs that unfold such a recursive scheme deadlock at some point, then the complex workflow does not terminate either. It remains to consider the case of complex workflows without unbounded recursive schemes. The executions of such workflows are of bounded length, and the complex workflow terminates (universally) iff all of them terminate.

Complex workflows terminate only if they have bounded recursive schemes, and if they do not deadlock. The former can be checked by considering how tasks are rewritten. If there is no unbounded recursive scheme allowed by CW , then its symbolic execution tree is finite. Then, we can detect deadlocks and potential deadlocks in this tree. If a deadlock exists, then the complex workflow does not terminate universally. Potential deadlocks occur only if a vertex V i in the tree allows a move that is a split of a dataset D. Now, emptiness of a dataset D with signature rn = (rn, A) with A = (a 1 , . . . a k ) can be encoded with the separated formula of the form x 1 , . . . x k , rn(x 1 , . . . x k ) ∈ D. Hence, using Proposition 3, one can decide whether a run starting with input data D in (or from some input data in D in ) which signature is the path leading to V i such that D = ∅ exists. This completes the proof of Theorem 2.

A.4 Proof of Proposition 8 Proposition 9. Let ρ = C 0 .C 1 . . . C q be a run under RD semantics. Then, for every C i = (W i , Ass i , Dass i ), the number of nodes in W i is smaller than C(n, k) = k.n 2 + |W 0 |.

Proof. Each decomposition of a task t i replaces a single node n by a new workflow with at most d i = max u∈U max{|W j | | W j ∈ P rof ile(t i , u)} nodes. Recall that decomposition profiles are known, and that all nodes of workflows in profiles are attached distinct task names. So, we have d i < n. Every run ρ starting from C 0 is a sequence of rule applications. Rule 1 does not affect the size of workflows in configurations, and rules 2 and 3 remove at most one node from the current workflow when applied. For each task t i , a run ρ contains at most k occurrence of rule 4 refining a task of type t i . Application of rule 4 to task t i adds at most d i nodes to the current workflow, and removes the refined node. All other rules decrease the number of nodes. One can notice that as each task can be decomposed at most k times, rule 4 can be applied at most k.n times in a run following the RD semantics, even if this run is of length greater than k.n. Let S 0 = |W 0 |, S 1 = S 0 + n -1, and S i+1 = S i + (n -1). For a fixed n and a fixed k, the maximal size of the workflow component W i in every configuration C i of a run under RD semantics is smaller than

S k.n = |W 0 | + (k.n)(n -1) = |W 0 | + k • n 2 -k • n.
Proposition 8: Let ρ = C 0 . . . C k be a run of a complex workflow under RD semantics. The length of ρ is bounded by

L(n, k) = 3 • k • n 2 + 3 • |W 0 | Proof.
Recall that a configuration is a triple C i = (W i , Ass i , Dass i ), with Ass(n) = u i . Each configuration is a "global state" of the execution of a complex workflow. W i represents the work that needs to be done before completion, Ass the users assignment, and Dass the data assignment. Recall that a configuration with a single node is necessarily a final configuration with a node n f which task is to return all computed values during the execution of the complex workflow.

The only way to change user or data assignment part of configurations is to execute the task attached to a node (i.e., apply rule R2 or R3) or refine a node (i.e. apply rule 4). Starting from a configuration C i , the maximal number of user assignment that can be performed is |W i |, and along the whole run, as each node can be assigned an user at most once, the maximal number of applications of rule R1 is C(n, k).

The length of a run ρ is |ρ| = |ρ| 1 +|ρ| 2 +|ρ| 3 +|ρ| 4 where |ρ| i denotes the number of applications of rule R i . Now, |ρ| 1 ≤ C(n, k). Similarly, |ρ| 1 = |ρ| 2 +|ρ| 4 . Last, rule R3 can be applied only a number of times bounded by the maximum number of created nodes, i.e, [START_REF] Bernays | Zum entscheidungsproblem der mathematischen logik[END_REF] Proof of Proposition ?? Proposition ??: Let ψ i be an FO formula. Then, for any move m i from C i-1 to C i and any formula ψ i , ψ i-1 = wp[m i ]ψ i is an effectively computable FO Formula. Further, if ψ i is in separated form, then ψ i-1 is also in separated form.

|ρ| 3 ≤ C(n, k). So overall, |ρ| = |ρ| 1 + (|ρ| 2 + |ρ| 4 ) + |ρ| 3 ≤ C(n, k) + C(n, k) + C(n, k). Hence, the length of ρ is bounded by L(n, k) = 3 • k • n 2 + 3 • |W 0 | A.
Proof. Each move m i in the execution tree represents a configuration change, and transforms input datasets D 1 , . . . D n into output datasets D 1 . . . D p . These transformations are projections, selections, joins, field addition update or enlargement, or a one to one automated linear transformation of records in a dataset. Slightly abusing the notation for FO used so far, we write D 1 , . . . D k |= ψ to denote that a set of datasets satisfies formula ψ. In the formula, given a relation rn(v 1 , . . . v m ) depicting a record in a dataset, we will also make clear in the formula which dataset contains the record, using a notation of the form rn(v 1 , . . . v m ) ∈ D i . Lemma 3 (Weakest precondition for R2R transformations). Let φ be a FO formula, and act be an atomic action that transforms each record in a dataset into another record. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formula, then ψ is also separated.

Proof. Record to Record Transformation(R2R) converts each record from an input dataset D i to a new record corresponding to output dataset D j by applying some linear transformation. Consider the dataset D j with relational schema rs j = (rn j , B). Let ψ post be an FO formula such that D 1 , . . . D j , . . . , D k |= ψ post , and where D j is obtained by R2R transformation of an input dataset D i with relational schema rs i (rn i , A). Let A = (a 1 , . . . , a p ) and B = (b 1 , . . . , b q ). An R2R transformation from rs i to rs j is a transformation, that associates to each records r 1 = (v 1 , . . . v p ) with relational schema rs i , where v k is the value of attribute a k , a record r 2 = (w 1 , . . . w q ) with relational schema rs 2 such that every w j is the value of attribute b j obtained as a combination of values v 1 , . . . v p . If v 1 , . . . v p are numerical values then each w j is a linear combination of the form

w j = k j,1 v 1 + k j,2 v 2 + k j,p v p + k j .
where k, k 1 , . . . , k p are constant values. This type of transformation allows to define mean values, sums of values in fields, etc.

Let ψ post constrain values of variables W = w 1 , . . . w h . Variables in W depict values of attributes b 1 , . . . , b q in records of D j (i.e. they appear in a subformula of the form rn j (w 1 , . . . w q )). Let Att(w i ) denote the attribute of variable w i . We assume that the variables used under the scope of two subformulas of the form rn 2 (w 1 , . . . w q ) and rn 2 (w 1 , . . . w q ) are disjoint, and that equality of values is achieved through side formulas of the form w i = w j . Note that even if transformation f is a record to record transformation, formula ψ post can address values of more that one record, i.e. be of the form ∃w 1 , . . . w q , w q+1 . . . w 2.q , rn j (w 1 , . . . w q ) ∧ rn j (w q+1 , . . . w 2.q ) ∧ . . . φ. However, every record rn j (w 1 , . . . w q ) is obtained as transformation of a record of the form rn i (v 1 , . . . v p ). Let K rnj be the number of subformulas of the form rn j (w i , . . . w x+q ) in ψ post . We denote by ψ post [B/R2R(A)] the formula ψ post where every instance of relational schema rs j i.e., an instance of the form rn i (w k.q+1 , . . . v k.(q+1) ) is replaced by an instance rn i (v k.p+1 , . . . v k.(p+1) ) of schema rs i , and every occurrence of a variable w i used in an instance of rs j and appearing outside a relation is replaced by the linear combination of values v j+1 . . . v j+p and constant k j (where j = i p ) allowing to obtain the value of variable w i . Hence, the weakest precondition for R2R transformation is a precondition on D 1 , . . . D i , . . . , D k , given as

wp[R2R]ψ post = ψ post [B/R2R(A)]
One can notice that wp[R2R]ψ post simply replaces atoms in a separated formula by other atoms, over new sets of variables. However, this transformation replaces a universally (resp. existentially) quantified block of variables by a new universally (resp. existentially) quantified block, which preserves vacuity of intersection of existential and universal variables. Hence, if ψ post is separated, then wp[R2R]ψ post is also separated. Lemma 4 (Weakest precondition for Selection of records). Let φ be a FO formula, and act be an atomic action that selects records that satisfy a predicate P from datasets. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ and P are separated FO formulas, then ψ is also separated.

Proof. Let D 1 , . . . D j , . . . D k |= ψ post , and let D j be a dataset with relational schema rs(rn, A) obtained by selection of records from an input dataset D i with relational schema rs(rn, A). One can notice that selection keeps the same relational schema, and in particular the same set of attributes A = (a 1 , . . . a k ). We will assume that selected records are records that satisfy some predicate P (v 1 , . . . v k ) that constrain the values of a record (but do not address properties of two or more records with relational schema rs). That is, the record selected from D i by P are records that satisfy

ψ sel = ∃v 1 , . . . v k , rn(v 1 , . . . v p ) ∧ P (v 1 , . . . , v k ).
Formula ψ post is a formula of the form Q(V ars(ψ post )), φ. It contains K rn subformulas of the form rn(w i , . . . w i+k ) or ¬rn(w i , . . . , w i+k ) and, as for R2R transformation, we assume without loss of generality that these subformulas are over disjoint sets of variables. Let φ rn,1 , . . . φ rn,Krn be the subformulas of φ addressing tuples with relational schemas in rs. For i ∈ 1..K rn , we let φ P rn,i denote the formula rn(w i , . . . w i+k ) ∧ P (w i , . . . w i+k ) if φ rn,i is in positive form and ¬(rn(w i , . . . w i+k ) ∧ P (w i , . . . w i+k )) otherwise. Last, let us denote by φ [{φrn,i}|{φ P rn,i }] the formula where every {φ rn,i } is replaced by {φ rn,i } P . The weakest precondition on D 1 , . . . D i , . . . , D k for a selection operation ψ post still holds. The weakest precondition hence includes the amount of imprecision on each variable in W imp , and can be modeled by adding variables X = {x 1 , . . . x Krn } with domain [-δ, +δ] to existentially quantified variables. Note that adding imprecision to an universally quantified variables v is not needed, as the considered properties should hold for all possible values of v in its domain. Considering an expression of the form expr ::= k 1 .w 1 + k 2 .w 2 . . . k p w p + k, the expression expr [ v j /v j + x j ] is obtained by replacing existentially quantified variable v j by (v j + x j ) in expr. For a subformula of the form φ = expr 1 expr 2 , where expr 1 contains a variable v j+n.p and expr 2 contains a variable v j+m.p , we denote by φ imp = expr 1 [v j+n.p /v j+n.p +x j+n.p ] expr 2 [v j+n.p /v j+n.p +x j+n.p ] the formula where each occurrence of imprecise variable v j+n.p is replaced by v j+n.p + x j+n.p . For a subformula of the from φ = rn(v 1 , . . . v j , . . . v k ) where v j is an existential variable corresponding to the enlarged field a j , φ imp = rn(v 1 , . . . v j + x j , . . . v k ). For formulas containing no existentially quantified enlarged variables, φ imp = φ. Last, for formulas that are boolean combinations of subformulas φ 1 , φ 2 , φ imp is the formula obtained as a boolean combination of φ imp 1 and φ imp As we need to introduce imprecision through new variables, we replace every statement of the form ∃w i , φ by a statement of the form ∃w i , ∃x i , φ, and letting Q(V )||X denote the prefix obtained by replacement of every substring ∃w i , by a string ∃w i , ∃x i in Q(V ) and expression using φ. We now define the weakest precondition for ψ post that has to be satisfied by D 1 , . . . D i , . . . D k when enlarging field a j as

wp[Enlargement δ ]ψ post = Q(V )||X, φ imp post
One can notice that if φ post is separated (resp. in BSR fragment of FO), then wp[Enlargement δ ]ψ post is also separated (resp. in BSR fragment).

Lemma 7 (Weakest precondition for unions of datasets). Let φ be a FO formula, and act be an atomic action that merges datasets with common relational schema. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formula, then ψ is also separated.

Proof. Union operations merge datasets that have same relational schema. It takes data from different input datasets D 1 , . . . D q with the same relational schema rs = (rn, A), where A = (a 1 , . . . , a p ) and produces an output dataset D a with relational schema rs.

Let us assume that D 1 , . . . D a , . . . D k |= ψ post . We want to compute the weakest preconditions on D 1 , . . . , D 1 , . . . D q , . . . D k . As usual, ψ post is an FO formula of the form Q(V ), φ post . Now, every relation rn(w i , w i+p ) ∈ D a mentioned in the formula has to appear in a dataset D i , i ∈ 1..q, that can be chosen when interpreting the formula. Similarly, if ψ post contains a statement of the form ¬rn(w i , w i+p ) ∈ D a , then rn(w i , w i+p ) should not appear in any dataset D i , i ∈ 1..q. Formula ψ post holds for dataset D a iff one can build a map af f : 1..KU → 1..q that associates to every occurrence of relation rn a dataset from which a record instantiating relation rn(w i , . . . w i+p ) originates. Let Assign(KU, q) denote the set of all possible assignments for the KU relations in ψ post . For a particular assignment af f ∈ Assign(KU, q) we can write a formula φ af f post where the m th occurrence of rn(w i , . . . , w i+p ) ∈ D a is replaced by rn(w i , . . . , w i+p ) ∈ D af f (m) , and every occurrence of ¬rn(w i , . . . , w i+p ) ∈ D a is replaced by the conjunction ¬rn(w i , . . . , w i+p )

∈ D i . D 1 , . . . D a , . . . D k |= ψ post iff one can find af f ∈ Assign(KU, k) such that D 1 , . . . , D 1 , . . . D q , . . . D k |= φ af f
post . Note that here, choices of records in different D j 's are not independent (for some contents of input datasets, affecting rn(w 1 , . . . w p ) to D 1 can impose to search a matching record for rn(w p+1 , w 2.p ) in another dataset).

Hence the weakest precondition on D 1 , . . . , D 1 , . . . D q , . . . D k such that ψ post hold on D 1 , . . . D a , . . . D k after merging D

1 , . . . D q is wp[U nion]ψ post = Q(V ), af f ∈Assign(KU,k) ψ af f post
As variables used in atoms of wp[U nion]ψ post do not change with respect to the original formula, if ψ post is separated, then all atoms in wp[U nion]ψ post also separated universally and existentially quantified variables.

Lemma 8 (Weakest precondition for joins). Let φ be a FO formula, and act be an atomic action that performs a join between two datasets over a common field. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ and P are separated FO formulas, then ψ is also separated.

Proof. Join operations merge datasets with different relational schemas. For simplicity, we consider that joins apply to a pair of input datasets D 1 , D 2 with respective relational schemas rs 1 = (rn1, A 1 ) and rs 2 = (rn 2 , A 2 ) to produce a output dataset D a with relational schema rs a = (rn a , B = A 1 ∪ A 2 ). We also assume that joins operate on equality of a single common field a i . Without loss of generality, letting A 1 = (a 1 , a p1 ) and A 2 = (a 1 , . . . a p2 , we consider that jointure on a common field is represented by a p1 in rs 1 and by a 1 in rs 2 . That is, if a pair of records r 1 = rn 1 (v 1 , . . . v p1 ) and r 2 = rn 2 (u 1 , . . . u p2 ) have common value on their common field, v n is the value of a i in r 1 and u m the value of a i in r 2 then D a will contain a record r = (v 1 , . . . v p , u 2 , . . . u p2 ). Hence, letting D a , D 3 , . . . D k be a set of datasets that satisfy a formula ψ post , the weakest precondition that has to be computed is a property of D 1 , D 2 , D 3 , . . . D k .

Formula ψ post is an FO formula over a set of variables V = W ∪ X, where W are variables involved in relational statements of the form in the form rn a (w i , . . . w i+p ) or ¬rn a (w 1 , . . . w p ). Hence ψ post is of the form Q(V ), φ post . Now, every positive statement of the from rn a (w i , w i+p1+p2-1 ) mentioned in the formula originates from a pair of records in D 1 , D 2 with common value on a i . Hence, every statement of the form rn a (w i , . . . w i+p1+p2-1 ) holds for D a iff the statements φ EQ,i = ∃x i , rn 1 (w i , . . . w i+p1-1 ) ∈ D 1 ∧ rn 2 (x i , w i+p1 . . . w i+p1+p2-1 ) ∈ D 2 ∧ w i+p1-1 = x i , where x i is a new variable that does not already appear in V ars(ψ post ) holds. Similarly, for relational statement in negative form ¬rn a (w i , . . . w i+p1+p2-1 ) holds for D a iff the statement φEQ,i = ∀x i , ¬(rn 1 (w i , . . . w i+p1-1 ) ∈ D 1 ∧ rn 2 (x i , w i+p1 . . . w i+p1+p2-1 ) ∈ D 2 ∧w i+p1-1 = x i ), where x i is a new variable that does not already appear in V ars(ψ post . Let ψ post [Da |D1,D2] be the formula obtained by replacing every statement of the form rn a (w i . . . ) by φ EQ,i , and every statement of the form ¬rn a (w i . . . ) by φEQ,i . As x i 's are fresh new variables, we can easily convert this formula into a prenex formula ψ prenex post [ Da|D1,D2] of the form Q(V ).∃x 1 , x k ∀x k+1 , . . . x k+m φ, where x 1 , . . . x k are fresh variables originating from positive relational statements and x k+1 , . . . x k+m originate from negative ones. Hence, the weakest precondition on D 1 , D 2 , D 3 , . . . for ψ post to hold after a join is:

wp[Join]ψ post = ψ prenex post [ Da|D1,D2]
One can immediately notice that if ψ post is separated, then wp[Join]ψ post is in separated form. As ψ post is separated, all atoms either address properties of existentially quantified x i 's or properties of universally quantified y i 's. Hence, replacing a statement of the form rn(x 1 , . . . x k ) on existential variables with a statement of the from rn(x 1 , . . . x q ) ∧ rn(x q+1 . . . x k ) ∧ x 1 = x q+1 in which all atoms address existentially quantified variables. For atoms with universally quantified variables, one can notice that ψ post can be rewritten into an equivalent BSR formula. Hence, a formula of the form ∃ → Z, ∀x, w, y rn(x, w, y) holds iff the precondition ∃ → Z, ∀x, w, y, rn 1 (x, w) ∧ rn 2 (w, y), which remains separated. Lemma 9 (Weakest precondition for record insertion). Let φ be a FO formula, and act be an atomic action that inserts a new record is a dataset. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, -if φ is a separated FO formulas, then ψ is also separated.

Proof. Record insertion consists in adding a record to an existing dataset. Let D j be a dataset with relational schema rs = (rn, A) with A = (a 1 , . . . a p ), and assume that D j is obtained after adding a record to an input dataset D i with the same relational schema. Let D 1 , . . . D j . . . D k |= ψ post . When a set of records R selected from D i 's serves as a witness for the truth of ψ post after an insertion, then at most one of these records or the form r = rn(v 1 , . . . , v p ) can be the newly inserted tuple. That is, D

1 , . . . D j . . . D k |= ψ post iff D 1 , . . . (D i {r}) . . . D k |= ψ post . It means that either D 1 , . . . D i . . . D k |= ψ post or D 1 , . . . D i . . . D k |= ψ post ∧ D 1 , . . . D i {r} . . . D k |= ψ post Let ψ post be of the form Q(V ), φ, with V = W ∪ Y ,
and W be the variables appearing in relational clauses of the from rn(w i , . . . w i+p ). Let us assume that φ is a quantifier free formula in disjunctive normal form. In other words, φ is of the from φ = k=1..K

φ k = at k,1 (V ) ∧ • • • ∧ at k,m k (V )
, where each at k,k (V ) is an atom involving a subset of variables in V . If Q(V ), φ k is separated, then one can compute an equivalent formula in BSR form of the form ∃

-→ V 1 , ∀ -→ V 2 φ k .
This formula is satisfied if one can find an assignment of variables in V 1 such that for every assignment of variables in V 2 , φ k evaluates to true when replacing variables by their value. All existential variables are separated. For existential variables under the scope of a relational statement rn(w i , . . . w i+p ). Let AK be the number of relational statements of the form rn(..) ∈ D j . One can hence choose, for each statement rn(w i , . . . w i+p ) whether variables w i , . . . w i+p are assigned values freshly introduced by the newly created record or not. In the first case, one can relax constraints on w i , . . . w i+p in the precondition, i.e., remove all atoms of the form rn(w i , . . . w i+p ) or P(X) where X ⊆ {w i , . . . w i+p } and eliminate the variables from arithmetic predicates: for a predicate P (w i , . . . w i+p , x, y, z, ...) that imposes linear constraints on the values of variables, one can use elimination techniques such as Fourier-Motzkin to compute a new predicate P on x, y, z.... We hence have 2 AK possible assignments. For every possible assignment Ass X , we can define the set V X of variables that can be eliminated, and we can compute the formula φ k\Ass X that eliminates relational statements matching the newly inserted record according to Ass X from φ k , and computes new predicates. Hence, under the assumption that Ass X is a correct assignment, D 1 , . . .

D j . . . D k |= φ k iff D 1 , . . . D i . . . D k |= φ k\Ass X .
For ψ post to hold after insertion, there must be at least a correct assignment.

The precondition for ψ post that has to be satisfied by D 1 , . . . D i . . . D k hence becomes : wp

[Additive]ψ post = k=1..K ∨ 1..2 AK ∃V 1 \ V X ∀V 2 φ k\Ass X
One can notice that if ψ post is separated, the resulting formula is still separated.

Lemma 10 (Weakest precondition for record deletion). Let φ be a FO formula, and act be an atomic action that removes a record from a dataset. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formulas, then ψ is also separated.

Proof. Record deletion removes a record from an existing dataset. Let D j be a dataset with relational schema rs = (rn, A) with A = (a 1 , . . . a p ) such that D 1 , . . . D j . . . D k |= ψ post and is obtained after deletion a record from an input dataset D i with the same relational schema. Let r = rn(v 1 , . . . v p ) be the tuple removed from D i . We can rewrite the statement D j |= ψ post as D i \ {r} |= ψ post . Now, for every possible instance of record r there are two possibilities: either presence of r does not falsify ψ post , or r is a record that falsifies ψ post if it appears in dataset D i .

In the first case, we have that D i |= ψ. In the second case, we have that D j {r} |= ¬ψ. Formula ¬ψ is a separated formula obtained in the usual way by inverting existential and universal quantifiers in the prefix of ψ and negation of atoms in the matrix. As existence of record r is required we have that r necessarily matches (at least) one of the positive relational statements rn(w i , ..w i+p ) in ¬ψ. As for record additions, we can build a formula ¬ψ X in BSR form that should hold under the assumption that assignment X assigns the field values of r to some relational statements of ¬ψ. More precisely, ¬ψ X is the formula obtained by removing relational statements assigned to r in the BSR form computed from ψ. The weakest precondition for deletion that has to be satisfied by D 1 , . . . D i . . . D k becomes : wp

[Del]ψ = Q(V ), ψ ∧ X∈Ass Q(V \)¬ψ X
Notice that if ψ is in separated from, then wp[Del]ψ is also in separated form.

Lemma 11 (Weakest precondition for datasets decomposition). Let φ be a FO formula, and act be an atomic action that decomposes a dataset into smaller datasets. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formula, then ψ is also separated.

Proof. The Decomposition of a task is a higher order operation to split a task into several orchestrated subtasks. In particular, this operation splits an input dataset D i with relational schema rs = (rn, A) into a set of datasets D 1 , . . . D l . Each D j , j ∈ 1..l is obtained through application of a function f j to the input dataset D i . The relational schemas rs j = (rn j , A j ) of D j 's need not be the same as rs. Property ψ is of the form ψ = Q(V ), φ, and such that φ contains positive relational statement of the form rn j (w 1 ..w |Aj | ) ∈ D j , and negative relational statements of the from ¬rn j (w 1 ..w |Aj | ) ∈ D j . As we have that D j is a dataset obtained as a function f j (D i ) we can rewrite ψ as an equivalent formula ψ 2 = Q(V ), φ 2 , where φ 2 is obtained by replacing every instance of rn j (w i ..w i+|Aj |-1 ) ∈ D j by rn j (w i ..w i+|Aj |-1 ) ∈ f j (D i ) in formula φ. Let us assume that f 1 , . . . f l are simply selections of records according to predicates P 1 , . . . P l that form a partition of D. Let p = |A|. Statement rn(w i , w i+p ) ∈ f j (D i ) holds iff there exists a record r = (v 1 , . . . v p ) in D i that is a solution for formula P j (w i , . . . w i+p ). Equivalently, a positive statement of the from rn j (w k , . . . w k+|Aj |-1 ) ∈ f j (D i ) can be replaced by rn j (v k , . . . v k+|Ai|-1 ) ∈ D i ∧ P j (w k , . . . w k+|Aj |-1 ), and a negative statement of the form ¬rn j (v k , . . . v k+|Aj |-1 ) ∈ f j (D i ) can be replaced by ¬ rn j (v k , . . . v k+|Ai|-1 ) ∈ D i ∧ P j (w k , . . . w k+|Aj |-1 ) . Letting φ 3 be the formula φ 2 where every relational statement has been replaced this way, and letting Q (V ) denote the prefix in which every instance of w k , . .

D i |= ∃v 1 , v 2 , z, t, rn 1 (v 1 , v 2 ) ∈ D i ∧ v 1 < 10 ∧rn 2 (v 3 , v 4 ) ∈ D i ∧ v 3 < v 4 ∧ v 2 = v 3
Data distribution performed by splits is mainly a generalization of selection. Indeed if ψ post is a separated formula, then all atoms in wp[Decomp]ψ are separated, and wp[Decomp]ψ a separated formula. Now that we have defined weakest preconditions for basic operation that manipulate data , we can formalize how these conditions are associated to steps along a run of a complex workflow. Let ρ = C 0 . . . C n be a run, that ends in a configuration where a node n k with input data D k can be split. We will define inductively a sequence W P 0 . . . W P n-1 of conditions to be met at each stage such that condition D n = ∅ is met at step n (hence leading to an unavoidable deadlock). If a condition W P i = D 1 , . . . D m |= ψ has to be met when reaching a configuration C i , then the condition associated with W P i-1 is the weakest precondition such that W P i holds. Depending on the nature of the move C i-1 -→ C i , W P i-1 is of the form D 1 , . . . D q |= ψ i-1 , where ψ i-1 is computed inductively as wp For automatic actions executions, the operation used is a combination of selection, projection, R2R transformations and the weakest precondition follows the rules defined above. For splitting, the operation used is a decomposition of a particular dataset according to a set of functions f 1 , . . . f k , to obtain new datasets and new data assignments. If W P i is of the form D 1 , . . . D m and datasets D n , . . . D n+k are obtained by splitting a node and its input data D then W P i-1 is of the form D 1 , D k-1 , D, D n+k+1 |= wp[decomp]ψ i . For user actions that are input or deletions, one transforms a single datasets D j and W P i-1 is of the form D 1 , . . . D j , . . . D m |= ℘[add/remove]ψ i . Last, moves that simply perform user assignments do not change the nature of conditions that have to be met by a set of datasets. Let D 1 , D m |= ψ be the condition that has to be met at step k of a run ρ and let the move from C k-1 be an user assignment. Computing the weakest preconditions for addition of records calls for the use of an elimination step. Let ψ be an FO formula, with equality only. This formula can encode properties of the form x + 1 < y as boolean relations of the form P lus1 -LessT han(x, y). More generally, an inequality of the form x + k < y can be encoded as a boolean statement P lusk -Lessthan(x, y). Conversely, one can syntactically transform every expression of the form P lusk -Lessthan(x, y) into an inequality x + k < y. Now, when eliminating a variable y from a system of inequalities with equations of the form x + k < y and y + k < z one may obtain an inequality of the form x + (k + k ) < z. That is, if one converts again this inequality into a boolean assertion, one needs to use one more binary predicate. Hence, at every weakest precondition computation, the number of side arithmetic predicates in use increases. This is not a problem in our case however, as a finite number of new predicates is produced at each step, and the number of weakest precondition to compute is also bounded. Lemma 12. Let ρ = C 0 . . . C n be a path of the execution tree, where C n is a configuration that allows for the split of a particular dataset D n . Let W n ::= D n = ∅, and W 0 , . . . W n-1 be the weakest preconditions computed for each step of ρ. Then, the number of side arithmetic predicates used to define W P 0 , . . . W P n is bounded.

Proof. The elimination of variables while deriving the weakest precondition is carried using Fourier-Motzkin elimination technique (see appendix B.2). During each step, running an elimination step of one variable over m number of linear inequalities results into at most m 2 /4 = θ(m 2 ) linear inequalities in worst case. If we remove k number of variables, the algorithm must perform k step, hence the worst case the algorithm takes is θ(m 2 k ). FME may result into redundant set of linear inequalities. The detection and elimination of redundant variables is trivial and can be done using principle of linear programming. The scope of removal of redundant linear inequalities is beyond the scope of this paper. Now, in context to our problem, the total number of weakest precondition that needs to be calculated is n. Let m i be number of linear inequalities and k i denote the number of variables that need to be eliminated for the derivation of each w i in ρ. Hence, in the worst case the total number of new linear inequalities becomes n i=1 m 2 k i i . Now these inequalities can be expressed in terms of boolean assertion to get the predicates. Henceforth, as the number of new linear inequalities is bounded, we infer that the number of side predicate is also bounded. Lemma 13. Let ρ = C 0 . . . C n be a path of the execution tree, where C n is a configuration that allows for the split of a particular dataset D n . Let W P n ::= D n = ∅, and W P 0 , . . . W P n-1 be the weakest preconditions computed backwards for each step of ρ. Then, every W P j , j ∈ 1..n -1 is a weakest precondition of form W P j = D 1 , . . . D mj |= ψ j where ψ j is a separated FO formula.

Proof. The proof follows from the lemma ??. In a run ρ, every move m i transform a set of input data to output data using the transform function f i . Let v n be the split node in the execution tree resembling the configure C n . We compute the weakest precondition on the backward path from the node v n to the root node v 0 as v n → v n-1 → v 0 . At each node v j of the execution, there exist a function f j which transform the input dataset D 1 , . . . D mj to the corresponding set of output dataset. As per lemma ??, for every move m i , we can compute an effective weakest precondition wp[m i ]ψ posti . The weakest precondition is a FO formula ψ j that holds on input dataset D 1 , . . . , D mj such that after execution of the function f j , the output dataset must satisfy the given post condition ψ postj . Hence, for every move m j there exist a weakest precondition W P j such that D 1 , . . . D mj |= ψ j . With all the above lemmas, we have shown that the weakest precondition for a FO formula and actions that are projections, deletion or insertion of records, field addition, splits of datasets, joins, atomic execution of tasks transforming one record or all records, application of linear transformation of records. All actions occurring during the execution of a complex workflows can be expressed as a sequence of all these basic transformation of datasets (for instance, insertion of imprecise data can be seen as an insertion of a record followed by a linear transformation.) As all weakest preconditions for basic transforms of dataset are FO formulas, and as separated formulas also give separated weakest preconditions, we obtain our result.

B Additional material

For the convenience of readers, this section provides additional material on Symbolic execution trees and on the elimination technique (Fourier-Motzkin) used to compute new predicates on record.

B.1 Symbolic Execution Tree

Remind that a symbolic execution tree is a tree (V, E) where every vertex represents a set of configurations of a complex workflow that only differ with respect to their data assignment, and E represents moves among these configurations (user assignments, task executions, refinements). Figure 10 represents a symbolic execution tree. Vertices of the tree are represented by circles. Deadlocked vertices are represented by dotted circles, terminated vertices by dotted-dashed circles, and potential deadlocks by circles with dashed lines. Two vertices v i , v j are connected by an arrow iff there exists an action (user assignment, task execution, complex task refinement) that transforms the configuration represented by vertex v i into another configuration represented by vertex v j .

If the execution tree of a complex workflow contains a deadlocked vertex, then obviously all executions of the workflow do not terminate, as there is a path from the initial configuration to a deadlocked situation, and that the sequence of actions represented by this path cannot be prevented by the contents of data forged during the execution.

If the execution tree contains a potential deadlock V i = (W i , Ass i , Dass S i ), then the workflow part W i of this vertex contains a split node n, minimal in the workflow. To be able to split and distribute data, Dass i (n), the data input to n should not contain an empty dataset. Otherwise, an execution starting from a configuration of the form C i = (W i , Ass i , Dass i ) will eventually deadlock. On the Figure, the property to check is that no execution ending in a configuration with signature v 3 and such that dataset D 3 is empty is accessible. In this example, if there is no way to derive preconditions for D in such that D 3 = ∅, then the split operation can be done safely, and all executions stating from v 3 terminate.

B.2 Elimination with Fourier-Motzkin

The Fourier-Motzkin Elimination (FME) technique is a standard algorithm to eliminate variables and solve systems of linear inequalities. Let X = {x 1 , . . . x k } be a set of variables. A system of linear inequalities over X is an expression of γ ::= A.X ≤ B, i.e. a collection of inequalities of the form a 1 .x 1 + a 2 .x 2 + . . . a k .x k ≤ b. Given a variable x i , the FME technique computes a new system of inequalities γ ::= A .X ≤ B over X = X \ {x i }, and such that γ has a solution if and only if γ has a solution. The algorithm works in three steps:

Step 1: Normalize all inequalities in γ, i.e. rewrite every inequality containing x i of the form

a 1 .x 1 + a 2 .x 2 + • • • + a i .x i + • • • + a k .x k ≤ b
into a new inequality of the form

x i ≤ b a i - a 1 a i .x 1 - a 2 a i .x 2 -• • • - a k a i .x k or x i ≥ b a i - a 1 a i .x 1 - a 2 a i .x 2 -• • • - a k a i .x k
Step 2: separate the obtained system into γ + , γ -, γ ∅ , where γ + contains all inequalities of the form

x i ≥ f (x 1 , . . . x i-1 , x i+1 , . . . . . . x k ), γ -contains all inequalities of the form

x i ≤ f (x 1 , . . . x i-1 , x i+1 , . . . . . . x k ), and γ ∅ all other inequalities that do not refer to x i .

Step 3: create a new system of inequalities that contains γ ∅ and, for each pair of inequalities

x i ≤ f 1 (x 1 , . . . x i-1 , x i+1 , . . . , x k ) ∈ γ - and x i ≥ f 2 (x 1 , . . . x i-1 , x i+1 , . . . , x k ) ∈ γ + , a fresh inequality of the form f 2 (x 1 , . . . x i-1 , x i+1 , . . . , x k ) ≤ f 1 (x 1 , . . . x i-1 , x i+1 , . . . , x k )

The new system obtained is still a system of linear inequalities. It does not contain variable x i and is equivalent to the original system.

Fig. 1 .

 1 Fig. 1. A simple actor popularity poll.

Fig. 3 .

 3 Fig.3. A refinement of node n1, replaced by the profile for task t like in Figure2.

  in ) = D out i

Fig. 4 .

 4 Fig. 4. Application of semantic rule R1

Fig. 5 .

 5 Fig. 5. Application of semantic rule R2

Fig. 6 .

 6 Fig. 6. Application of semantic rule R3

Figure 8 Fig. 8 .

 88 Figure 8 gives an example of run. The top-left part of the figure is an initial configuration C 0 = (W 0 , Ass 0 , Dass 0 ) composed of an initial workflow W 0 , an empty map Ass 0 and a map Dass 0 that associates dataset D in to node n i . The top-right part of the figure represents the configuration C 1 = (W 1 , Ass 1 , Dass 1 ) obtained by assigning user u 1 for execution of task t 2 attached to node n 2 (Rule 1). The bottom part of the Figure represents the configuration C 2 obtained from C 1 when user u 1 decides to refine task t 2 according to

Proposition 4 .

 4 Complex workflows that are not recursion free have non-terminating executions. Proposition 5. Let CW = (W 0 , T , T cs , U, sk, P) be a complex workflow. One can decide if CW is recursion free in O(|T 2 cx | + |P(T cx , U)|).

2

 2

.

  . w k+|Aj |-1 is replaced by fresh variables v k , . . . v k+|Aj |-1 , the weakest precondition needed such that D1 , . . . D 1 , . . . D l . . . D k |= ψ is hence wp[Decomp]ψ = Q (V ), φ 3If one function f j is not simply a selection but also computes new attributes for records in D j from values attached to variables v k , . . . v k+|Ai|-1 then one can also replace rn j (w k , . . . w k+|Aj |-1 ) by another FO formula following the lines of R2R replacement. We leave details of the construction to readers.Let us illustrate it with a small example. LetD 1 , D 2 |= ∃x, y, z, t, rn 1 (x, y) ∈ D 1 ∧ rn 2 (z, t) ∈ D 2 ∧ y = z, with rs 1 = (rn 1 , {a 1 , a 2 } rs 2 = (rn 2 ,{a 3 , a 4 }, and Dom(a 1 ) = dom(a 2 ) = dom(a 3 ) = dom(a 4 ) = R. Let us assume that D 1 and D 2 are obtained by decomposition of an input dataset D i with relational schema rs i = (rn i , {b 1 , b 2 }, through selection with selection predicates P 1 ::= b 1 < 10 and P 2 ::= b 1 < b 2 . Then, wp[Decomp]ψ is the formula

  [op 1 ](wp[op 2 ](. . . wp[op k ]ψ i )), and op 1 , . . . op k is the sequence of operations used to transform datasets D 1 , D q in C i-1 into D 1 , . . . D m in C i . The weakest precondition for move from C i-1 to C i is hence D 1 , . . . D m |= wp[op 1 ](wp[op 2 ](. . . wp[op k ]ψ i )).

Fig. 10 .

 10 Fig. 10. Symbolic Execution Tree

  . . , dom s , a finite set of attribute names att and a finite set of relation names relnames. Each attribute a ∈ att is associated with a domain dom(a) ∈ dom. A relational schema (or table) is a pair rs = (rn, A), where rn is a relation name and A denotes a finite set of attributes. Intuitively, attributes are column names in a table. The arity of rs is the size of its attributes set. A record of a relational schema rs = (rn, A) is tuple rn(v 1 , . . . v |A| ) where v i ∈ dom(a i ) (it is a row of the table), and a dataset with relational schema rs is a multiset of records of rs. A database schema DB is a non-empty finite set of tables, and an instance over a database DB maps each table in DB to a dataset.

  11 (Deadlocks, Potential deadlocks).A symbolic configuration C S = (W, Ass, Dass S ) is final if its workflow part consists of a single node n f . It is a deadlock if it has no successor. It is a potential deadlock iff a split action can occur from this node, i.e. there exists n, n 1 , n 2 ∈ W such that n is minimal and {(n, n 1 ); (n, n 2 )} ⊆-→ W .

  is of the from ∀ Xφ 0 , this can be done in O(|D in | |ψ0| . If the answer is true then we have found preconditions that are satisfied by D in and that are sufficient to obtain an empty dataset at configuration C i in a run C 0 . . . C i that has signature C S Tcx . Considering that data fields are encoded with c bits of information, D in is a dataset of size in O(2 r.c ). Hence, the overall complexity to check that C S 0 . . . C S i is a witness path that deadlocks in 2 -EXP T IM E.

	0 . . . C S i , i.e. C S 0 . . . C S

→ i

witnesses the existence of a deadlock. Overall, one has to solve up to i < 3.K Tcx satisfiability problems for universal FO formulas ψ i-1 , ψ i-2 . . . ψ 1 of size smaller than r i , and a model checking problem for input D in with a cost in O(|D in | r i ). The satisfiability problems are NEXPTIME in the size of the formula

[START_REF] Harry | Complexity results for classes of quantificational formulas[END_REF]

, hence a complexity that is doubly exponential in K

  do All Split nodes have non-empty input datasets 22 if ∃v ∈ V without successors and v is not final then

	9	Check satisfiability of W P
	10	if W P not satisfiable then
	11	break; //unfeasible path
	12	end
	13	W P ::= wp[ai-1]W P
	14	end
	15	//WP= WP0
	17	return NO-TERM
	18	end
	19	end
	20 end
	21 //23	return NO-TERM
	24 end
	25 return TERM

16

if W P satisfiable ∧ Din |= W P then

https://www.cancerresearchuk.org

http://zoo1.galaxyzoo.org

https://www.mturk.com

https://www.foulefactory.com

https://www.crowdflower.com

http://www.spipoll.org/

http://zoo1.galaxyzoo.org/

.t 1 .λ(w f ) k .λ(n f ). In this recursive scheme, the workfow part of configurations obviously grows, but one can easily find unbounded recursive schemes with unboundedly growing of data (for instance if λ(w f ) adds a record to some dataset). Hence, without

A Appendix : proofs

A.1 Proof of Theorem 1 Theorem 1 Existential termination of complex workflows is an undecidable problem.

The proof is done by reduction from the halting problem of two counter machines to termination of complex workflows.

Proof. A 2-counter machine (2CM) is a tuple Q, c 1 , c 2 , I, q 0 , q f where, -Q is a finite set of states.

q 0 ∈ Q is the initial state, q f ∈ Q is the final state.

c 1 , c 2 are two counters holding non-negative integers.

-I = I 1 ∪ I 2 is a set of instructions. Instructions in I 1 are of the form inst q = inc(q, c l , q ), depicting the fact that the machine is in state q, increases the value of counter c l by 1, and moves to a new state q . Instructions in I 2 are of the form inst q = dec(q, c l , q , q ), depicting the fact that the machine is in state q, if c l == 0, the machine moves to new state q without making any change in the value of counter c l , and otherwise, decrements the counter c l and moves to state q . We consider deterministic machines, i.e. there is at most one instruction inst q per state in I 1 ∪I 2 . At any instant, the machine is in a configuration C = (q, v 1 , v 2 ) where q is the current state, v 1 the value of counter c 1 and v 2 the value of counter c 2 .

From a given configuration C = (q, v 1 , v 2 ), a machine can only execute instruction inst q , and hence the next configuration ∆(C) of the machine is also unique. A run of a two counters machine is a sequence of

). The reachability problem is defined as follows: given a 2-CM, an initial configuration C 0 = (q 0 , 0, 0), decide whether a run of the machine reaches some configuration (q f , n 1 , n 2 ), where q f is a particular final state and n 1 , n 2 are arbitrary values of the counter. It is well known that this reachability problem is undecidable.

Let us now show how to encode a counter machine with complex workflows.

-We Consider a dataset D with relational schema rs = (R, {k, cname}) where k is a unique identifier, and cname ∈ Cnt 1 , Cnt 2 , ⊥. Clearly, we can encode the value of counter c x with the cardinal of

We start from a configuration where the dataset contains a single record R(0, ⊥) -For every instruction of the form inc(q, c x , q ) we create a task t q , and a workflow W inc q , and a worker u q , who is the only user allowed to execute these tasks. The only operation that u q can do is refine t q with workflow W inc q . W inc q has two nodes n inc q and n q such that (n inc q , n q ) ∈-→, λ(n inc q ) = t inc q and λ(n q ) = t q . Task t inc q is an atomic task that adds one record of the form (k , Cnt x ) to the dataset. Hence, after executing tasks t q and t inc q , the number of occurrences of Cnt x has increased by one. -For every instruction of the form dec(q, c x , q , q ), we create a complex task t q and a worker u q who can choose to refine t q according to profiles P rof ile(t q , u q ) = {W q,Z , W q,N Z }. The choice of one workflow or another will simulate the decision to perform a zero test or a non-zero test. Note that as the choice of a workflow in a profile is non-deterministic, worker u q can choose one or the other. -Let us now detail the contents of W q,N Z . This workflow is composed of nodes n div q , n Cx q , n Cx∪⊥ q , n ⊗ q , n dec q and n q , respectively labeled by tasks t div q , t Cx q , t Cx∪⊥ q , t ⊗ q , t dec q and t q . The dependence relation in W q,N Z contains pairs (n div q , n Cx q ), (n div q , n Cx∪⊥ q ), (n Cx q , n ⊗ q ), (n Cx∪⊥ q , n ⊗ q ), (n ⊗ q , n dec q ) and (n dec q , n q ). The role of t div q is to split Dass(n div q ) into disjoint parts: the first one contains records of the form R(k, C x ) and the second part consists of all other remaining records. Tasks t Cx q and t Cx∪⊥ q simply forward their inputs, and task t ⊗ q computes the union of its inputs. Note however that if one of the inputs is empty, the task cannot be executed. Then, task t dec q deletes one record of the form R(k, C x ). Hence, if D q = Dass(n q ) is a dataset that contains at least one record of the from R(k, C x ), the execution of all tasks in W q,N Z leaves the system in a configuration with a minimal node n q labeled by task t q , and with Dass(n q ) = D q \R(k, C x ) -Let us now detail the contents of W q,Z . This workflow is composed of nodes n div q , n Cx∪⊥ q , n id q , n btest q , n done q , n q respectively labeled by tasks t div q , t Cx∪⊥ q , t id q , t btest q , t done q , t q . The flow relation if given by pairs (n div q , n Cx∪⊥ q ), (n div q , n id q ) (n Cx∪⊥ q , n btest q )(n btest q , n done q ) and (n id q , n done q

). The role of task t div q is to project its input to denote the fact that ψ pre is this weakest precondition, or simply ψ pre wp[tr]ψ post when outputs are clear from the context. Now, moves from one configuration to another are atomic actions that may involve several successive transformations. Similarly, given a move mv from a configuration C to a configuration C , we write ψ pre wp[mv]ψ post to denote that ψ pre is the precondition on datasets in use in C required for ψ post to hold in datasets in use in C after move mv. First, for each type of basic transformation tr, we give the weakest precondition of any FO formula ψ post . We then build preconditions for atomic moves from them, to prove that all preconditions needed to reach deadlocks can be expressed as FO properties. For each transformation, we also show that separated FO formulas also give separated weakest preconditions. For a formula ψ, we denote by V ars(ψ) the variables x 1 . . . x n used in ψ. In the rest of the proof, we assume that all formulas over variables x 1 , . . . , x n are in prenex normal form, and more precisely are of the form ψ ::= Q(V ars(φ)), φ, where Q(V ars(ψ)) is the prefix (a string of variables and quantifiers ∀, ∃), φ is a boolean combination of quantifier free FO statements called the matrix. It includes relational statements of the form rn(x 1 , . . . x k ) ∈ D j to describe the fact a record of the form rn(w i , . . . w i+p ) belongs to dataset D j , predicates indicating constraints on values of variables, such as x 1 ≤ x 2 , and equalities. Note that computing a weakest precondition for a transformation that impacts the contents of a dataset D i when D i |= ψ yields properties that should be satisfied jointly by several datasets D 1 , . . . , D q used to forge the contents of D i , and that these properties cannot be necessarily considered as independent preconditions of the form D 1 |= ψ 1 , . . . D q |= ψ q . As datasets contents and properties are not independent, we will write global properties of datasets used by all minimal nodes in configurations under the form D 1 , . . . D k |= ψ. We denote by RS(ψ) the set of relational statements used in ψ. We now provide a series of lemmas proving that for each type of action, weakest preconditions are effectively computable, and transform separated FO formulas into separated FO formulas.

Lemma 2 (Weakest precondition for Projection). Let φ be a FO formula, and act be an atomic action that projects the contents of some datasets. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formula, then ψ is also separated.

Let us assume that D 1 , . . . , D k |= ψ post and that D j is a dataset with relational schema rs j = (rn j , A j ), obtained by projection of some input dataset D i with relational schema rs i = (rn i , A i ) on a subset of its fields. We have A j ⊆ A i , and letting A i = (a 1 , . . . a k ), A j is of the form (a i1 , a i2 , . . . a iq ). Clearly, if a FO formula ψ addresses values of attributes (a i1 , a i2 , . . . a iq ) of records in relational schema rs j , if a record r = (v 1 , . . . , v q ) satisfies ψ and is obtained by projection of a record r = (v 1 , . . . , v k ) with relational schema rs i , then r also satisfies ψ. Similar reasoning holds for several instances of rs j . Let RS(ψ post ) contain KP instances of relational schema rs j . Then, we can replace each instance of rn j (x i , . . . x i+q ) by an instance of rn i (x i , . . . x i+q , y i+q+1 , y i+k ), where y i s are new variables addressing values of fields in A i \ A j . We denote by ψ post [rs j /rs i ] the formula ψ post where every instance of rs j has been replaced this way. Similarly, letting Y = {y i+q+1 , . . . y i+k | i ∈ 1..KP }, we denote by Q (V ars(ψ) ∪ Y ) the sentence Q(V ars(ψ)).Q Y where Q Y = q 1 .y 1 . . . q n y n is a sentence where y i 's are all variables of Y , q i 's their quantifiers, and that associates existential quantifiers to variables of Y appearing in statements of the form rn i (. . . ) and universal quantifiers to variables of Y appearing in statements of the form ¬rn i (. . . ). The weakest precondition for projection is hence a precondition on D 1 , . . . D i , . . . , D k , given as wp

Clearly, as variables are added to increase the number of fields in relational statements, if ψ post is separated, wp[P roj]ψ post is also separated. with predicate P is defined as

One can notice that this weakest precondition is a rather syntactic transformation, that replaces atoms of the form rn(x 1 , . . . x k ) by rn(x 1 , . . . x k ) ∧ P (x 1 , . . . x k ). If x 1 , . . . , x k are all existentially quantified variables (resp. all universally quantified variables in ψ post , then they remain existentially (resp universally quantified). Hence, if ψ post is separated, then wp[Selection(ψ sel )]ψ post is also separated.

Lemma 5 (Weakest precondition for field addition). Let φ be a FO formula, and act be an atomic action that adds new fields to a dataset. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formulas, then ψ is also separated.

Proof. The Field Addition action adds an extra field to an existing relational schema, and populates this field. This transformation models entry of new information by users for each record in a dataset (for instance a tagging operation). Let D 1 , . . . D j , . . . D k |= ψ post , and let D j be the modified dataset. Let D j be a dataset over relational schema rs j = (rn j , A j ), where A j = (a 1 , . . . , a p ). As D j is obtained by adding a field to D i , we have A i = (a 1 , . . . a p-1 ). We assume that constrains on possible values of new fields are provided by a predicate P add (v 1 , . . . v p ) that is true if, value v p is a legal value for field a p if a 1 , . . . a p-1 take values v 1 , . . . v p (if the value of field a p can be any value in its domain, this predicate is simply true). Let K f ld be the number of sub-formulas of the form rn j (...) or ¬rn(...) in ψ post (again these sub-formulas are over disjoint variables). Formula ψ post is hence a formula over variables W = V ars(φ post ) that contain at least a set of variables w 1 , . . . w p , w p+1 . . . w K f ld .p appearing in relational sub-formulas. ψ post is of the form Q(V ars(ψ post )), φ, where φ is a boolean combination of relational statements and comparisons of field values. Here, we can transform φ over variables W into another formula φ [rnj |rni] , where every relation statement of the form rn j (w k , . . . , w p+k ) is replaced by a sub-formula rn i (w k , . . . w p+k-1 ) ∧ P add (w k , . . . w p+k ) in positive sub-formulas, and by a sub-formula of the form ¬(rn i (w k , . . . w p+k-1 ) ∧ P add (w k , . . . w p+k-1 ) otherwise.

The weakest precondition for the addition of a field a p hence becomes:

Let us assume that ψ post is separated. Then, as for the selection case, wp[F A(a p )]ψ post performs a syntactic replacement of a separated atom rn j (w k , . . . , w p+k ) by a conjunction of separated atoms rn i (w k , . . . w p+k-1 )∧ P add (w k , . . . w p+k ). Hence wp[F A(a p )]ψ post is also separated. Lemma 6 (Weakest precondition for field enlargement). Let φ be a FO formula, and act be an atomic action that selects records that adds imprecision to the contents of a field in dataset. Then one can effectively compute an FO formula ψ = wp[act]φ. Moreover, if φ is a separated FO formula, then ψ is also separated.

Proof. Enlargement of field is used to model the fact that users answers are sometimes subject to imprecision. The effect of imprecision is to replace a value in some field of a particular dataset with continuous domain by another value that is close to the original value, i.e. at some distance δ. Let D j be an output dataset with relational schema rs(rn, A) where A = (a 1 , . . . , a p ), and obtained by making a particular field a j in an input dataset D i with the same relational schema imprecise. Enlargement of field function transforms every input record r 1 = (v 1 , . . . v j , . . . , v p ) where each v i is the value of a i to new record r 2 = (v 1 , . . . v j , . . . , w p ) such that v j ∈ [v j -δ, v j + δ] ∩ Dom(a j ). One can notice that enlargement preserves the relational schema of input dataset D i .

Let ψ post be a FO property over a set of variables W and let D 1 , . . . D j . . . D k |= ψ post . If K rn is the number of subformulas of the form rn(x 1 , . . . x p ) ∈ D j , then we can define ψ post as a formula over V = W ∪Y where W = w 1 , . . . w p , w p+1 . . . w Krn.p is the set of variables used in these relational statements and Y the other variables. ψ post is hence of the form ψ post = Q(V ), φ post .

The weakest precondition required so that D 1 , . . . D j . . . D k |= ψ post is a condition on values of variables in W such that, even after adding some imprecision to values of variables in set W imp = w j , w j+p , . . . w (Krn-1).p+j