Abstract The first Provenance Challenge was set up in order to provide a forum for the community to understand the capabilities of different provenance systems and the expressiveness of their provenance representations. To this end, a functional magnetic resonance imaging workflow was defined, which participants had to either simulate or run in order to produce some provenance representation, from which a set of identified queries had to be implemented and executed. Sixteen teams responded to the challenge, and submitted their inputs. In this paper, we present the challenge workflow and queries, and summarize the participants' contributions. Copyright © 2007 John Wiley & Sons, Ltd.

Abstract Taverna is a workflow workbench developed as part of the UK's myGrid project. Taverna's provenance model captures both internal provenance locally generated in Taverna and external provenance gathered from third‐party data providers. This model also supports overlaying secondary provenance over the primary logs and lineage. This design is motivated by the particular properties of bioinformatics data and services used in Taverna. A Semantic Web of provenance, Ouzo, is built to combine the above different provenance by means of semantic annotations. This paper shows how Ouzo can be mined by a provenance usage component, Provenance Query and Answer (ProQA). ProQA supports provenance retrievals as well as provenance abstraction, aggregation, and semantic reasoning. ProQA is implemented as a suite APIs which can be deployed as provenance services to compose system provenance workflows that analyse experiment results using the provenance records. We show how these features of Taverna's provenance support us in answering the questions from the provenance challenge workshop and a set of additional provenance queries. Copyright © 2007 John Wiley & Sons, Ltd.

This paper presents the formal syntax and the operational semantics of Taverna, a workflow management system with a large user base among the e-Science community. Such formal foundation, which has so far been lacking, opens the way to the translation between Taverna workflows and other process models. In particular, the ability to automatically compile a simple domain-specific process description into Taverna facilitates its adoption by e-scientists who are not expert workflow developers. We demonstrate this potential through a practical use case.

Provides a semantic framework for (first-order) message-passing process calculi by combining categorical theories of abstract syntax with binding and operational semantics. In particular, we obtain abstract rule formats for name and value passing with both late and early interpretations. These formats induce an initial-algebra/final-coalgebra semantics that is compositional, respects substitution and is fully abstract for late and early congruence. We exemplify the theory with the /spl pi/-calculus and value-passing CCS (calculus of communicating systems).

We develop a theory of abstract syntax with variable binding. To every binding signature we associate a category of models consisting of variable sets endowed with compatible algebra and substitution structures. The syntax generated by the signature is the initial model. This gives a notion of initial algebra semantics encompassing the traditional one; besides compositionality, it automatically verifies the semantic substitution lemma.

We present a categorical theory of 'well-behaved' operational semantics which aims at complementing the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if the operational rules of a programming language can be modelled as a natural transformation of a suitable general form, depending on functorial notions of syntax and behaviour, then one gets the following for free: an operational model satisfying the rules and a canonical, internally fully abstract denotational model which satisfies the operational rules. The theory is based on distributive laws and bialgebras; it specialises to the known classes of well-behaved rules for structural operational semantics, such as GSOS.