Prof. Dr. Wolfgang Reisig

Leiter des Lehrstuhles Theorie der Programmierung

Wolfgang Reisig (Foto mit freundlicher Genehmigung von H. Plötz)
Foto: H. Plötz
Adresse Humboldt-Universität zu Berlin
Institut für Informatik
Unter den Linden 6
10099 Berlin
Sitz Humboldt-Universität zu Berlin
Institut für Informatik
Haus IV, 1. Etage, Raum 116

Rudower Chaussee 25
12489 Berlin
Sprechstunde nach Vereinbarung
Telefon +49 30-2093-3066 (Sekretariat)
+49 30-2093-3065 (Büro)
Fax +49 30 2093-5484
E-Mail reisig@informatik.hu-berlin.de

Lebenslauf

Lehrveranstaltungen

Publikationen von Wolfgang Reisig

    2015

  • Völlinger, Kim, Reisig, Wolfgang
    Certifcation of Distributed Algorithms Solving Problems with Optimal Substructure
    In Software Engineering and Formal Methods, 2015
    close
  • 2013

  • Reisig, Wolfgang
    Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies
    Springer, 2013
    close
  • Reisig, Wolfgang
    The Synthesis Problem
    volume 7 of T. Petri Nets and Other Models of Concurrency 7, 2013
    close
  • Reisig, Wolfgang, Rozenberg, Grzegorz, Thiagarajan, P. S.
    In Memoriam: Carl Adam Petri
    volume 7 of T. Petri Nets and Other Models of Concurrency 7, 2013
    close
  • Reisig, Wolfgang
    Remarks on Egon Börger: "Approaches to model business processes: a critical analysis of BPMN, workflow patterns and YAWL, SOSYM 11: 305-318"
    volume 12 of Software and System Modeling 12 (1), 2013
    close
  • 2012

  • Reisig, Wolfgang
    A Fresh Look at Petri Net Extensions
    In Software Service and Application Engineering, 2012
    close
  • 2011

  • Reisig, Wolfgang
    Petri Nets
    In Modeling in Systems Biology, The Petri Net Approach, Springer, 2011
    close
  • Reisig, Wolfgang
    Rezension - Die vergessene Revolution oder die Wiedergeburt des antiken Wissens
    volume 34 of Informatik Spektrum, Springer 34, december 2011
    close
  • 2010

  • Reisig, Wolfgang
    Petrinetze: Modellierungstechnik, Analysemethoden, Fallstudien
    Leitfäden der Informatik, Vieweg+Teubner, 15 July 2010
    close
  • Reisig, Wolfgang
    50 Jahre Verhaltensmodellierung: Vom Modellieren mit Programmen zum Programmieren mit Modellen
    In Modellierung, 2010
    close
  • Blass, Andreas, Dershowitz, Nachum, Reisig, Wolfgang
    Yuri, Logic, and Computer Science
    In Fields of Logic and Computation, 2010
    close
  • 2009

  • Reisig, Wolfgang
    The Universal Net Composition Operator
    Forschungsbericht, Humboldt-Universität zu Berlin, jan 2009
    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.
    close
    close
  • Brauer, Wilfried, Reisig, Wolfgang
    Carl Adam Petri and ''Petri Nets''
    volume 3 of Advances in Computer Science and Engineering: Texts, Fundamental Concepts in Computer Science 3, Imperial College Press, 2009
    close
  • Reisig, Wolfgang
    Simple Composition of Nets
    In Proceedings of the 30th International Conference on Petri Nets and Other Models Of Concurrency, volume 5606 of Lecture Notes in Computer Science, Springer-Verlag, Paris, France, jun 2009
    close
  • 2008

  • Reisig, Wolfgang
    Abstract State Machines for the Classroom - The Basics
    volume XXII, 624 p. 69 illus., Hardcover of Monographs in Theoretical Computer Science. An EATCS Series, Logics of Specification Languages XXII, 624 p. 69 illus., Hardcover, 2008
    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.
    close
    close
  • Reisig, Wolfgang
    Towards a Theory of Services
    In Information Systems and e-Business Technologies, 2nd International United Information Systems Conference, UNISCON 2008, Springer-Verlag, Klagenfurt, Austria, apr 2008
    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.
    close
    close
  • Reisig, Wolfgang
    The computable kernel of Abstract State Machines
    volume 409 of Theoretical Computer Science 409, aug 2008
    Abstract State Machines (ASMs) were introduced as "a computation model that is more powerful and more universal than standard computation models", by Yuri Gurevich in 1985. ASMs gained much attention as a specification method. It is extremely flexible because any mathematical structure may serve as a state. Gurevich characterized the expressive power of ASMs in terms of intuitively convincing postulates. The core result of this paper shows that the next-state function M of an Abstract State Machine M can be described on a symbolic level, notwithstanding the generality of the model: The successor state M(S) of a state S is fully specified by the equivalence ~s induced by S on the terms over the signature of M. Consequently, M(S) is computable in case ~s is decidable. Furthermore, this result implies a notion of computability for general structures, e.g. for algorithms operating on real numbers.
    close
    close
  • Reisig, Wolfgang
    The Scholten/Dijkstra Pebble Game Played Straightly, Distributely, Online and Reversed
    volume 4800 of Pillars of Computer Science, LNCS 4800, Springer-Verlag, 2008
    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.
    close
    close
  • Lohmann, Niels, Kopp, Oliver, Leymann, Frank, Reisig, Wolfgang
    Analyzing BPEL4Chor: Verification and Participant Synthesis
    In Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, Springer-Verlag, 2008
    Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.
    close
    close
  • 2007

  • Reisig, Wolfgang, Bretschneider, Jan, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Services as a Paradigm of Computation
    In Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj\orner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, Springer-Verlag, sep 2007
    The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.
    close
    close
  • Hohberg, Bodo, Reisig, Wolfgang, Wu, Bixia
    Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2007
    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.
    close
    close
  • Reisig, Wolfgang, Wolf, Karsten, Bretschneider, Jan, Kaschner, Kathrin, Lohmann, Niels, Massuthe, Peter, Stahl, Christian
    Challenges in a Service-Oriented World
    volume 70 of ERCIM News 70, jul 2007
    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.
    close
    close
  • Glausch, Andreas, Reisig, Wolfgang
    A Semantic Characterization of Unbounded-Nondeterministic ASMs
    In Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science, volume 4624 of Lecture Notes in Computer Science, aug 2007
    Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs.
    close
    close
  • Glausch, Andreas, Reisig, Wolfgang
    An ASM-Characterization of a Class of Distributed Algorithms
    In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, Springer, 2007
    close
  • Reisig, Wolfgang
    The Decent Philosophers: An Exercise in Concurrent Behaviour
    volume 80 of Fundamenta Informaticae 80 (1-3), nov 2007
    Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.
    close
    close
  • 2006

  • Glausch, Andreas, Reisig, Wolfgang
    Distributed Abstract State Machines and Their Expressive Power
    Informatik-Berichte, Humboldt-Universität zu Berlin, jan 2006
    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.
    close
    close
  • Reisig, Wolfgang, Fahland, Dirk, Lohmann, Niels, Massuthe, Peter, Stahl, Christian, Weinberg, Daniela, Wolf, Karsten, Kaschner, Kathrin
    Analysis Techniques for Service Models
    In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, IEEE Computer Society, nov 2006
    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.
    close
    close
  • Glausch, Andreas, Reisig, Wolfgang
    How Expressive are Petri Net Schemata?
    In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
    Petri net schemata are an intuitive and expressive approach to describe high-level Petri nets. A Petri net schema is a Petri net with edges and transitions inscribed by terms and Boolean expressions, respectively. A concrete high-level net is gained by interpreting the symbols in the inscriptions by a structure. Its semantics can then be described in terms of a transition system. Therefore, the semantics of a Petri Net schema can be conceived as a family of transition systems indexed by structures. In this paper we characterize the expressive power of a general version of Petri net schemata. For that purpose we examine families of transition systems in general and characterize the families as generated by Petri net schemata. It turns out that these families of transition systems can be characterized by simple and intuitive requirements.
    close
    close
  • Acu, Baver, Reisig, Wolfgang
    Compensation in Workflow Nets
    In Petri Nets and Other Models of Concurrency - ICATPN 2006, 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, Turku, Finland, June 26-30, 2006, Proceedings, volume 4024 of Lecture Notes in Computer Science, Springer, 2006
    close
  • Brauer, Wilfried, Reisig, Wolfgang
    Carl Adam Petri und die ``Petrinetze''
    volume 29 of Informatik-Spektrum 29 (5), oct 2006
    close
  • Glausch, Andreas, Reisig, Wolfgang
    On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines
    Informatik-Berichte, Humboldt-Universität zu Berlin, dec 2006
    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.
    close
    close
  • 2005

  • Reisig, Wolfgang
    Modeling- and Analysis Techniques for Web Services and Business Processes
    In Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings, volume 3535 of Lecture Notes in Computer Science, Springer Verlag, may 2005
    Open distributed systems include in particular Web services and business processes. There is a need of techniques to model such systems formally, and to derive decisive properties from such models. Three such techniques are presented in this paper, exemplified by help of realistic examples, and mutually related w.r.t. their respective expressive power and the availability of analysis techniques.
    close
    close
  • Reisig, Wolfgang
    On the Expressive Power of Petri Net Schemata
    In Applications and Theory of Petri Nets 2005: 26th International Conference, ICATPN 2005, Miami, USA, June 20-25, 2005. Proceedings, volume 3536 of Lecture Notes in Computer Science, Springer Verlag, may 2005
    High-level Petri nets are frequently represented as Petri net schemas, with places, transitions and arcs inscribed by terms. A concrete system is then gained by interpreting the symbols in those terms. The behavior of a concrete system is a transition system. The composition of all those transition systems represents the behavior of the Petri net schema. This paper characterizes the expressive power of (a basic class of) Petri net schemas. It turns out that quite simple as well as quite general requirements at a transition system suffice to generate it by such a Petri net schema.
    close
    close
  • Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
    Hazard Detection in a GALS Wrapper: A Case Study
    In Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD'05), IEEE Computer Society, St. Malo, France, jun 2005
    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.
    close
    close
  • Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
    Kommunizierende Workflow-Services modellieren und analysieren
    Informatik - Forschung und Entwicklung, Springer-Verlag, oct 2005
    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.
    close
    close
  • Fahland, Dirk, Reisig, Wolfgang
    ASM-based semantics for BPEL: The negative Control Flow
    In Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), Paris XII, mar 2005
    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.
    close
    close
  • Stahl, Christian, Reisig, Wolfgang, Krstic, Milos
    Hazard Detection in a GALS Wrapper: a Case study
    Informatik-Berichte, Humboldt-Universität zu Berlin, feb 2005
    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.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2005
    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.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    In 2nd South-East European Workshop on Formal Methods 2005 (SEEFM05), Ohrid, Republic of Macedonia, 2005
    close
  • Reisig, Wolfgang
    Modeling- and Analysis Techniques for Web Services and Business Processes
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2005
    close
  • Reisig, Wolfgang, Schmidt, Karsten, Stahl, Christian
    Verteilte Geschäftsprozesse modellieren und analysieren
    Informatik-Berichte, Humboldt-Universität zu Berlin, feb 2005
    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.
    close
    close
  • Massuthe, Peter, Reisig, Wolfgang, Schmidt, Karsten
    An Operating Guideline Approach to the SOA
    volume 1 of Annals of Mathematics, Computing \& Teleinformatics 1 (3), 2005
    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.
    close
    close
  • 2004

  • Alexander, Adrianna, Reisig, Wolfgang
    Compositional Temporal Logic Based on Partial Order
    Informatik-Berichte, Humboldt-Universität zu Berlin, dec 2004
    close
  • Reisig, Wolfgang, Brade, A.
    ASM Models for Web Services
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2004
    close
  • Reisig, Wolfgang
    The computable kernel of Sequential Abstract State Machines
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2004
    close
  • Alexander, Adrianna, Reisig, Wolfgang
    Compositional Temporal Logic Based on Partial Order
    In 11th International Symposium on Temporal Representation and Reasoning (TIME'04), IEEE Computer Society, 2004
    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.
    close
    close
  • 2003

  • Alexander, Adrianna, Reisig, Wolfgang
    Logic of Involved Variables - System Specification with Temporal Logic of Distributed Actions
    In Proc. of the 3rd International Conference on Application of Concurrency to System Design (ACSD'03), Guimaraes, Portugal , IEEE Computer Society, jun 2003
    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.
    close
    close
  • Weber, Herbert, Ehrig, Hartmut, Reisig, Wolfgang, Borusan, Alexander, Lembke, Sabine, Dehnert, Juliane, Weber, Michael, Martens, Axel, Padberg, Julia, Ermel, Claudia, Qemali, A.
    The Petri Net Baukasten of the DFG Forschergruppe PETRI NET TECHNOLOGY
    In Petri Net Technology for Communication-Based Systems, volume 2472 of Lecture Notes in Computer Science, Springer-Verlag, 2003
    In the long history of Petri nets a universe of Petri nets has evolved consisting of an enormously rich theory, a wide variety of tools, and numerous successful applications and case studies in various application domains. This vast variety is not any more handable for anyone working with Petri nets, which results in the strong need of a structured access to Petri nets. This structured access has been the main aim of the DFG-Forschergruppe PETRI NET TECHNOLOGY, which has developed the so-called Petri Net Baukasten for this purpose. It is designed to support Petri net experts, application developers and tool developers alike in their specific work with Petri nets. This paper presents an overview of the concepts, initial and 2nd installment of the Petri Net Baukasten, which have been presented at the 1st and 2nd International Colloquium on Petri Net Technologies for Modelling Communication Based Systems in 1999 and 2001, respectively.
    close
    close
  • Reisig, Wolfgang
    The Computable Kernel of ASM
    In Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Taormina, Italy, volume 2589 of Lecture Notes in Computer Science, 2003
    A rich variety of system models for sequential, deterministic systems has been suggested during recent decades, including automata, process algebras, many versions of Petri Nets, and models to describe the semantics of Programming languages. All models for sequential, deterministic systems assume a set S of states, or configurations, and a next state function $\upsilon: S \rightarrow S$.
    close
    close
  • Reisig, Wolfgang
    The Expressive Power of Abstract State Machines
    volume 22 of Computing and Informatics 22 (3), 2003
    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.
    close
    close
  • Reisig, Wolfgang
    On Gurevich's Theorem on Sequential Algorithms
    volume 39 of Acta Informatica 39 (5), Springer-Verlag, 2003
    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.
    close
    close
  • 2002

  • Reisig, Wolfgang
    Teleteaching-Vorlesung 'Verteilte Systeme: Formale Methoden - Anwendungen - Werkzeuge'
    In Informatik bewegt: Informatik 2002 - 32. Jahrestagung der Gesellschaft für Informatik e.v. (GI), volume 19 of LNI, GI, 2002
    close
  • 2001

  • Reisig, Wolfgang
    Modelling of learning process, using methodology of System Petri Nets
    In Tagungsband der International Scientific Conference MANAGEMENT INFORMATION SYSTEMS, Tibilisi, jun 2001
    close
  • 2000

  • Reisig, Wolfgang
    The Linear Theory of Multiset Based Dynamic Systems
    In Workshop on Multiset Processing (WMP 2000), volume 2235 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Reisig, Wolfgang
    Towards an ASM Thesis for Unconventional Algorithms
    In Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich's ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.
    close
    close
  • Kindler, Ekkart, Martens, Axel, Reisig, Wolfgang
    Inter-operability of Workshop Applications - Local Criteria for Global Soundness
    In Business Process Management, volume 1806 of Lecture Notes in Computer Science, Springer-Verlag, 2000
    close
  • Foremniak, Adrianna, Reisig, Wolfgang
    A Temporal Logic of Distributed Actions (TLDA)
    Informatik-Berichte, Humboldt-Universität zu Berlin, 2000
    close
  • 1999

  • Battke, Anne, Borusan, Alexander, Dehnert, Juliane, Ehrig, Hartmut, Ermel, Claudia, Gajewsky, Maike, Hoffmann, Kathrin, Hohberg, Bodo, Juhás, Gabriel, Lembke, Sabine, Martens, Axel, Padberg, Julia, Reisig, Wolfgang, Vesper, Tobias, Weber, Herbert, Weber, Michael
    Petrinetz-Technologie: Initial Realization of the Petri Net Baukasten
    Informatik-Berichte, Humboldt-Universität zu Berlin, oct 1999
    close
  • 1998

  • Reisig, Wolfgang
    On the structure of DNA Algorithm
    Informatik-Berichte, Humboldt-Universität zu Berlin, dec 1998
    close
  • Desel, Jörg, Reisig, Wolfgang
    Place/Transition Petri Nets.
    In Petri Nets, nov 1998
    close
  • Reisig, Wolfgang
    Distributed Algorithms: Modeling and Analysis with Petri Nets
    In Systems, Man, and Cybernetics, 1998. 1998 IEEE International Conference on, volume 1 of oct 1998
    close
  • Reisig, Wolfgang
    Elements Of Distributed Algorithms: Modeling and Analysis with Petri Nets
    Springer-Verlag, sep 1998
    close
  • 1997

  • Ehrig, Hartmut, Reisig, Wolfgang
    An Algebraic View on Petri Nets.
    volume 61 of Bulletin of the EATCS 61, feb 1997
    close
  • Weber, Michael, Walter, Rolf, Völzer, Hagen, Vesper, Tobias, Reisig, Wolfgang, Peuker, Sibylle, Kindler, Ekkart, Freiheit, Jörn, Desel, Jörg
    DAWN: Petrinetzmodelle zur Verifikation Verteilter Algorithmen
    Informatik-Berichte, Humboldt-Universität zu Berlin, dec 1997
    close
  • Reisig, Wolfgang
    Verteilte Algorithmen: Nutzen sie der Forschergruppe?
    1997
    close
  • Reisig, Wolfgang
    Interleaved progress, concurrent progress, and local progress
    In Proceedings of the DIMACS workshop on Partial order methods in verification (POMIV '96), volume 29 of AMS Press, Inc., New York, NY, USA, 1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang, Völzer, Hagen, Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    volume 9 of Formal Aspects of Computing 9 (4), Springer-Verlag, 1997
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Verification of Distributed Algorithms with Algebraic Petri Nets
    In Foundations of Computer Science: Potential - Theory - Cognition, volume 1337 of Lecture Notes in Computer Science, Springer-Verlag, 1997
    close
  • 1996

  • Walter, Rolf, Völzer, Hagen, Vesper, Tobias, Reisig, Wolfgang, Kindler, Ekkart, Freiheit, Jörn, Desel, Jörg
    Memorandum: Petrinetzmodelle zur Verifikation verteilter Algorithmen
    Informatik-Berichte, Humboldt-Universität zu Berlin, aug 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang
    Algebraic System Nets for Modelling Distributed Algorithms
    volume 51 of Petri Net Newsletter 51, nov 1996
    close
  • Ehrig, Hartmut, Reisig, Wolfgang, Weber, Herbert
    Kick-Off-Workshop der DFG-Forschergruppe 'Petrinetz-Technologie'
    Informatik-Berichte, Humboldt-Universität zu Berlin, dec 1996
    close
  • Reisig, Wolfgang
    Temporallogische Verifikation verteilter Algortihmen: Mehr als nur eine Variante
    In Formal Methods for Concurrency, GI-Kolloquium, Fachberichte der TU Dresden, Technische Universität Dresden, jul 1996
    close
  • Kindler, Ekkart, Reisig, Wolfgang, Völzer, Hagen, Walter, Rolf
    Petri Net Based Verification of Distributed Algorithms: An Example
    Informatik-Berichte, Humboldt-Universität zu Berlin, may 1996
    close
  • Reisig, Wolfgang
    Modelling and Verification of Distributed Algorithms
    In CONCUR 96, volume 1119 of Lecture Notes in Computer Science, Springer-Verlag, 1996
    close
  • Reisig, Wolfgang, Kindler, Ekkart, Vesper, Tobias, Völzer, Hagen, Walter, Rolf
    Distributed Algorithms for Networks of Agents.
    In Petri Nets (2), 1996
    close
  • Reisig, Wolfgang, Rozenberg, Grzegorz
    Informal Introduction to Petri Nets
    In Petri Nets, 1996
    close
  • Desel, Jörg, Reisig, Wolfgang
    The Synthesis Problem of Petri Nets.
    volume 33 of Acta Informatica 33 (4), 1996
    close
  • 1995

  • Reisig, Wolfgang
    Petri Net Models of Distributed Algorithms.
    In Computer Science Today, 1995
    close
  • 1994

  • Reisig, Wolfgang
    Correctness Proofs of Distributed Algorithms.
    In Dagstuhl Seminar on Distributed Systems, 1994
    close
  • Reisig, Wolfgang
    Petri-Netze und ihre Anwendungen
    In Integrierte Informationsverarbeitung in Büro, Produktion und Logistik, VDI Reihe 10: Informatik / Kommunikationstechnik, VDI-Verlag, Düsseldorf, 1994
    close
  • Reisig, Wolfgang
    Progress in Petrinets
    Informatik-Berichte, Humboldt-Universität zu Berlin, 1994
    close
  • Reisig, Wolfgang
    Verteiltes Rechnen: Im wesentlichen das Herkömmliche oder etwas grundlegend Neues?
    Öffentliche Vorlesungen, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099 Berlin, Germany, 1994
    close
  • 1993

  • Reisig, Wolfgang
    Formal methods for concurrent systems design: a survey
    In Programming Models for Massively Parallel Computers, 1993. Proceedings, IEEE, sep 1993
    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.
    close
    close
  • Reisig, Wolfgang
    Spezifikation, Modellierung und Korrektheit von Informationssystemen
    In Petrinetze im Einsatz für Entwurf und Entwicklung von Informationssystemen, Springer, 1993
    close
  • Desel, Jörg, Reisig, Wolfgang
    The Synthesis Problem of Petri Nets.
    In STACS, SFB-Bericht, 1993
    close
  • 1992

  • Reisig, Wolfgang
    Elements of a Temporal Logic Coping with Concurrency
    SFB-Bericht, Technische Universität München, 1992
    close
  • Reisig, Wolfgang
    Report on the REX Workshop on Semantics-Foundations and Applications
    volume 84 of Bulletin of the EATCS 84, 1992
    close
  • Reisig, Wolfgang
    Combining Petri Nets and Other Formal Methods
    In Application and Theory of Petri Nets, 1992
    close
  • Reisig, Wolfgang
    A Primer in Petri Net Design
    Springer Compass International, 1992
    close
  • 1991

  • Reisig, Wolfgang
    Petri Nets and Algebraic Specifications
    volume 80 of Theor. Comput. Sci. 80 (1), 1991
    close
  • Reisig, Wolfgang
    Parallel Composition of Liveness
    SFB-Bericht, Technische Universität München, 1991
    close
  • Reisig, Wolfgang
    Concurrent Temporal Logic
    SFB-Bericht, Technische Universität München, 1991
    close
  • 1990

  • Reisig, Wolfgang
    Petrinetze: Grundfragen, Konzepte, Konsequenzen
    Arbeitspapiere der GMD, 1990
    close
  • Plünnecke, Helmut, Reisig, Wolfgang
    Bibliography on Petri nets 1990.
    In Applications and Theory of Petri Nets, 1990
    close
  • 1989

  • Reisig, Wolfgang
    The decent philosophers: An exercise in operational semantics of concurrent systems
    In 25 Jaar Semantiek-Liber Amicorum, CWI, Amsterdamm, 1989
    close
  • 1988

  • Reisig, Wolfgang
    Towards a temporal logic of causality and choice in distributed systems
    In REX Workshop, 1988
    close
  • Reisig, Wolfgang
    Concurrency is more fundamental than interleaving
    volume 35 of Bulletin of the EATCS 35, 1988
    close
  • Reisig, Wolfgang
    Temporal Logic and Causality in Concurrent Systems.
    In Concurrency, 1988
    close
  • 1987

  • Smith, E., Reisig, Wolfgang
    The Semantics of a Net is a Net: An Exercise in General Net Theory
    Concurrency and Nets - Advances in Petri Nets, Springer-Verlag, Berlin, 1987
    close
  • Reisig, Wolfgang
    Das Verhalten verteilter Systeme
    GMD-Bericht, Oldenbourg Berichte der GMD, München, 1987
    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''.
    close
    close
  • Reisig, Wolfgang
    Towards a Temporal Logic for True Concurrency. Part I: Linear Time Propositional Logic
    Arbeitspapiere der GMD, Gesellschaft für Mathematik und Datenverarbeitung mbH, Sankt Augustin, Arbeitspapiere der GMD, 1987
    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.
    close
    close
  • Reisig, Wolfgang, Vautherin, J.
    An Algebraic Approach to High Level Petri Nets
    In Proceedings of the Eighth European Workshop on Application and Theory of Petri Nets, Universidad de Zaragoza, Spain, 1987
    close
  • 1986

  • Reisig, Wolfgang
    Embedded System Description Using Petri Nets
    In Embedded Systems, 1986
    close
  • Reisig, Wolfgang
    Anforderungsbeschreibung und Systementwurf mit Petri-Netzen.
    Handbuch der modernen Datenverarbeitung, Heft 130: Formale Methoden in der Systementwicklung, Forkel-Verlag, jul 1986
    close
  • Reisig, Wolfgang
    A strong part of concurrency.
    In European Workshop on Applications and Theory of Petri Nets, 1986
    close
  • Reisig, Wolfgang
    Petri Nets in Software Engineering
    In Advances in Petri Nets, 1986
    close
  • Reisig, Wolfgang
    Place/Transition Systems
    In Advances in Petri Nets, 1986
    close
  • Drees, Stefan, Gomm, Dominik, Plünnecke, Helmut, Reisig, Wolfgang, Walter, Rolf
    Bibliography of Petri nets
    In European Workshop on Applications and Theory of Petri Nets, 1986
    close
  • 1985

  • Reisig, Wolfgang
    Petri Nets with Individual Tokens
    volume 41 of Theoretical Computer Science 41, 1985
    close
  • Reisig, Wolfgang
    On the Semantics of Petri Nets.
    Formal Models in Programming, IFIP 1985, North-Holland, Elsevier Science Publishers B. V., 1985
    close
  • Reisig, Wolfgang
    Systementwurf mit Netzen
    Springer, 1985
    close
  • 1984

  • Reisig, Wolfgang
    On the Semantics of Petri Nets.
    Univ. Hamburg, Fachbereich Informatik, Bericht Nr. 100, sep 1984
    close
  • Reisig, Wolfgang
    What Operational Semantics is Adequate for Nonsequential Systems?
    Research Report, Tech. Univ. of Helsinki, Digital Systems Laboratory, Research, 1984
    close
  • Reisig, Wolfgang
    Partial Order Semantics versus Interleaving Semantics for CSP-like Languages and its Impact on Fairness.
    In ICALP, 1984
    close
  • Herzog, Otthein, Reisig, Wolfgang, Valk, Rüdiger
    Petri-Netze: ein Abri\ss ihrer Grundlagen und Anwendungen.
    volume 7 of Informatik Spektrum 7 (1), 1984
    close
  • Goltz, Ursula, Reisig, Wolfgang
    CSP-programs with individual tokens.
    In European Workshop on Applications and Theory in Petri Nets, 1984
    close
  • 1983

  • Reisig, Wolfgang
    System Design Using Petri Nets
    In Requirements Engineering, 1983
    close
  • Goltz, Ursula, Reisig, Wolfgang
    Processes of Place/Transition-Nets
    In ICALP, 1983
    close
  • Goltz, Ursula, Reisig, Wolfgang
    The Non-sequential Behavior of Petri Nets
    volume 57 of Information and Control 57 (2/3), 1983
    close
  • Berthelot, G., Memmi, G., Reisig, Wolfgang
    A Control Structure for Sequential Processes Synchronized by Buffers
    In 4th Workshop on Theory and Applications of Petri Nets, Toulouse, September 1983, 1983
    close
  • 1982

  • Reisig, Wolfgang
    Petri Nets with Individual Tokens
    In European Workshop on Applications and Theory of Petri Nets, 1982
    close
  • Reisig, Wolfgang
    Deterministic Buffer Synchronization of Sequential Processes
    volume 18 of Acta Informatica 18, 1982
    close
  • Reisig, Wolfgang
    Petrinetze, Eine Einführung
    Springer, 1982
    close
  • 1981

  • Reisig, Wolfgang
    Recursive Nets
    In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
    close
  • Goltz, Ursula, Reisig, Wolfgang, Thiagarajan, P. S.
    Two Alterative Definitions of Synchronic Distance
    In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
    close
  • Goltz, Ursula, Reisig, Wolfgang
    Weighted Synchronic Distances.
    In Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, 1981
    close
  • 1980

  • Reisig, Wolfgang
    A Graph Grammar Representation of Non-Sequential Processes
    In WG, 1980
    close
  • Reisig, Wolfgang
    Schemes for Nonsequential Processing Systems.
    In MFCS, 1980
    close
  • 1979

  • Reisig, Wolfgang
    On a Class of Co-Operating Sequential Processors.
    In Proc. of the 1st European Conference on Parallel and Distributed Processing, Cepadues Editions, Toulouse, 1979
    close
  • Reisig, Wolfgang
    A Note on the Representation of Finite Tree Automata
    volume 8 of Information Processing Letters 8 (5), 1979
    close
  • Reisig, Wolfgang
    Zur Verwendung von Petrinetz-Morphismen bei der Systemkonstruktion.
    Informatik-Fachberichte 21: Formale Modelle für Informationssysteme, Fachtagung der GI, Tutzing 1979, Springer-Verlag, Berlin, Heidelberg, New York, 1979
    close
  • Reisig, Wolfgang
    On Solving Conflicts in Petri Nets. Workshop on Graph Theoretical Concepts in Computer Science, Berlin 1979
    Discrete Structures and Algorithms, Hanser Verlag, 1979
    close
  • Reisig, Wolfgang
    Untersuchungen einer Klasse kooperierender sequentieller Prozesse mit Hilfe von Petri-Netzen
    Dissertation, 1979
    close
  • 1977

  • Reisig, Wolfgang
    Interactive Schemes
    In Parallel Computers - Parallel Mathematics, Proc. of the IMACS-GI-Symp., March 14--16, 1977, Munich, North-Holland Publishing Company, Amsterdam, 1977
    close
  • 1975

  • Reisig, Wolfgang
    Eine Verallgemeinerung des Berechenbarkeitsbegriffes durch Gleichungssysteme
    Interner Bericht, Institut für Informatik der Universität Bonn, 1975
    close
  • 1974

  • Indermark, K., Reisig, Wolfgang
    On Recursively Definable Relations
    In Report on the 14th Lattice Theory Conference, Szeged, Hungary, 1974, 1974
    close