Ian Foster

Distinguished Carl Adam Petri Lecture

Reasoning about Discovery Clouds

A discovery cloud is a set of automated, cloud-hosted services to which individuals may outsource their routine and not-so-routine research tasks: finding relevant data, inferring links between data, running computational experiments, inferring new knowledge claims, evaluating the credibility of knowledge claims produced by others, designing experiments, and so on. If developed successfully, a discovery cloud can accelerate and democratize access to data and knowledge tools and the collaborative construction of new knowledge. Such systems are also fascinating to consider from a reasoning perspective because they integrate great complexity at multiple levels: the underlying cloud-based hardware and software, for which issues of reliability and responsiveness may be paramount; the knowledge bases and inference engines that sit on that cloud substrate, for which issues of correctness may be less well defined; and the human communities that form around the discovery clouds, and that arguably form as much as part of the cloud as the hardware, software, and data. In this talk I raise questions about what it might mean to reason about such systems. I do not promise any answers.

Manfred Broy

Keynote Speaker

From Actions, Transactions, and Processes to Services

For the problem domain of business process engineering we introduce, model, and formalize notions of business processes such as action, actor, event, business process, business transaction. In addition, for the solution domain of service-oriented architectures (SOA) we introduce, model, and formalize notions of service, service composition, service-oriented architecture, and layered SOA in a systematic way. We do that by a rigorous mathematical system model. For that purpose, we first develop a basic mathematical system model for formalizing fundamental concepts of processes and services. The goal is to provide a minimal set of formal modeling concepts, nevertheless expressive enough to formalize key notions and concepts in business process engineering and service-oriented architectures capturing also their mutual relationships. This way, the relationship between central notions in business process modeling is captured formally, which provides a basis for a methodology for deriving the systematic specification and design of service-oriented architectures from business process modeling. The purpose of the approach is manifold; one goal is a clear definition of terminology, concepts, terms, and models in business process modeling and SOA; another goal is a rigorous formal basis for the specification, design, and development of business processes and, in particular, SOAs. We end up with a strictly formal concept for the development steps from business process models to services as part of a SOA-oriented development process.

Jetty Kleijn

Keynote Speaker

On Processes and Paradigms

Understanding the causal relations between occurrences of actions (events) during a run of a distributed system is crucial for reasoning about its behaviour. We will present a semantical theory for extended Elementary Net (EN) systems based on executions and observations represented as sequences of steps (sets of one or more simultaneously occurring transitions). When step sequences are used to describe a run of an EN system, transitions that can be observed one after the other in any order can also occur together in a step and vice versa. This property reflects the ‘true concurrency paradigm’. In this case the structure of runs can be described in terms of partial orders. In general however, the relational structures obtained from sets of step sequences are not partial orders. We characterise the general order structures that correspond to the least restrictive, most general paradigm and that can thus capture any concurrent history consisting of labelled structures underlying the step sequences that form the observations of a run. These structures prove to match exactly with step traces, a generalisation of Mazurkiewicz traces to equivalence classes of step sequences. EN systems with inhibitor arcs and mutex arcs are a system model for the general concurrency paradigm. Their process semantics and step trace semantics fit together through these general order structures. The presentation is based on and extends earlier work done together with Ryszard Janicki, Maciej Koutny, and Łukasz Mikulski

Sławomir Lasota

Keynote Speaker

Decidability border for Petri nets with data: WQO dichotomy conjecture

In Petri nets with data, every token carries a data value, and executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems for Petri nets with data may depend on the structure of data domain. For instance, if data values are only tested for equality, decidability status of the reachability problem is unknown (but decidability is conjectured). On the other hand, the reachability problem is undecidable if data values are additionally equipped with a total ordering.
We investigate the frontiers of decidability for Petri nets with various data, and formulate the WQO Dichotomy Conjecture: under a mild assumption, either a data domain exhibits a well quasi-order (in which case one can apply the general setting of well-structured transition systems to solve problems like coverability or boundedness), or essentially all the decision problems are undecidable for Petri nets over that data domain.

Philip Wadler

Keynote Speaker

The Inevitable Coincidence: A Basis for Concurrency and Distribution

The principle of Propositions as Types is an inevitable coincidence: independently formulated notions of logic and computation turn out to be identical. Under it, propositions correspond to types, proofs to programs, and simplification of proofs corresponds to evaluation of programs. It is a robust notion, adapting to almost all areas of computation, but with one important exception: concurrency! I will explain what Propositions as Types means, why it is important, and why concurrency and distribution may at last be about to benefit from this approach. And I will explain how this links to a broader research effort on extending the benefits of types to communication by introducing session types.