Prof. Dr. Wolfgang Reisig

Petri nets are frequently composed of given nets. Literature suggests a lot of different composition operators, for different purposes and different classes of Petri nets. Formal definitions are frequently surprisingly technical, not matching the intuitively very elegant composition of Petri nets in the framework of their graphical representation. This paper suggests the universal net composition operator. This operator allows to specify any specific composition variant by very simple means, leaving all technical details to the operator, where they are treated once and for all. General properties of composition, in particular associativity, are inherited by all instantiations of the operator. We show the practical advantage of the universal composition operator by means of a lot of examples from various areas of Petri nets.

Abstract State Machines (henceforth referred to as just ASM) were introduced as ä computation model that is more powerful and more universal than standard computation models\" by Yuri Gurevich in 1985. Here we provide some intuitive and motivating arguments, and characteristic examples for (the elementary version of) ASM. The intuition of ASM as a formal framework for \"pseudocode\" algorithms is highlightes. Generalizing variants of the fundamental \"sequential small-step\" version of ASM are also considered.

Service-oriented Computing and Service-oriented Architectures aspire to better exploit existing middleware technologies. To this end, a more flexible, platform independent software design methodology is suggested, to develop rapid, low cost, interoperable, evolving and massively distributed software systems. Intended application areas include electronic commerce, information systems, supply chain control, and many other areas. Time is ripe to underpin this effort by theoretically well-founded concepts to model services, and to analyze such models. In this paper we suggest first proposals and principles for a comprehensive theory of services.

The Scholten/Dijkstra "Pebble Game" is re-examined. We show that the algorithm lends itself to a distributed as well as an online version, and even to a reversed variant. Technically this is achieved by exploiting the local and the reversible nature of Petri Net transitions. Furthermore, these properties allow to retain the verification arguments of the algorithm.

Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen, die durch Petrinetze modelliert werden, haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion, also eine verteilende Verfeinerung. Die Arbeit klärt den Zusammenhang von Eigenschaften des Verfeinerungsnetzes und den bei der Verfeinerung gültig bleibenden Eigenschaften des verfeinerten Algorithmus. Hierbei sind Kausalitäten im Verfeinerungsnetz von entscheidender Bedeutung. Die Anwendung der Methode wird in der Arbeit an anschaulichen Beispielen demonstriert.

Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.

Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.

Gurevich's sequential Abstract State Machines (ASMs)are taken as a basis for the construction of distributed ASMs as sets of sequential ASMs. A theorem on the expressive power of distributed ASMs is proven in analogy to Gurevich's classical theorem on the expressive power of sequential ASMs.

The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.

Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emphsequential algorithms by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.

An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion two techniques to reduce the model's state space are presented. By use of these techniques we detected several potential hazards and a deadlock in the wrapper.

Zur adäquaten Nutzung von Workflow-Implementierungen kommunizierender Geschäftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und dafür Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Geschäftsprozess-Modellierungssprache BPEL demonstriert.

BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.

An asynchronous wrapper of a fabricated GALS system is analyzed for hazards. For this purpose a Petri net based modelling approach of this GALS wrapper is presented. In our model the question whether a hazard can occur in a gate is reduced to a model checking problem: the reachability of a particular marking in the Petri net. In order to alleviate state space explosion three techniques to reduce the model?s state space are presented. By use of these techniques we detected several potential hazards in the wrapper.

Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.

Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.

Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.

The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

The Temporal Logic of Distributed Actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. TLDA can be syntactically viewed as a slight extension of TLA. We propose a different semantical model based on partial order which evidently increases the expressiveness of the logic. Local variable updates in a system are explicitly modeled and expressed by TLDA formulas. Consequently, we can distinguish between concurrency and nondeterministic choice. All valuable features of TLA (composition is conjunction, implementation is implication) are retained. In addition, we are able to describe some important phenomena and properties typical for distributed systems.

Conventional computation models assume symbolic representations of states and actions. Gurevich's "Abstract-State Machine" model takes a more liberal position: Any mathematical structure may serve as a state. This results in "a computational model that is more powerful and more universal than standard computation models". We characterize the Abstract-State Machine model as a special class of transition systems that widely extends the class of "computable" transition systems. This characterization is based on a fundamental Theorem of Y. Gurevich.

Abstract-State Machines have been introduced as ?a computation model that is more powerful and more universal than standard computation models?, by Yuri Gurevich in 1985 ([Gur85]). ASM gained much attention as a specification method, in particular for the description of the semantics of programming languages, communication protocols, distributed algorithms, etc. Gurevich proved recently that a sequential algorithm must only meet a few, liberal requirements, to be representable as an ASM. We re-formulate Gurevich?s requirements for sequential algorithms, as well as the semantics of ASM-programs and the proof of his main theorem. A couple of examples support and explain intuition and motivation of ASM.

Concurrency is frequently employed as a means to increase the performance of computing systems: a conventional sequential program is designed, to be parallelised later on. This contribution is intended to show that concurrent systems can also differ essentially from conventional, sequential systems, with respect to the kind of problems to be solved, and even to the principal limits of capability and performance. This paper surveys particular concepts and properties of concurrent systems, followed by a choice of models that more or less reflect those properties. Finally, the author discusses a typical example of an algorithm for concurrent systems.

Modern information processing devices are normally considered distributed systems. Then particular processes are generally represented by sequences of states and/or transitions. In this book a different approach is developed where processes are only derived from the causal dependicies. The conceptual and practical advantages are explained using the problem of the ``dining philosophers''.

A logic is introduced, tailored for causality based partial order semantics of nonsequential systems. Properties which are essential for such systems can be formulated in the logic. Technically, the system model we consider is the most fundamental version of Petri Nets. The logic resembles to a liniear time propositional logic, applied to a universe of sets of partially ordered potential states.