I N T ERMS OF N ETS
SYSTEM DESIGN
WITH
P ETRI NETS
AND
P ROCESS ALGEBRA
T WAN BASTEN
Copyright ?1998 by Antonius Andr? Basten, Eindhoven, The Netherlands. e
All rights reserved. No part of this publication may be stored in a retrieval system, transmitted, or reproduced, in any form or by any means, including but not limited to photocopy, photograph, magnetic or other record, without prior agreement and written permission of the author.
CIP-DATA LIBRARY TECHNISCHE UNIVERSITEIT EINDHOVEN Basten, Antonius Andr? e In terms of nets : system design with Petri nets and process algebra / by Antonius Andr? Basten. - Eindhoven : e Eindhoven University of Technology, 1998. -x, 237 p. Proefschrift. - ISBN 90-386-0631-1 NUGI 852 Subject headings: Petri nets / process algebra / object oriented modelling / software description ; program veri?cation CR Subject Classi?cation (1998): D.2.2, D.2.4, F.3, D.1.3, D.1.5, D.3.3
The work in this thesis has been carried out under the auspices of the research school IPA (Institute for Programming research and Algorithmics). IPA Dissertation Series 1998-05 Printed by University Press Facilities, Eindhoven Cover Design by Ben Mobach
I N T ERMS OF N ETS
SYSTEM DESIGN
WITH
P ETRI NETS
AND
P ROCESS ALGEBRA
PROEFSCHRIFT
TER VERKRIJGING VAN DE GRAAD VAN DOCTOR AAN DE
TECHNISCHE U NIVERSITEIT EINDHOVEN , OP GEZAG VAN DE R ECTOR M AGNIFICUS , PROF. DR . M. R EM , VOOR EEN COMMISSIE AANGEWEZEN DOOR HET C OLLEGE VOOR P ROMOTIES IN HET OPENBAAR TE VERDEDIGEN OP DONDERDAG 3 DECEMBER 1998 OM 16.00 UUR
DOOR
? ANTONIUS ANDR E BASTEN
GEBOREN TE
S EVENUM
Dit proefschrift is goedgekeurd door de promotoren: prof.dr. J.C.M. Baeten prof.dr. K.M. van Hee
“ ‘What a shame,’ Kalten sighed. ‘So many good ideas have to be discarded simply because they won’t work.’ ” The Sapphire Rose, David Eddings
Preface
When I applied for a Ph.D. position almost ?ve years ago, I thought that I knew what it meant to be doing research. I also thought that I understood what it meant to be working towards a Ph.D. thesis. However, research is harder than I expected and successfully completing a Ph.D. thesis is even more dif?cult than doing research. As a Ph.D. student, I started working in the Formal Methods group of Jos Baeten and the Information Systems group of Kees van Hee. Jos and Kees wanted to ?nd out whether their favorite formalisms for describing and analyzing concurrent systems, namely process algebra and Petri nets, could be integrated. At the time, several members of both groups were interested in this topic. Thus, I had a very good start in my ?rst year. The results that I obtained during that year form the basis of Chapter 3 of this thesis. Unfortunately, as any Ph.D. student experiences sooner or later, the good times did not last. Jos became Dean of the Faculty of Mathematics and Computing Science and Kees went to Bakkenist Management Consultants. In addition, the faculty had to cut back costs and was being reorganized. The atmosphere was spoiled and the interest in the topic of my research diminished. At that time, I had serious doubts whether I made the right choice to become a Ph.D. student. However, times changed, the reorganization was ?nished, and I found a new interesting topic to work on. In a few months time, I developed the theory which forms the core of Chapter 4. The next dif?cult step was to start writing my thesis. I did not like the idea that I had to redo the work of the ?rst three years yet another time. I had already written down all results several times in the form of reports and papers. I felt the work was ?nished. However, once I had written the ?rst sections of my thesis, I realized that there were still several interesting aspects of my research that were not yet completely clear. My enthusiasm returned and I worked longer and longer hours. But then something happened that changed my entire life. Due to the many hours I spent behind the keyboard, the muscles and nerves in my arms were damaged, to the point that I could no longer type, write, or lift anything. I had to stop working on my thesis, which ultimately led to a delay of almost nine months. However, with the support of colleagues, family, and friends, I worked myself back into life. The fact that, today, my thesis is ?nished is one of the signs that I have succeeded. As may be clear from the above paragraphs, this thesis would not have been the same without the help and support of many people. First of all, I would like to thank my promotors Jos Baeten and Kees van Hee. From vii
viii
Preface
Jos, I learned many things that are useful when working in a scienti?c environment. Kees, with his questions and criticism, made sure that I stayed in touch with practice. Second, I am grateful to Marc Voorhoeve and Wil van der Aalst. My cooperation with Marc and Wil provided the basis for Chapters 3 and 4 of this thesis. I would like to thank Marc for always believing in my research, even when I did not. I want to thank Eike Best and Gregor Engels for evaluating my thesis as members of the reading committee. I thank Wil van der Aalst, Paul De Bra, Jan Friso Groote, Martin Rem, and Marc Voorhoeve for their willingness to participate in the graduation committee. Several colleagues and friends commented on various drafts of this thesis or parts of it: Jos Baeten, Eike Best, Gregor Engels, Reiko Heckel, Kees van Hee, Isabelle Reymen, Bram Stappers, Eric Verbeek, and Marc Voorhoeve. I am grateful for their effort. Their suggestions helped to improve the readability and technical presentation of this thesis. I would like to thank Bram Stappers for writing a script to format the index. Eric Verbeek provided me with the Petri net of Figure 4.3.49 on Page 195 and showed me that the original example was incorrect. I am indebted to Dragon Systems for developing the speech recognition software that I used to complete this thesis. The successful completion of a Ph.D. thesis requires a lot of hard work. However, one other aspect is at least as important: I would like to thank my family and close friends for their enthusiasm and interest in good times and their care and support in dif?cult times. I thank Bram for having to live with me when I was too busy writing my thesis. I am grateful to Karel and Balkie for the pleasant atmosphere they created at De Koppele. I want to thank Bram, Eric, Marielle, Eveline, Chiel, Marcel, Gabri¨ lle, Patricia, and e Yves for helping me with all those things that I can no longer do myself. I am grateful to my parents, Theo and Marga, for always being there when I need them. Their education gave me the attitude and the sense of responsibility that is needed to earn the doctoral degree. Finally, I would like to say thanks to Isabelle for her love and support. There are so many things she did for me that it is impossible to mention them all. Therefore, I’ll keep it simple: Thank you, Isabelle! Twan Basten Eindhoven, October 2, 1998
“Life is what happens to you while you’re busy making other plans.” John Lennon
Contents
Preface 1 2 Introduction Basic Concurrency Theory 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Process Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2.1 Operational semantics . . . . . . . . . . . . . . . . . . . 2.2.2 Strong bisimilarity . . . . . . . . . . . . . . . . . . . . . 2.2.3 Branching bisimilarity . . . . . . . . . . . . . . . . . . . 2.3 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3.1 Notations for bags . . . . . . . . . . . . . . . . . . . . . 2.3.2 Labeled Place/Transition nets . . . . . . . . . . . . . . . 2.3.3 Analysis of labeled P/T nets . . . . . . . . . . . . . . . . 2.3.4 Other classes of P/T nets . . . . . . . . . . . . . . . . . . 2.3.5 Analysis of free-choice P/T nets . . . . . . . . . . . . . . 2.4 Process Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . 2.4.1 Basic Process Algebra . . . . . . . . . . . . . . . . . . . 2.4.2 Basic Process Algebra with inaction . . . . . . . . . . . . 2.4.3 Process Algebra with inaction and renaming . . . . . . . . 2.4.4 Process Algebra with inaction, silent actions, and renaming 2.4.5 Iteration in process algebra . . . . . . . . . . . . . . . . 2.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . Algebraic Veri?cation of Modular Nets 3.1 Introduction . . . . . . . . . . . . . . . . . 3.2 Design Method . . . . . . . . . . . . . . . . 3.3 P/T-Net Components . . . . . . . . . . . . . 3.4 Algebraic Semantics for P/T-Net Components 3.4.1 Glass-box semantics . . . . . . . . . 3.4.2 Black-box semantics . . . . . . . . . 3.5 Modular P/T Nets . . . . . . . . . . . . . . 3.6 Algebraic Semantics for Modular P/T Nets . 3.6.1 Glass-box semantics . . . . . . . . . ix . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii 1 5 5 5 5 8 10 15 16 17 20 26 28 33 34 38 40 47 51 57 59 59 60 62 65 65 71 75 82 83
3
x 3.6.2 System semantics . . . . . . . . . . . . . . . . 3.6.3 Black-box semantics . . . . . . . . . . . . . . . Case Study: The Alternating-Bit Protocol . . . . . . . . 3.7.1 Introduction . . . . . . . . . . . . . . . . . . . 3.7.2 A modular P/T net of the ABP . . . . . . . . . . 3.7.3 Verifying the modular P/T net . . . . . . . . . . 3.7.4 The P/T-net components of the modular net . . . 3.7.5 Verifying the P/T-net components . . . . . . . . 3.7.6 A remark on the equivalence of modular P/T nets Case Study: The Production Unit . . . . . . . . . . . . 3.8.1 Introduction . . . . . . . . . . . . . . . . . . . 3.8.2 The basic production unit . . . . . . . . . . . . 3.8.3 Complex production units . . . . . . . . . . . . Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Contents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 87 88 88 90 94 105 108 110 111 111 112 121 137 143 143 145 145 155 159 159 165 171 197 197 198 199 201 203 207 209 211 219 229 231 233
3.7
3.8
3.9 4
Inheritance of Dynamic Behavior 4.1 Introduction . . . . . . . . . . . . . . . . . . . . 4.2 A Process-Algebraic Approach . . . . . . . . . . 4.2.1 Object life cycles and inheritance relations 4.2.2 Axioms of inheritance . . . . . . . . . . . 4.3 A Petri-Net-Based Approach . . . . . . . . . . . . 4.3.1 Object life cycles . . . . . . . . . . . . . 4.3.2 Inheritance relations . . . . . . . . . . . . 4.3.3 Transformation rules . . . . . . . . . . . . 4.4 Case Study: A Groupware Editor . . . . . . . . . 4.4.1 Introduction . . . . . . . . . . . . . . . . 4.4.2 The multi-user viewer . . . . . . . . . . . 4.4.3 The multi-user editor . . . . . . . . . . . . 4.4.4 The groupware editor . . . . . . . . . . . 4.5 Conclusions . . . . . . . . . . . . . . . . . . . . Concluding Remarks
5
A List of Axioms Bibliography Index Summary Samenvatting (Dutch Summary) Curriculum Vitae
1
Introduction
“The term “formal methods” denotes software development and analysis activities that entail a degree of mathematical rigor. ( ... ) A formal method manipulates a precise mathematical description of a software system for the purpose of establishing that the system does or does not exhibit some property, which is itself precisely de?ned.” (D ILLON AND S ANKAR, 1997)
Motivation. To date, many different formal methods exist to support the development of complex software and hardware systems. Each of these methods builds upon a mathematical formalism to describe and analyze the system under consideration. The motivation for the development of a formal method varies widely. Often a method is developed for a speci?c application domain. Sometimes methods are based on certain proof techniques. Other formal methods are geared towards the veri?cation of a speci?c class of properties of systems. Yet other methods are speci?cally developed to facilitate automated tool support. In a few occasions, mathematical elegance is the main motivation. The result is a wide variety of formal methods and accompanying mathematical formalisms for describing complex systems, each with their own strengths and weaknesses. Despite the large number of formal methods existing to date, new methods are still being developed on a regular basis. Often, the question arises whether it is worth the effort. There is still much that can be improved on and learned from existing methods and formalisms for developing complex systems. It is particularly fruitful to study combinations of several methods or formalisms with different characteristics and complementary strengths. Such studies may lead to improved and more complete methods and formalisms, as well as a better conceptual understanding of the methods and formalisms, their strengths, and their weaknesses. This thesis studies the combination of two formalisms for reasoning about complex systems, namely Petri nets and process algebra. Petri nets originate from (P ETRI, 1962), whereas the process algebra considered in this thesis was ?rst described in (B ERGSTRA 1
2
AND
Introduction
K LOP, 1982). Petri nets and process algebra share two important characteristics. First, they both have a precise mathematical de?nition. Second, they are both designed for reasoning about so-called concurrent systems. A concurrent system is a system that exhibits parallelism or distribution, either physically or in its behavior. The most important characteristic of a concurrent system is that it usually consists of multiple components that communicate to exchange information or to synchronize. Very many of the complex systems being developed in current software-engineering practice belong to the class of concurrent systems. Except for the abovementioned two common characteristics, Petri nets and process algebra are entirely different formalisms. Petri nets have an intuitive graphical representation, which is easy to understand for non-experts. A Petri-net model describes both the states and the actions of the system under consideration. There are many analysis techniques available to investigate properties about the states as well as the dynamic behavior of a Petri-net model. Process algebra is a purely symbolic formalism which is particularly well suited for computer manipulation. A process-algebraic description of a system focuses on its dynamic behavior. It usually has no explicit representation of system states. Proof techniques in process algebra are generally aimed at showing the equality of behavioral descriptions. Consequently, process algebra is useful to compare behavioral descriptions of concurrent systems. For example, it is often used to compare a high-level speci?cation of a system and a more detailed description of an implementation of the system. The goal of such a comparison is to verify whether the implementation satis?es the speci?cation. The above observations show that, in several aspects, Petri nets and process algebra are complementary. The goal of this thesis is to study topics combining the strengths of both Petri nets and process algebra. An important objective is to improve the acceptance of formal methods in design practice. Considering current design practice, the most important problem is to cope with the increasing complexity of the systems being developed. Therefore, a lot of effort is put into the development of methods that support modular or component-based design. Important goals of such methods are to structure the design process and to stimulate the reuse of system components during the design process and in future designs. As explained below, the two main topics of this thesis are both inspired by these developments in design practice. To conclude this paragraph, it is useful to explain what is not the aim of this thesis. It is not meant to argue the need for formal methods in the design of complex software and hardware systems. It is also beyond the scope of this thesis to give a detailed overview and comparison of formal methods in general. The interested reader is referred to (B OWEN, 1998), which contains numerous references to literature on these two topics. Overview. The remainder of this thesis is organized as follows. Chapter 2 contains an introduction to basic concurrency theory. It gives a detailed and fairly complete introduction to Petri nets and process algebra, including references to related literature. The chapter is aimed at readers with a basic mathematical knowledge. It is set up in such a
3 way that the thesis is self-contained. Prior knowledge of Petri nets or process algebra is not necessary. Chapter 3 describes the ?rst contribution of this thesis. It combines Petri nets and process algebra into a method supporting compositional design. In this method, Petri nets are used to model system components. Process algebra is used to specify and verify the behavior of these components. The method is compositional in the sense that the behavior of the entire system can be derived from the behavior of its components. The basis for the method is formed by a number of algebraic semantics for the behavior of so-called modular P/T nets. The class of modular P/T nets is a class of Petri nets especially developed to support modular design. The chapter describes two case studies to evaluate the method in practical design situations. The chapter is based on results published earlier in (BASTEN AND VOORHOEVE , 1995a, 1995b). Chapter 4 is devoted to the second topic of this thesis. It describes an approach to support inheritance of dynamic behavior in object-oriented design methods. In such methods, the so-called class construct is used to structure a system design. A class describes a set of objects sharing a common static structure and dynamic behavior. The concept of inheritance is an important means to stimulate the reuse of class descriptions during the design process. However, many object-oriented methods being used in practice lack a precise de?nition of inheritance of dynamic behavior. In Chapter 4, inheritance of dynamic behavior is ?rst studied in a simple process-algebraic setting. The goal is to get a clear understanding of the important concepts. The results are then translated to a framework based on Petri nets. The Petri-net framework is more expressive than the algebraic framework and it is closer to existing object-oriented methods. The chapter also contains a small case study to validate the approach taken to support inheritance of dynamic behavior. The chapter is based on results published earlier in (BASTEN AND VAN DER A ALST, 1996; VAN DER A ALST AND BASTEN, 1997). Chapters 3 and 4 both contain detailed introductions, including a further motivation of the research, and detailed conclusions, including discussions of related work and open problems. Chapter 5 contains some concluding remarks discussing the results of this thesis in the context of system design as sketched in this introductory chapter. Finally, this thesis ends with an overview of algebraic axioms, which is a useful aid in reading algebraic veri?cations, the bibliography, the index, a summary of the thesis, a translation of the summary into Dutch, and a brief curriculum vitae of the author.
2
Basic Concurrency Theory
2.1 Introduction
Two of the most widely used formalisms for describing concurrent systems are Petri nets and process algebra. This chapter provides an introduction to concurrency theory, containing basic de?nitions and results. A concurrent system is assumed to be a collection of processes running in parallel that may communicate with each other to synchronize or to exchange information. Three different formalisms for describing concurrent systems are discussed. First, a general framework of processes is introduced, based on the notion of transition systems. Transition systems can be used to provide different formalisms for describing concurrent systems with a common operational semantics. In this way, it is possible to compare systems described in any such formalism in an unambiguous way. Second, Section 2.3 introduces the formalism of Place/Transition nets, or simply P/T nets. The framework of P/T nets is a basic class of Petri nets which is illustrative for other Petrinet formalisms. Third, in Section 2.4, a few simple process algebras are introduced to illustrate the essentials of a process-algebraic approach to describing concurrent systems. Finally, Section 2.5 contains some concluding remarks.
2.2 Process Theory
2.2.1 Operational semantics
A very natural and straightforward way to describe a concurrent system is by means of a labeled transition system. A labeled transition system is a set of states plus a transition relation on states. Each transition is labeled with an action. An action may be any kind of activity performed by a concurrent system, such as a computation local to some component of the system, a procedure call, the sending of a message or the receipt of a message. For modeling purposes, the details of actions are often not important. Actions 5
6
Basic Concurrency Theory
are assumed to be atomic entities without internal structure. The set of states in a labeled transition system is an abstraction of all possible states of a concurrent system. The transition relation describes the change in the state of a concurrent system when some action, the label of the transition, is performed. The basic notion in the framework of labeled transition systems used in this thesis is the so-called process space. A process space describes a set of processes. A process space is a labeled transition system as described above extended with a termination predicate on states. Each state in a process space can be interpreted as the initial state of a process. A process is a labeled transition system extended with a termination predicate and a distinguished initial state. The termination predicate of a process de?nes in what states the process can terminate successfully. If a process is in a state where it cannot perform any actions or terminate successfully, then it is said to be in a deadlock. The possibility to distinguish between successful termination and deadlock is sometimes useful. Process spaces form the basis for any operational semantics for concurrent systems. A predicate on the elements of some set is represented as a subset of this set: It holds for elements in the subset and it does not hold for elements outside the subset. De?nition 2.2.1. (Process space) A process space is a quadruple ( , , , ), where is a set of states, is a set of actions, ? × × is a ternary transition relation, and ? is a termination predicate.
S
process that consists of all states reachable from s.
A ,! S Let (S , A, ,!, ) be some process space. Each state s in S uniquely determines a S A
?
S A ,! S A S S S
De?nition 2.2.2. (Reachability) The reachability relation ? ? × is de?ned as the smallest relation satisfying, for any s, s , s ∈ and α ∈ , ? s ? s and α ? ? (s ? s ∧ s s ) ? s ?s . ? State s is said to be reachable from state s if and only if s ? s . The set of all states reachable from s is denoted s?.
,!
De?nition 2.2.3. (Process) Let s be a state in . The process de?ned by s is the 5-tuple (s, s?, , ∩ (s? × × s?), ∩ s?). State s is the initial state of the process.
A ,!
A
S
In the remainder, processes are identi?ed with their initial states. Sometimes, it is intuitive to think about elements of as states, whereas sometimes it is more natural to see them as processes.
S
Example 2.2.5. Figure 2.2.4 on the facing page shows some examples of processes modeling variants of a very simple production unit. Process states are depicted as dots. The initial state of a process is marked with a small incoming arrow. The production unit in Figure 2.2.4(a) is a simple sequential process that starts with receiving a command by performing action rcmd. After it has received a command, it processes some input material (pmat), outputs the processed material (omat), and then terminates. The unit in Figure 2.2.4(b) is the same process, except that, upon receiving a command, it may deadlock.
2.2 Process Theory
7
rcmd pmat omat
rcmd pmat omat
rcmd
rcmd pmat
omat
rcmd pmat omat sprdy sprdy
(c)
(d)
omat
(a)
(b)
Figure 2.2.4: Some simple examples of processes. A reason could be that the command is not understood. The process in Figure 2.2.4(c) is a variant that iterates the behavior of the production unit in (a). It does not have an option to terminate. The production unit of Figure 2.2.4(d) is again a non-iterative process. The interesting aspect of this process is that it exhibits concurrency. In parallel to its output action, it sends a ready-processing signal (sprdy) to, for example, an operator. This can be useful for an operator who must pick up the processed material if processing takes a large, but variable amount of time. In the context of process spaces, concurrency typically means that actions may be executed in any order. This representation of concurrent behavior is often called the interleaving view of concurrency. As mentioned, process spaces are used to provide a formalism for describing concurrent systems with an operational semantics. However, it might occur that the behavior of two different processes is very similar, even to such an extent that the processes may be considered equivalent. Therefore, a process space is equipped with an equivalence relation on processes, yielding the following de?nition for an operational semantics. The de?nition provides suf?cient ?exibility to precisely de?ne the meaning of system speci?cations in any Petri-net formalism or any process algebra used in this thesis. De?nition 2.2.6. (Operational semantics) An operational semantics for some given formalism for describing concurrent systems is a process space with an accompanying equivalence relation on processes. In the next two subsections, two well-known equivalence relations on processes are discussed that capture the notion of similarity of behavior in an intuitive way. The basic idea is that two processes are equivalent if and only if they can always copy, or simulate, each others actions. Two processes satisfying this requirement are called bisimilar. Bisimilarity was ?rst introduced in (PARK, 1981). Although there are many possible choices for a meaningful equivalence relation on processes, bisimilarity is the basic semantic equivalence used throughout this thesis. There are several reasons for choosing bisimilarity.
8
Basic Concurrency Theory
First, it has an easy-to-understand, intuitive de?nition. Second, it preserves some important properties of concurrent systems, such as deadlocks. And ?nally, processes that are bisimilar are also equivalent in many other semantics for concurrent systems. However, it is only fair to note that bisimilarity is not always the proper equivalence relation for concurrent systems. “When semantic equivalences are used in the design of concurrent systems ( ... ), they should be chosen in such a way that two system descriptions are considered equivalent only if the described behaviours share the properties that are essential in the context in which the system will be embedded.” (VAN G LABBEEK, 1990a, Introduction) For a detailed study of many different semantics for concurrent systems, the reader is referred to (VAN G LABBEEK, 1990a, 1990b, 1993). Since bisimilar processes are also equivalent in many other semantics, the ideas presented in this thesis carry over to these semantics with only little change. In the next subsection, the formal de?nition of bisimilarity is given and it is shown that it is an equivalence relation. Bisimilarity is often referred to as strong bisimilarity in order to distinguish it from other forms of bisimilarity. In Section 2.2.3, the notion of branching bisimilarity is introduced. Branching bisimilarity is a variant of bisimilarity that distinguishes external or observable behavior from internal or silent behavior. The distinction between external and internal behavior captures the idea that an environment observing two processes might not be able to see any differences in their behavior while internally the two processes perform different computations.
2.2.2 Strong bisimilarity
Let ( , , , ) be some process space as de?ned in De?nition 2.2.1 on Page 6. The notation has been changed from to to emphasize that, in this subsection, it is most natural to see elements of as processes. De?nition 2.2.7. (Strong bisimilarity) A binary relation R ? × is called a bisimulation or strong bisimulation if and only if, for any p, p , q, q ∈ and α ∈ , i) pRq ∧ p ii) iii)
P A ,!
P
S P
Two processes p and q are called bisimilar, or strongly bisimilar, denoted p ? q, if and only if there exists a bisimulation R such that pRq. Figure 2.2.8 on the facing page shows the essence of a bisimulation between two processes. It clearly shows that bisimulation captures the intuitive idea that two processes are equivalent if and only if, at any given point in time, they can copy each others actions. The third requirement in the de?nition above states that two bisimilar processes must have the same termination behavior.
,! p ? (? q : q ∈ P : q ,! q ∧ p Rq ), pRq ∧ q ,! q ? (? p : p ∈ P : p ,! p ∧ p Rq ), and pRq ? ( p ? q).
α α α α
P P P
A
2.2 Process Theory p α p
9
R R
q α q
Figure 2.2.8: The essence of a bisimulation. Theorem 2.2.9. Strong bisimilarity, ? , is an equivalence relation. Proof. It must be shown that bisimilarity is re?exive, symmetric, and transitive.
Re?exivity: Let I be the identity relation on × . Obviously, I is a bisimulation. Hence, for any p ∈ , p ? p. Symmetry: Let p and q be processes in . Let R be a bisimulation such that pRq. It follows from the symmetry in De?nition 2.2.7 on the preceding page that R?1 , the inverse of R, is a bisimulation such that q R?1 p. Hence, for any p, q ∈ , p ? q implies q ? p. Transitivity: Let p, q, and r be processes in . Let Q and R be bisimulations such that pQq and q Rr. It is straightforward to verify that the relation composition Q ? R is a bisimulation such that pQ ? Rr. Hence, for any p, q, r ∈ , p ? q and q ? r implies p ? r.
P
P P
P
P
P
P
2
Example 2.2.10. Consider again the examples of Figure 2.2.4(a) and (b) on Page 7. It is not dif?cult to verify that it is impossible to construct a bisimulation between these two processes. This observation is consistent with the claim made earlier that bisimilarity preserves deadlocks in processes. That is, two processes can only be bisimilar if they have the same deadlocks (see, for example, BAETEN AND W EIJLAND, 1990, Chapter 7).
rcmd
rcmd
? ? ?
rcmd pmat1 omat pmat2
rcmd pmat1 omat pmat2 omat
pmat1 omat
pmat2
(a)
(b)
(c)
Figure 2.2.11: Bisimilar or not?
10
Basic Concurrency Theory
Example 2.2.12. Figure 2.2.11 on the previous page shows again three examples of processes modeling a production unit. Although all three are different, they appear to behave similarly. In these examples, a unit has two different material sources. Hence, it has two different processing commands pmat1 and pmat2 . In the version of the unit depicted in Figure 2.2.11(a), the command speci?es which material source should be used. Therefore, before the unit receives its command, the choice is made between the two sources. In the unit depicted in Figure 2.2.11(b), the command does not specify the source and the choice is made after the unit has received its command. It is not dif?cult to see that it is impossible to construct a bisimulation between the two processes. The reason is that the moments of choice of the two processes are different. In other words, bisimilarity is said to preserve the branching structure of processes (see, for example, VAN G LABBEEK, 1994). It is useful to distinguish the two processes in Figure 2.2.11(a) and (b). Consider, for example, a situation where only the ?rst input source is ?lled with material. If the unit of Figure 2.2.11(a) receives a command specifying the second source, it will not be able to execute its processing task. If at least one of the two input sources contains material, the unit in Figure 2.2.11(b) is always able to process. Figure 2.2.11 shows also a third version of the production unit. It is easy to see that the two processes in Figure 2.2.11(b) and (c) are bisimilar. The dashed lines depict what pairs of processes construct a bisimulation. It is straightforward to check that it satis?es the conditions of De?nition 2.2.7 on Page 8. The two processes have the same branching structure. The only difference is that in process (c) the two branches do not join, whereas they do come together in the process depicted in (b).
2.2.3 Branching bisimilarity
To be able to distinguish between external, or observable, and internal, or silent, behavior, silent actions are introduced. Silent actions are actions that cannot be observed. Usually, silent actions are denoted with the action label τ . A single symbol is suf?cient, since all internal actions are equal in the sense that they do not have any visible effects. Since strong bisimilarity as de?ned in the previous subsection does not distinguish between observable actions and silent actions, it is not a suitable equivalence for processes with silent behavior. In case one is interested in observable behavior only, processes with the same observable behavior, but with different internal behavior should be equal. Branching bisimilarity is an equivalence that satis?es this requirement. Branching bisimilarity was ?rst introduced in (VAN G LABBEEK AND W EIJLAND, 1989). The de?nition given in this subsection is slightly different from the original de?nition. In fact, it is the de?nition of semi-branching bisimilarity, which was ?rst de?ned in (W EIJLAND, 1989, Chapter 1). It can be shown that the two notions are equivalent in the sense that they de?ne the same equivalence relation on processes (VAN G LABBEEK AND W EIJLAND, 1996; BASTEN, 1996). The reason for using the alternative de?nition is that it is more concise and more intuitive than the original de?nition. It also yields shorter proofs. A comparison of the two de?nitions can be found in (BASTEN, 1996).
2.2 Process Theory
11
As is the case for strong bisimilarity, branching bisimilarity distinguishes processes with different moments of choice (see VAN G LABBEEK, 1994). It is a slightly ?ner equivalence than the well-known observation equivalence (M ILNER, 1980, 1989). That is, it distinguishes more processes than observation equivalence (see VAN G LABBEEK, 1993). A comparison of branching bisimilarity, observation equivalence, and a few other equivalences on processes with silent behavior can be found in ( VAN G LABBEEK AND W EIJ LAND, 1996). Let ( , , , ) be a process space as de?ned in De?nition 2.2.1 on Page 6. The set of actions is de?ned as A ∪ {τ }, where A is some set of observable actions. To de?ne branching bisimilarity, two auxiliary de?nitions are needed: i) a relation expressing that a process can evolve into another process by executing a sequence of zero or more τ actions; ii) a predicate expressing that a process can terminate by performing zero or more τ actions.
P A ,! A
De?nition 2.2.13. The relation ? ? satisfying, for any p, p , p ∈ , p ? p and τ p ) ? p ?p . (p ? p ∧ p
P
P × P is de?ned as the smallest relation
,!
De?nition 2.2.14. The predicate ? ? isfying, for any p, p ∈ , p ? ? p and τ (? p ∧ p p) ? ? p .
P
P is de?ned as the smallest set of processes satA ,! ,!
,!
Note that it is also possible to de?ne the predicate ? in terms of ?. (α) Let, for any processes p, p ∈ and action α ∈ , p p be an abbreviation of (τ ) α the predicate (α = τ ∧ p = p ) ∨ p p . Thus, p p means that zero τ actions are performed, when the ?rst disjunct of the predicate is satis?ed, or that one τ action is performed, when the second disjunct is satis?ed. For any observable action a ∈ A, the (a) ?rst disjunct of the predicate can never be satis?ed. Hence, p p is simply equal to a p p , meaning that a single a action is performed.
P
,!
De?nition 2.2.15. ((Rooted) branching bisimilarity) A binary relation R ? × called a branching bisimulation if and only if, for any p, p , q, q ∈ and α ∈ , i) pRq ∧ p p ? (? q , q : q , q ∈
α
,!
,!
,!
α
P
P P is A
ii) pRq ∧ q q ? (? p , p : p , p ∈ iii) pRq ? ( p ? ? q ∧
,!
P:q
?q
,! q ∧ pRq
(α) (α)
∧ p Rq ),
Two processes are called branching bisimilar, denoted p ?b q, if and only if there exists a branching bisimulation R such that pRq. A branching bisimulation R is called a rooted branching bisimulation between p and q in if and only if pRq and, for any p , q ∈ and α ∈ ,
P : p ? p ,! p ∧ p Rq ∧ p Rq ), and q ? ? p). P A
P
12 iv) p
α α
Basic Concurrency Theory
Two processes p and q are called rooted branching bisimilar, denoted p ?rb q, if and only if there exists a rooted branching bisimulation between p and q. p τ p q =q q α p q α q Figure 2.2.16: The essence of a branching bisimulation. Figure 2.2.16 shows the essence of a branching bisimulation. A process must be able to simulate any action of an equivalent process after performing any number of silent actions, except for a silent action which it may or may not simulate. The third property in De?nition 2.2.15 on the previous page guarantees that related processes always have the same termination options. The root condition, introduced in the last three requirements of the de?nition, states that the initial actions of two rooted branching bisimilar processes must be the same. The requirements are identical to the requirements in the de?nition of strong bisimilarity (De?nition 2.2.7 on Page 8). The root condition is needed, because branching bisimilarity is not a congruence for the process-algebraic choice operator which is introduced in Section 2.4. Rooted branching bisimilarity, on the other hand, is a congruence for all the process-algebra operators used in this thesis. As explained in Section 2.4, any equivalence used in an operational semantics for a process algebra must have the congruence property for all the algebraic operators. Below, it is shown that branching bisimilarity and rooted branching bisimilarity are equivalence relations. However, before giving these results, a few examples are given to illustrate both equivalences. τ a p q
,! p ? (? q : q ∈ P : q ,! q ∧ p Rq ), v) q ,! q ? (? p : p ∈ P : p ,! p ∧ p Rq ), and vi) p ? q.
α α
a
Figure 2.2.17: Two branching bisimilar processes that are not rooted branching bisimilar. Example 2.2.18. Figure 2.2.17 shows two processes that are branching bisimilar but not rooted branching bisimilar. The problem is caused by the initial silent action of the left
2.2 Process Theory
13
process, which cannot be simulated by the right one. This example shows the essential difference between branching bisimilarity and rooted branching bisimilarity. Branching bisimilarity allows to remove initial silent actions, whereas rooted branching bisimilarity does not.
rcmd τ omat
rcmd omat
rcmd τ omat τ omat
(b)
(a)
(c)
Figure 2.2.19: Some examples of branching bisimilar processes. Example 2.2.20. Figure 2.2.19 shows three examples of branching bisimilar processes. The processes in (a) and (c) are the processes of Figure 2.2.11(b) and (c) on Page 9 after abstracting away the processing actions pmat1 and pmat2 . Note that the two transitions labeled pmat1 and pmat2 in Figure 2.2.11(b) result in a single transition labeled τ in Figure 2.2.19(a), because it is not possible to have two transitions with the same label between the same process states. The reason for the abstraction could be that one is interested in the input/output behavior of the production units. In both cases, the i/o behavior should be the receipt of a command followed by the output of processed material. Figure 2.2.19 shows that this is indeed the case. It is not dif?cult to verify that the two relations depicted by the dashed lines are indeed branching bisimulations. Note that they also satisfy the root condition. Hence, the three processes are not only branching bisimilar, but also rooted branching bisimilar. To prove that branching bisimilarity and rooted branching bisimilarity are equivalence relations, three auxiliary lemmas are needed. Lemma 2.2.21. Let p and q be two processes in ; let R ? bisimulation between p and q . For any p , q ∈ , i) p ? p ? (? q : q ∈ : q ? q ∧ p Rq ) and ii) q ? q ? (? p : p ∈ : p ? p ∧ p Rq ).
P P
P
P
P × P be a branching
Proof. Since the proofs of implications i) and ii) are symmetric only implication i) is proven. The proof is by induction on the number of silent actions from p to p . Base case: Assume the number of silent actions from p to p equals zero. Then, p and p must be equal. Since pRq and q ? q, Lemma 2.2.21i) is satis?ed.
14
Basic Concurrency Theory
Lemma 2.2.22. Let R ? that pRq , ? p ? ? q .
Inductive step: Assume p ? p in n silent actions, for some n ≥ 1. It follows from De?nition 2.2.13 ( ?) on Page 11 that there must exist a p ∈ such that p ? τ p in n ? 1 silent actions and p p . By induction, there exists a q ∈ such τ that q ? q and p Rq . Since p p and R is a branching bisimulation, (τ ) there exist q and q such that q ? q q , p Rq , and p Rq . Hence, q ? q and p Rq , which proves Lemma 2.2.21i) also in this case. 2
,!
P
,!
P
,!
P × P be a branching bisimulation. For any p, q ∈ P such
Proof. Only one implication is proven. The other implication follows from a symmetrical argument. The proof is by induction on the number of silent actions that a process needs to execute in order to terminate successfully.
Base case: Let p, q ∈ be two processes such that pRq and ? p with zero silent actions. It follows from De?nition 2.2.14 (? ) on Page 11 that p. Hence, Requirement iii) of De?nition 2.2.15 (Branching bisimilarity) also on Page 11 yields that ? q. Inductive step: Let p, q ∈ be two processes such that pRq and ? p with n silent actions, for some n ≥ 1. It follows from De?nition 2.2.14 (? ) that there must exτ ist a p ∈ such that p p and ? p with n ? 1 silent actions. Since R is a (τ ) branching bisimulation, there must exist q , q ∈ such that q ? q q, pRq , and p Rq . Since ? p with n ? 1 silent actions, by induction, ? q . It follows immediately from De?nitions 2.2.13 ( ? ) and 2.2.14 (? ), that ? q, which completes the proof. 2
P
P
P
,!
P
,!
As mentioned, the de?nition of branching bisimilarity chosen in this thesis is slightly different from the original de?nition. The following lemma is only valid for (rooted) branching bisimulations as de?ned in De?nition 2.2.15 on Page 11. In (BASTEN, 1996), an example is given showing that it does not hold for the original de?nition in (VAN G LABBEEK AND W EIJLAND, 1989). Lemma 2.2.23. The relation composition of two (rooted) branching bisimulations is a (rooted) branching bisimulation. Proof. Let p, q, and r be processes in ; let Q and R be (rooted) branching bisimulations such that pQq and q Rr. The goal is to show that Q ? R is a (rooted) branching bisimulation between p and r. First, to prove Requirement i) of De?nition 2.2.15 ((Rooted) α branching bisimilarity) on Page 11, assume there is a p ∈ such that p p , for some α ∈ . It must be shown that
P
A
P
,!
(? r , r : r , r ∈
P:r
?r
Since pQq, there exist q , q ∈ such that q ? q q , pQq , and p Qq . Since q Rr and q ? q , Lemma 2.2.21 i) on the previous page yields that there is an r ∈ such that r ? r and q Rr . Two cases can be distinguished.
(α)
P
,! r ∧ pQ ? Rr
(α)
,!
∧ p Q ? Rr ).
(2.2.24)
P
2.3 Petri Nets
(α)
15
ii) Assume q ?→ q . Since q Rr and R is a branching bisimulation, there must (α) exist r , r ∈ such that r ? r ?→ r , q Rr , and q Rr . It follows from (α) r ? r ?→ r , pQ ? Rr , and p Q ? Rr , that also in this case Property 2.2.24 is satis?ed.
α
i) Assume α = τ and q = q . It follows immediately that r ? r ?→r , pQ ?Rr , and p Q ? Rr . Hence, Property 2.2.24 is satis?ed.
P
Second, for reasons of symmetry, it follows immediately from the above argument that α for any r ∈ and α ∈ such that r r , Requirement ii) of De?nition 2.2.15 on Page 11 is satis?ed. Third, to prove Requirement iii) of De?nition 2.2.15, assume that p. Since Q is a branching bisimulation such that pQq, it follows that ? q. Since R is a branching bisimulation relating q to r, it follows from Lemma 2.2.22 on the preceding page that ? r. Hence, p implies ? r. A symmetrical argument yields that Requirement iii) of De?nition 2.2.15 is satis?ed. Finally, in case Q and R are rooted branching bisimulations, it is straightforward to verify that also Q ? R satis?es the root condition stated in Requirements iv) through vi) of De?nition 2.2.15. 2
P
A
,!
Theorem 2.2.25. Branching bisimilarity, ?b , and rooted branching bisimilarity, ?rb , are equivalence relations. Proof. It must be shown that branching bisimilarity and rooted branching bisimilarity are re?exive, symmetric, and transitive.
Re?exivity: Let I be the identity relation on × . It is clear that for any p ∈ , I is both a branching bisimulation and a rooted branching bisimulation between p and p. Hence, for any p ∈ , p ?b p and p ?rb p. Symmetry: Let p and q be processes in . Let R be a (rooted) branching bisimulation such that pRq. It follows from the symmetry in De?nition 2.2.15 on Page 11 that R?1 is a (rooted) branching bisimulation such that q R?1 p. Hence, for any p, q ∈ , p ?b q implies q ?b p and p ?rb q implies q ?rb p. Transitivity: Let p, q, and r be processes in . Let Q and R be (rooted) branching bisimulations such that pQq and q Rr. It follows from Lemma 2.2.23 on the preceding page that the relation composition Q ? R is a (rooted) branching bisimulation such that pQ ? Rr. Hence, for any p, q, r ∈ , p ?b q and q ?b r implies p ?b r, and p ?rb q and q ?rb r implies p ?rb r.
P P
P
P
P
P
P
P
2
2.3 Petri Nets
This section presents an introduction to Petri nets as a formalism for modeling and analyzing concurrent systems. Petri nets were introduced in 1962 by Carl Adam Petri (P ETRI, 1962). Since then, Petri-net theory has been extended in many ways and applied to many
16
Basic Concurrency Theory
kinds of problems. Its popularity is due to both its easy-to-understand graphical representation of nets and its potential as a technique for formally analyzing concurrent systems. One way of classifying the large number of Petri-net formalisms that exist to date is to separate them into colored and uncolored formalisms. This thesis is mainly concerned with uncolored Petri nets. In this section, an introduction is given to the framework of Place/Transition nets, which is illustrative for any other uncolored Petri-net formalism. Good starting points for further reading on uncolored Petri nets are (P ETERSON, 1981; ? R EISIG, 1985; B EST AND F ERN ANDEZ C., 1988; M URATA, 1989). Colored Petri nets extend the basic Petri-net formalism with data, hierarchy, and time. A full treatment of colored Petri nets can be found in (J ENSEN, 1992, 1995, 1997; VAN H EE, 1994). The next subsection introduces the notion of bags, which play an important role in any Petri-net formalism. Section 2.3.2 presents the class of labeled P/T nets, which is the most general class of P/T nets considered in this thesis. Section 2.3.3 presents some theoretical results about P/T nets that are the basis for some of the analysis techniques available to analyze Petri-net models of concurrent systems. Section 2.3.4 introduces some subclasses of labeled P/T nets. The reason to consider subclasses of labeled P/T nets is that analysis techniques for these subclasses are generally more powerful than the techniques for labeled P/T nets. This is particularly true for the so-called class of free-choice P/T nets. Section 2.3.5 focuses on the analysis of free-choice P/T nets.
2.3.1 Notations for bags
In this thesis, bags are de?ned as ?nite multi-sets of elements from some alphabet A. A bag over alphabet A can be considered as a function from A to the natural numbers IN such that only a ?nite number of elements from A is assigned a non-zero function value. For some bag X over alphabet A and a ∈ A, X (a) denotes the number of occurrences of a in X, often called the cardinality of a in X. The set of all bags over A is denoted B ( A). Note that any ?nite set of elements from A also denotes a unique bag over A, namely the function yielding 1 for every element in the set and 0 otherwise. The empty bag, which is the function yielding 0 for any element in A, is denoted 0. For the explicit enumeration of a bag, a notation similar to the notation for sets is used, but using square brackets instead of curly brackets and using superscripts to denote the cardinality of the elements. For example, [a 2, b, c3 ] denotes the bag with two elements a, one b, and three elements c; the bag [a 2 | P(a)] contains two elements a for every a such that P(a) holds, where P is some predicate on symbols of the alphabet under consideration. To denote individual elements of a bag, the same symbol “∈” is used as for sets: For any bag X over alphabet A and element a ∈ A, a ∈ X if and only if X (a) > 0. The sum of two bags X and Y , denoted X Y , is de?ned as [a n | a ∈ A ∧ n = X (a) + Y (a)]. The difference of X and Y , denoted X ? Y , is de?ned as [a n | a ∈ A ∧ n = (X (a) ? Y (a)) max 0]. The binding of sum and difference is left-associative. The restriction of X to some domain D ? A, denoted X |` D, is de?ned as [a X (a) | a ∈ D]. Restriction binds stronger than sum and difference. The notion of subbags is de?ned as expected: Bag X is a subbag of Y , denoted X ≤ Y , if and only if for all a ∈ A, X (a) ≤ Y (a).
2.3 Petri Nets
17
2.3.2 Labeled Place/Transition nets
Let U be some universe of identi?ers; let L be some set of labels. The set of positive natural numbers is denoted IP. De?nition 2.3.1. (Labeled P/T net) An L-labeled Place/Transition net, or simply labeled P/T net, is a tuple (P, T , F, W, ) where i) P ? U is a ?nite set of places; ii) T ? U is a ?nite set of transitions such that P ∩ T = ?; iii) F ? (P × T ) ∪ (T × P) is a set of directed arcs, called the ?ow relation; iv) W : F → IP is a weight function; v) : T → L is a labeling function. Let (P, T , F, W, ) be a labeled P/T net. Elements of P ∪ T are referred to as nodes. A node x ∈ P ∪T is called an input node of another node y ∈ P ∪T if and only if there exists a directed arc from x to y; that is, if and only if x F y. Node x is called an output node of y if and only if there exists a directed arc from y to x. If x is a place in P, it is called an input place or an output place; if it is a transition, it is called an input or an output transition. The set of all input nodes of some node x is called the preset of x; its set of output nodes is called the postset. Two auxiliary functions ? , ? : (P ∪ T ) → P (P ∪ T ) are de?ned that assign to each node its preset and postset, respectively. For any node x ∈ P ∪ T , ? x = {y | y F x} and x ? = {y | x F y}. Two additional functions i, o : (P ∪T ) → B (P ∪T ) assign to each node its bag of input and output nodes, respectively. For any x ∈ P ∪ T , ix = [y W (y,x) | y ∈ ?x] and ox = [y W (x,y) | y ∈ x ? ]. Example 2.3.2. Besides a mathematical de?nition, labeled P/T nets also have an unambiguous graphical representation. Figure 2.3.3 on the following page shows a labeled P/T net representing a simple production unit. Places are depicted by circles, transitions by rectangles, and the ?ow relation by arcs. The small black dots residing in the places are called tokens, which are introduced below. The weight function is represented by labeling arcs with their weights; weights equal to one are omitted. Attached to each place is its identi?er. Attached to each transition are its identi?er and its label. In the example of Figure 2.3.3, it is assumed that the labeling function is the identity function. A labeled P/T net as de?ned above is a static structure. However, labeled P/T nets also have a dynamic behavior. The dynamic behavior of a net is determined by its structure and its state. To express the state of a net, its places may contain tokens. In labeled P/T nets, tokens are nothing more than simple markers (see the graphical representation of a labeled P/T net in Figure 2.3.3 on the next page). The distribution of tokens over the places is often called the marking of the net. De?nition 2.3.4. (Marked, labeled P/T net) A marked, L-labeled P/T net is a pair (N, s), where N = (P, T , F, W, ) is an L-labeled P/T net and where s is a bag over P denoting the marking of the net. The set of all marked, L-labeled P/T nets is denoted .
N
18 cmd rcmd tcmd prdy sprdy tprdy pmt imt
3
Basic Concurrency Theory
omt pmat omat
Figure 2.3.3: The graphical representation of a labeled P/T net. The dynamic behavior of marked, labeled P/T nets is de?ned by a so-called ?ring rule, which is simply a transition relation de?ning the change in the state of a marked net when executing an action. To de?ne the ?ring rule, it is necessary to formalize when a net is allowed to execute a certain action. De?nition 2.3.5. (Transition enabling) Let (N, s) be a marked, labeled P/T net in , where N = (P, T , F, W, ). A transition t ∈ T is enabled, denoted (N, s)[t , if and only if each of its input places p contains at least as many tokens as the cardinality of p in it. That is, (N, s)[t ? it ≤ s. Example 2.3.6. In the marked net of Figure 2.3.3, transition rcmd is enabled. None of the other transitions is enabled. When a transition t of a labeled P/T net is enabled, the net can ?re this transition. Upon ?ring, t removes W ( p, t) tokens from each of its input places p; it adds W (t, p) tokens to each of its output places p. This means that upon ?ring t, the marked net (N, s) changes into another marked net (N, s ? it ot). When ?ring a transition, the labeled P/T net executes an action. What action the net performs is determined by a so-called action function. Let A be some set of actions. For any labeled P/T net N equal to (P, T , F, W, ), an action function αN : T → A is a function assigning actions to all transitions in T . The de?nition of the ?ring rule for labeled P/T nets given below is parameterized by an action function. Doing so yields a ?exible de?nition which can be instantiated with a concrete action function when de?ning the semantics of nets. The parameterization of the ?ring rule differs from the usual de?nition of the ?ring rule (see, for example P ETERSON, 1981; R EISIG, 1985; M URATA, 1989). However, it proves to be useful in the remainder of this thesis. De?nition 2.3.7. (Firing rule) Let A be some set of actions; let, for any labeled P/T net N = (P, T , F, W, ), the function αN : T → A be an action function. The ?ring rule [ ? ×A× is the smallest relation satisfying for any (N, s) in , with N = (P, T , F, W, ), and any t ∈ T , (N, s)[t ? (N, s) [αN (t) (N, s ? it ot).
N
N
N
N
2.3 Petri Nets
19
Tokens that are removed from the marking when ?ring a transition are often referred to as consumed tokens or the consumption of a transition; tokens that are added to the marking are referred to as produced tokens or the production of a transition. There are many meaningful choices for concrete action functions. If labeled P/T nets are used to model programs written in some concurrent programming language where transition labels correspond to procedure identi?cations, actions could correspond to the implementations of the procedures. For theoretical purposes, the details of actions might not be relevant. Hence, one could choose the identity function on transitions as the action function, meaning that the action performed when ?ring a transition is the transition itself. Another feasible action function is the action function that assigns to each transition its label. In other words, the labels in a labeled P/T net are interpreted as actions. De?nition 2.3.8. (Labeling action function) Let N = (P, T , F, W, ) be an L-labeled P/T net. The labeling action function αlN : T → L is equal to the labeling function . In the remainder of this section, the labeling action function is chosen as the standard action function for labeled P/T nets. Example 2.3.9. In the labeled P/T net of Figure 2.3.3 on the preceding page, ?ring transition rcmd changes the marking from [cmd, imt3 ] to [tcmd, imt3 ], thus enabling transition pmat. Firing transition pmat yields the marking [tprdy, pmt]. This new marking enables both transitions sprdy and omat. These two transitions can be ?red in arbitrary order, yielding the ?nal marking [prdy, omt]. Since, in the net of Figure 2.3.3, the labeling function is simply the identity function, the choice of the labeling action function as the standard action function means that upon ?ring a transition t action t is performed. Note that the changes in the marking when ?ring a transition are independent of the chosen action function. This example shows two clear advantages of labeled P/T nets over process spaces as a formalism to model concurrent systems. The representation of states by marked places allows to express in a very natural way that the production unit needs three pieces of input material to produce one piece of processed material. Such details are not expressible in process spaces in a straightforward way. Another advantage is that concurrency is represented in a very natural way. As opposed to the example in Figure 2.2.4(d) on Page 7, it is not necessary to duplicate transitions sprdy and omat. The de?nitions introduced so far suf?ce to give an operational semantics for marked, labeled P/T nets. In the remainder of this subsection, four possible semantics are given illustrating the ?exibility of the framework of Section 2.2. The usual Petri-net semantics (see, for example, P ETERSON, 1981; R EISIG, 1985; M URATA, 1989) does not distinguish successful termination and deadlock nor is there any difference between observable and silent behavior. In the framework developed in this chapter, such a semantics is de?ned as follows. De?nition 2.3.10. (Operational semantics) The operational semantics ( ) for L-labeled P/T nets without successful termination is the process space ( , L, [ , ?) with strong bisimilarity as the equivalence relation.
N
SN
20
Basic Concurrency Theory
In order to distinguish successful termination from deadlock, a termination predicate is needed. A reasonable de?nition of successful termination in a P/T-net framework is to say that a labeled P/T net terminates successfully if and only if ?ring a transition results in the empty marking. If the marking of a net is not empty and it cannot ?re any transitions anymore, the net is said to be in a deadlock. This de?nition for successful termination of labeled P/T nets was ?rst given in (VAN G LABBEEK AND VAANDRAGER, 1987). Let be the set of all marked, labeled P/T nets (N, 0) in .
N
De?nition 2.3.11. (Operational semantics) The operational semantics ↓( ) for Llabeled P/T nets with successful termination is the process space ( , L, [ , ) with strong bisimilarity as the equivalence relation.
N
S N
Example 2.3.12. Assuming the operational semantics ↓( ), the labeled P/T net of Figure 2.3.3 on Page 18 has a semantics which is almost identical to the process given in Figure 2.2.4(d) on Page 7 (see also Example 2.3.9 on the previous page). Only its termination behavior is different. Since the ?nal marking of the net of Figure 2.3.3 has tokens in prdy and omt (see again Example 2.3.9) and a marked net only terminates successfully if its marking is empty, the net of Figure 2.3.3 terminates in a deadlock. However, it is straightforward to de?ne an operational semantics for labeled P/T nets in which the production unit terminates successfully. Let ( , L, [ , ) be a process space where is de?ned as the set of all (N, [prdy, omt]) in . It is easy to see that in an operational semantics based on this process space, the semantics of the production unit is identical to the process given in Figure 2.2.4(d) on Page 7. Such an operational semantics could well be used to compare the (termination) behavior of different designs of a production unit. Of course, one could achieve the same results in semantics ↓( ) by simply removing places prdy and omt from the net structure.
S N
N N
S N
In order to distinguish between observable and silent behavior, it suf?ces to assume that the set of labels L contains the special label τ . The labeling action function of De?nition 2.3.8 on the previous page guarantees that ?ring a transition labeled τ results in a silent action. De?nition 2.3.13. (Operational semantics) The operational semantics o( ) for L-labeled P/T nets with silent actions but without successful termination is the process space ( , L, [ , ?) with branching bisimilarity as the equivalence relation.
S N
N
De?nition 2.3.14. (Operational semantics) The operational semantics o↓( ) for Llabeled P/T nets with silent actions and successful termination is the process space ( , L, [ , ), where is the termination predicate de?ned above, with branching bisimilarity as the equivalence relation.
S N
N
2.3.3 Analysis of labeled P/T nets
P/T-net models of concurrent systems can be analyzed in many different ways. A commonly used technique to analyze the behavior of P/T nets is simulation. P/T nets are well
2.3 Petri Nets
21
suited for simulation techniques because of their intuitive graphical representation in combination with the precise de?nition of their dynamic behavior. To date, many tools for simulating Petri-net models exist. Three well-known tools are ExSpect (ASPT, 1994), Design/CPN (J ENSEN ET AL ., 1991), and PEP (B EST AND G RAHLMANN, 1995). All three tools support colored Petri nets. The Petri-net formalism which is the basis for ExSpect is described in (VAN H EE, 1994), whereas the formalism supported by Design/CPN can be found in (JENSEN, 1992). A good starting point for references to the various formalisms underlying PEP is (G RAHLMANN, 1997). In this thesis, simulation does not play an important role. A simple application of simulation techniques for Petri nets appears in Chapter 3. Simulation is not discussed in detail. Other analysis techniques for Petri-net models are focused on properties of such models. The basic idea is that properties of a concurrent system can be phrased in terms of properties of its Petri-net model. This subsection presents a selection of properties that can be used to analyze labeled P/T nets. This selection is not exhaustive. However, it illustrates the analytical power of P/T nets and it is suf?cient for the remainder of this thesis. Some properties of P/T nets are de?ned on the structure of a net, whereas other properties concern their dynamic behavior. Therefore, assume that ( , L, [ , ) is the process space in some operational semantics for labeled P/T nets, where the set of processes is the class of marked, L-labeled P/T nets, [ ? × L × is the ?ring rule of Definition 2.3.7 on Page 18, instantiated with the labeling action function of De?nition 2.3.8 on Page 19, and is some termination predicate on . The ?rst property de?ned in this subsection is a simple structural property which is often convenient in the analysis of P/T nets. The re?exive and transitive closure of a relation R is denoted R? ; the inverse of relation R is denoted R?1 .
N N
N N
N
De?nition 2.3.15. (Connectedness) A labeled P/T net N = (P, T , F, W, ) is weakly connected, or simply connected, if and only if, for every two nodes x and y in P ∪ T , x(F ∪ F ?1 )? y. Net N is strongly connected if and only if, for every two nodes x and y in P ∪ T , x F ? y. Example 2.3.16. The P/T net in Figure 2.3.3 on Page 18 is connected, but not strongly connected. The next de?nition is fundamental in the analysis of P/T nets. It de?nes the set of markings that a P/T net can reach from its initial marking. The set of reachable markings of a P/T ? net is also called the state space of the net. Recall that ? ? × is the reachability relation de?ned in De?nition 2.2.2 on Page 6.
N N
De?nition 2.3.17. (Reachable markings) The set of reachable markings of a marked, labeled P/T net (N, s) ∈ with N = (P, T , F, W, ), denoted [N, s , is de?ned as the ? set {s ∈ B (P) | (N, s) ? (N, s )}.
N
Sometimes it is convenient to know the sequence of transitions that are ?red in order to reach some given marking. This thesis uses the following notations for sequences. Let A be some alphabet of identi?ers. A sequence of length n, for some natural number n ∈ IN,
22
Basic Concurrency Theory
over alphabet A is a function σ : {0, . . . , n ? 1} → A. The sequence of length zero is called the empty sequence and written ε. For the sake of readability, a sequence of positive length is usually written by juxtaposing the function values: For example, a sequence σ = {(0, a), (1, a), (2, b)}, for a, b ∈ A, is written aab. The set of all sequences of arbitrary length over alphabet A is written A? . De?nition 2.3.18. (Firing sequence) Let (N, s) with N = (P, T , F, W, ) be a marked, labeled P/T net in . A sequence σ ∈ T ? is called a ?ring sequence of (N, s) if and only if for some natural number n ∈ IN, there exist markings s0 , . . . , sn ∈ B (P) and transitions t1 , . . . , tn ∈ T such that s = s0 , σ = t1 . . . tn if n > 0 or σ = ε if n = 0, and, for all i with 0 ≤ i < n, (N, si )[ti+1 and si+1 = si ? iti+1 oti+1 . Sequence σ is said to be enabled in marking s, denoted (N, s)[σ . Firing the sequence σ results in the unique marking sn , denoted (N, s) [σ (N, sn ).
N
The following property is a direct result of the de?nitions given so far. It states that a marking of a labeled P/T net is reachable if and only if there is a ?ring sequence leading to that marking. Property 2.3.19. Let (N, s) with N = (P, T , F, W, ) be a marked, labeled P/T net in . For any marking s ∈ B (P), s ∈ [N, s if and only if there exists a ?ring sequence σ of (N, s) such that (N, s) [σ (N, s ).
N
Proof. De?nitions 2.3.17 (Reachable markings) and 2.3.18 (Firing sequence).
2
Example 2.3.20. It is straightforward to verify that the set of reachable markings of the P/T net in Figure 2.3.3 on Page 18 equals {[cmd, imt3 ], [tcmd, imt3 ], [tprdy, pmt], [prdy, pmt], [tprdy, omt], [prdy, omt]}. Marking [prdy, pmt] is the result of ?ring sequence rcmd pmat sprdy. The following property is often useful when analyzing the set of reachable markings of a P/T net. Property 2.3.21. (Monotonicity of reachable markings) Let (N, s) with N = (P, T , F, W, ) be a marked, labeled P/T net in . Let s and s in B (P) be two markings of N . If s is a reachable marking in [N, s , then marking s s is reachable from s s ; that is, s s ∈ [N, s s .
N
Proof. Let s and s in B (P) be two markings of N such that s is a reachable marking in [N, s . If s = s, then the property is trivial. Therefore, assume s = s. According to Property 2.3.19 and De?nition 2.3.18 (Firing sequence), there exist a non-empty ?ring sequence σ = t1 . . . tn , for some positive natural number n ∈ IP and transitions t1 , . . . , tn ∈ T , and markings s0 , . . . , sn ∈ B (P) such that s = s0 , s = sn , and, for all i with 0 ≤ i < n, (N, si )[ti+1 and si+1 = si ?iti+1 oti+1 . It follows easily from De?nition 2.3.5 (Transition enabling) on Page 18 that, for all i with 0 ≤ i < n, (N, si s )[ti+1 and si+1 s = si s ? iti+1 oti+1 . Hence, De?nition 2.3.18 yields that (N, s s ) [σ (N, s s ). Again Property 2.3.19 yields that s s ∈ [N, s s . 2
2.3 Petri Nets
23
Example 2.3.20 on the preceding page shows that it can be straightforward to calculate the set of reachable markings of a P/T net. However, in general, the state space of a nontrivial P/T net can be very large or even in?nite. A P/T net with a ?nite state space is said to be bounded. De?nition 2.3.22. (Boundedness) A marked, labeled P/T net (N, s) ∈ and only if the set of reachable markings [N, s is ?nite.
N is bounded if
The following property characterizes boundedness; it is particularly useful to prove that a P/T net is unbounded. Property 2.3.23. (Characterization of boundedness) Let (N, s) be a marked, labeled P/T net in . Net (N, s) is bounded if and only if, for any markings s ∈ [N, s and s ∈ [N, s , s ≥ s implies s = s .
N
Proof. See (P ETERSON, 1981, Section 4.2.1.1), where the property is formulated as a property of the coverability tree (called the reachability tree in (PETERSON, 1981)). The property is a direct result of Property 2.3.21 (Monotonicity of reachable markings) on the facing page and the fact that the coverability tree of a labeled P/T net is always ?nite. 2 scmd cmd rcmd tcmd imt pmat prdy sprdy tprdy pmt omt omat
rmat
Figure 2.3.24: An example of a live and unbounded P/T net. Example 2.3.25. The P/T net of Figure 2.3.3 on Page 18 is bounded. Example 2.3.20 on the preceding page shows that its state space is ?nite. Figure 2.3.24 shows a variant of the P/T net of Figure 2.3.3. It contains two new transitions, modeling an operator that sends commands to the production unit (scmd) and replenishes input material (rmat). The initial marking is the empty bag 0. For convenience, all weights are set to one. As before, it is assumed that the labeling function is the identity function. It is not dif?cult to see that the net of Figure 2.3.24 is unbounded. Since the two abovementioned transitions have no input places, they are continuously enabled. Therefore, the number of tokens in places cmd and imt, and thus all other places, can increase inde?nitely. Property 2.3.23 can be used to prove this claim formally. Firing transition scmd leads to marking [cmd], which is strictly larger than the initial marking 0.
24
Basic Concurrency Theory
Another property of a P/T-net model, which is often meaningful from a design point of view, is that it contains no so-called dead transitions. A dead transition is a transition that is never able to ?re. De?nition 2.3.26. (Dead transition) Let (N, s) be a marked, labeled P/T net in . A transition t ∈ T is dead in (N, s) if and only if there is no reachable marking s ∈ [N, s such that (N, s )[t . A property stronger than the absence of dead transitions is liveness. A P/T net is live if and only if, no matter what marking has been reached, it is always possible to enable an arbitrary transition of the net by ?ring any number of other transitions. De?nition 2.3.27. (Liveness) A marked, labeled P/T net (N, s) ∈ with N = (P, T , F, W, ) is live if and only if, for every reachable marking s ∈ [N, s and transition t ∈ T , there is a reachable marking s ∈ [N, s such that (N, s )[t . Property 2.3.28. A live marked, labeled P/T net does not have any dead transitions. Proof. De?nitions 2.3.26 and 2.3.27. scmd cmd rdy rcmd tcmd imt pmat pmt rmat Figure 2.3.29: An example of a live and bounded P/T net. Example 2.3.30. The P/T net of Figure 2.3.24 on the preceding page is live. Figure 2.3.29 shows another example of a live P/T net. It is a variant of the production unit of Figure 2.3.24. It contains three extra places. A token in place rdy means that the unit is ready to receive a command; a token in bsy means that it is busy processing; a token in empty models that the unit contains no material. Another difference with the unit of Figure 2.3.24 is that the processing-ready signal is not sent immediately after processing, but only after the output material has been delivered. A ?nal difference concerns the commands and the omat bsy empty sprdy tprdy omt prdy
N
N
2
2.3 Petri Nets
25
input material for the unit. The operator only sends a new command to the unit after a processing-ready signal has been received. Material is only replenished after output material has been delivered. Initially, two commands have been sent to the unit and three pieces of input material are available. It is possible to prove that the two P/T nets of Figures 2.3.24 and 2.3.29 are live by analyzing their state spaces. From such an analysis, it also follows that the net of Figure 2.3.29 is bounded, whereas we have already seen that the net of Figure 2.3.24 is unbounded. The P/T net of Figure 2.3.3 on Page 18 is not live. Again, this follows easily from the state space (see Example 2.3.20 on Page 22). A marking of a marked P/T net is called a home marking if and only if it is reachable from every marking reachable from the initial marking. Home markings play an important role in the analysis of termination behavior and iterative behavior. Consider a marked P/T net that terminates successfully when some given marking is reached. If this marking is a home marking, it means that the P/T net always has the option to terminate successfully. If the initial marking is a home marking of the net, then its behavior is iterative. De?nition 2.3.31. (Home marking) Let (N, s) be a marked, labeled P/T net in . A reachable marking s ∈ [N, s is a home marking of (N, s) if and only if, for any reachable marking s ∈ [N, s , s ∈ [N, s . Example 2.3.32. The initial marking of the P/T net of Figure 2.3.29 on the preceding page is a home marking. This subsection ends with two properties that a set of places of a labeled P/T net may exhibit. A set of places X of a P/T net is called a trap if every transition that needs a token from X to ?re also returns a token to X. The preset and postset of a set of nodes X of a P/T net are de?ned as follows: ? X = (∪ x : x ∈ X : ?x) and X ? = (∪ x : x ∈ X : x ? ). De?nition 2.3.33. (Trap) Let N = (P, T , F, W, ) be a labeled P/T net. A set of places X ? P is called a trap if and only if X ? ? ? X. A trap is proper if and only if it is not the empty set. A characteristic property of a trap is that, once it becomes marked, it remains marked. Recall that, for some bag Y over alphabet A and element a ∈ A, Y (a) denotes the number of occurrences of a in Y . For any X ? A, Y (X) denotes the total number of occurrences of elements of X in Y ; that is, Y (X) = (+ a : a ∈ X : Y (a)). Property 2.3.34. Let (N, s) be a labeled P/T net with N = (P, T , F, W, ). Let X ? P be a trap of N . If s(X) > 0, then, for every reachable marking s ∈ [N, s , s (X) > 0. Proof. De?nitions 2.3.33 (Trap), 2.3.17 (Reachable markings) on Page 21, and 2.3.7 (Firing rule) on Page 18. 2 Example 2.3.35. Consider again the P/T net of Figure 2.3.29 on the preceding page. The following sets of places are traps: {rdy, bsy}, {empty, pmt}, {cmd, bsy, prdy}, {rdy, tcmd, pmt, tprdy}, {cmd, tcmd, pmt, tprdy, prdy}, and {imt, pmt, omt}. By de?nition, the union of any number of traps is again a trap. The P/T net of Figure 2.3.29 has no other proper
N
26
Basic Concurrency Theory
traps than the six mentioned above and the ones that consist of the union of any number of these six traps. A set of places X of a labeled P/T net is called a siphon if and only if every transition that puts a token in X upon ?ring also consumes a token from X. De?nition 2.3.36. (Siphon) Let N = (P, T , F, W, ) be a labeled P/T net. A set of places X ? P is called a siphon if and only if ? X ? X ? . A siphon is proper if and only if it is not the empty set. A characteristic property of a siphon is that, once it becomes unmarked, it always remains unmarked. Property 2.3.37. Let (N, s) be a labeled P/T net with N = (P, T , F, W, ). Let X ? P be a siphon of N . If s(X) = 0, then, for every reachable marking s ∈ [N, s , s (X) = 0. Proof. De?nitions 2.3.36 (Siphon), 2.3.17 (Reachable markings) on Page 21, and 2.3.7 (Firing rule) on Page 18. 2 Example 2.3.38. Consider again Figure 2.3.29 on Page 24. In this particular example, the set of siphons of the P/T net is identical to its set of traps given in Example 2.3.35 on the preceding page. In this subsection, a non-exhaustive selection of properties of labeled P/T nets has been presented. However, some important aspects have not yet been addressed. Is it always possible to decide whether some marking of a labeled P/T net is reachable from its initial marking? Or whether it is a home marking? And is it always possible to decide whether some given labeled P/T net is bounded or live? The answer to all these questions is af?rmative. However, the algorithms are very complex and inef?cient. The reader interested in these algorithms, and in decidability and complexity results for P/T nets in general, is referred to the literature. A good starting point is (E SPARZA AND N IELSEN, 1994). A solution to improve the ef?ciency of analysis techniques for P/T nets is to consider subclasses of P/T nets.
2.3.4 Other classes of P/T nets
In this subsection, several subclasses of labeled P/T nets are de?ned by imposing restrictions on the net structure. A result of this approach is that the de?nitions and properties introduced in the previous subsection are valid for any of the subclasses of labeled P/T nets. Subclasses are presented in the order of decreasing expressive power. The labeling function in labeled P/T nets is often only used for modeling purposes. It usually does not affect analysis techniques. Omitting transition labeling yields the class of unlabeled P/T nets. Recall that U is the universe of identi?ers. De?nition 2.3.39. (P/T net) An unlabeled P/T net, or simply P/T net, is a U-labeled P/T net (P, T , F, W, ), as de?ned in De?nition 2.3.1 on Page 17, where the labeling function is the identity function. That is, for all t ∈ T , (t) = t. An unlabeled P/T net is usually represented by the tuple (P, T , F, W ).
2.3 Petri Nets
27
Example 2.3.40. According to De?nition 2.3.39 on the facing page, the labeled P/T nets of Figures 2.3.3 on Page 18, 2.3.24 on Page 23, and 2.3.29 on Page 24 are actually unlabeled P/T nets. De?nition 2.3.41. (Ordinary P/T net) An ordinary P/T net is a P/T net (P, T , F, W ) as in De?nition 2.3.39 on the preceding page with all weights equal to one. That is, for all x ∈ F, W (x) = 1. An ordinary P/T net is usually represented by the triple (P, T , F). Example 2.3.42. The P/T net of Figure 2.3.3 is not ordinary. The weight of the arc between imt and pmat is greater than one. The P/T nets of Figures 2.3.24 and 2.3.29, on the other hand, are ordinary. The following de?nition de?nes a particularly interesting class of ordinary P/T nets, socalled free-choice P/T nets. Free-choice P/T nets are characterized by the fact that two transitions sharing an input place always share all their input places. The class of freechoice P/T nets combines a reasonable expressive power with strong analysis techniques. Consequently, free-choice P/T nets have been extensively studied in the literature. The most important results on free-choice P/T nets have been brought together in (DESEL AND ESPARZA, 1995). De?nition 2.3.43. (Free-choice P/T net) A free-choice P/T net is an ordinary P/T net (P, T , F) as in De?nition 2.3.41 such that, for all transitions t, u ∈ T , either ?t ∩ ?u = ? or ?t = ?u. a b c
Figure 2.3.44: A non-free-choice construct: confusion. Example 2.3.45. The two P/T nets of Figures 2.3.24 on Page 23 and 2.3.29 on Page 24 are both free-choice. Figure 2.3.44 shows a typical non-free-choice construct, called confusion. In the initial state, all three transitions a, b, and c are enabled. Transitions a and c are independent; they do not share any input places. However, both transitions compete for a token with transition b and are thus in con?ict with b. The construct is called confusion, because ?ring, for example, transition a solves the con?ict between the other two transitions b and c in favor of c. After a has ?red only c is enabled. Since free-choice P/T nets play such an important role in Petri-net theory, it is interesting to study some analysis techniques for this class. The next subsection is devoted to this topic. The current subsection ends with two subclasses of free-choice P/T nets, called state machines and marked graphs. Their expressive power is limited, but they play a role in the analysis of other classes of P/T nets. An ordinary P/T net is a state machine if and only if every transition has exactly one input place and one output place.
28
Basic Concurrency Theory
De?nition 2.3.46. (State machine) A state machine is an ordinary P/T net (P, T , F) as in De?nition 2.3.41 on the preceding page such that, for every transition t ∈ T , |?t| = 1 and |t ? | = 1. An ordinary P/T net is a marked graph if and only if every place has exactly one input transition and one output transition. De?nition 2.3.47. (Marked graph) A marked graph is an ordinary P/T net (P, T , F) such that, for every place p ∈ P, |? p| = 1 and | p? | = 1. Note that ordinary P/T nets, free-choice P/T nets, state machines, and marked graphs have all been de?ned as subclasses of unlabeled P/T nets. However, it is straightforward to extend any of these classes with transition labels, yielding for example labeled, ordinary P/T nets or labeled state machines.
2.3.5 Analysis of free-choice P/T nets
As mentioned in the previous subsection, free-choice P/T nets combine expressive power with strong analysis techniques. This subsection presents some results useful in the analysis of free-choice P/T nets. Except for Property 2.3.66 on Page 32, all results in this subsection appear in (D ESEL AND ESPARZA, 1995). The main theorems are given without proof. Some other results are accompanied with proofs, because the proofs illustrate the use of the main theorems. The results in this subsection show that traps, siphons, and state machines play an important role in analyzing liveness, boundedness, and home markings of free-choice P/T nets. As in Section 2.3.3, assume that ( , L, [ , ) is the process space in some operational semantics for labeled P/T nets. The following de?nition is the basis for several results in this subsection. It de?nes the notion of a subnet of an ordinary P/T net.
N
De?nition 2.3.48. (Subnet) Let N = (P, T , F) be an ordinary P/T net, as de?ned in De?nition 2.3.39 on Page 26; An ordinary P/T net S = (P0 , T0 , F0 ) with P0 ? P and T0 ? T is a subnet of N if and only if F0 = F ∩ ((P0 × T0 ) ∪ (T0 × P0 )). Subnet S is said to be generated by the set of nodes P0 ∪ T0 . Example 2.3.50. Consider the P/T net of Figure 2.3.29 on Page 24. Figure 2.3.49 on the next page shows its subnet generated by the set of nodes {cmd, rcmd, tcmd, pmat, pmt, omat, tprdy, sprdy, prdy, scmd}. The ?rst main theorem of this subsection states that a connected free-choice P/T net is live if and only if every proper siphon includes an initially marked trap. Theorem 2.3.51. (Commoner’s theorem) Let (N, s) with N = (P, T , F) be a marked, connected free-choice P/T net in such that T is not empty. Net (N, s) is live if and only if every proper siphon X ? P contains a trap Y ? X such that s(Y ) > 0.
N
Proof. (D ESEL
AND
ESPARZA, 1995, Section 4.3)
2
2.3 Petri Nets scmd cmd prdy
29
rcmd tcmd
sprdy tprdy
pmat pmt
omat
Figure 2.3.49: A subnet of the P/T net of Figure 2.3.29 on Page 24. Example 2.3.52. Consider the free-choice P/T net of Figure 2.3.24 on Page 23. It is not dif?cult to see that this P/T net does not have any siphons. Hence, it trivially satis?es the condition of Theorem 2.3.51, which means it is live. Figure 2.3.29 on Page 24 shows another free-choice P/T net. Its traps and siphons are given in Examples 2.3.35 on Page 25 and 2.3.38 on Page 26. It follows immediately that the net satis?es the condition of Commoner’s theorem, which means that also this net is live. Note that these two results conform to the conclusions of Example 2.3.30 on Page 24. The P/T net of Figure 2.3.3 on Page 18 is not free-choice, because one of its weights equals three. Therefore, consider a variant of this P/T net with all weights equal to one. Clearly, this variant is a free-choice net. The set consisting of the single place cmd is a siphon. Since it is not a trap, the condition of Commoner’s theorem is not satis?ed. As a result, the free-choice variant of the P/T net of Figure 2.3.3 is not live. Theorem 2.3.51 (Commoner’s theorem) on the facing page can be used to prove the following interesting property of live free-choice P/T nets. It says that a live free-choice P/T net remains live when an arbitrary number of tokens is added to its marking. The basic idea of the proof is that adding tokens to a marking cannot invalidate the requirements of Commoner’s theorem. Property 2.3.53. (Monotonicity of liveness) Let (N, s) with N = (P, T , F) be a live marked, free-choice P/T net in ; let s ∈ B (P) be a marking of N .The marked, freechoice P/T net (N, s s ) is live.
N
Proof. Since Commoner’s theorem is only valid for connected free-choice P/T nets, N is partitioned into connected subnets without any connections between them. Formally, let N0 = (P0 , T0 , F0 ), . . . , Nn = (Pn , Tn , Fn ), for some n ∈ IN, be connected subnets of N such that, for all i with 0 ≤ i ≤ n, Ni is generated by Pi ∪ Ti . Furthermore, assume that P0 through Pn , T0 through Tn , and F0 through Fn are partitionings of P, T , and F,
30
Basic Concurrency Theory
respectively. Clearly, it follows from De?nition 2.3.27 (Liveness) on Page 24 that, for any marking s ∈ B (P), (N, s) is live if and only if, for all i with 0 ≤ i ≤ n, (Ni , s |` Pi ) is live. Let Ni , for some i with 0 ≤ i ≤ n, be an arbitrary subnet of N as de?ned above. To prove Property 2.3.53, it suf?ces to show that, for arbitrary markings s, s ∈ B (Pi ), (Ni , s s ) is live from the assumption that (Ni , s) is live. If Ti = ?, De?nition 2.3.27 (Liveness) immediately yields that (Ni , s s ) is live. Therefore, assume that Ti = ?. Note that, since N is free-choice, also Ni is free-choice. Thus, it follows from the assumption that (Ni , s) is live and Theorem 2.3.51 (Commoner’s theorem) on Page 28 that every proper siphon X ? Pi of Ni contains a trap Y ? X such that s(Y ) > 0. Consequently, every proper siphon X ? Pi contains a trap Y ? X such that (s s )(Y ) > 0. Again Theorem 2.3.51 yields that (Ni , s s ) is live. 2 Note that liveness is not monotone for ordinary P/T nets. It is a nice exercise to ?nd a live ordinary P/T net that is no longer live when one or more tokens are added to the initial marking. For the impatient reader, Figure 4.3.49 on Page 195 in Chapter 4 contains an example of such a net. The following de?nition de?nes a very speci?c kind of subnet of ordinary P/T nets. It forms the basis for the second important theorem of this subsection. De?nition 2.3.54. (S-component) Let N = (P, T , F) be an ordinary P/T net; let ? , ? : P ∪T → P (P ∪T ) be the preset and postset functions of N. The subnet S = (P0 , T0 , F0 ) of N with P0 = ? is an S-component of N if and only if S is a strongly connected state machine, as de?ned by De?nitions 2.3.15 on Page 21 and 2.3.46 on Page 28, such that, for every place p ∈ P0 , ? p ∪ p? ? T0. Example 2.3.55. The ordinary P/T net of Figure 2.3.49 on the preceding page is an Scomponent of the P/T net of Figure 2.3.29 on Page 24. A characteristic property of an S-component of some ordinary P/T net is that the number of tokens in the places of the S-component is constant for all reachable markings. Property 2.3.56. Let (N, s) be a marked, ordinary P/T net in ; let (P, T , F) be an Scomponent of N . For any reachable marking s ∈ [N, s , s (P) = s(P). Proof. Induction on the length of any ?ring sequence needed to reach marking s from marking s plus Property 2.3.19 on Page 22. 2 Example 2.3.57. Consider again the P/T net of Figure 2.3.29 on Page 24 and its S-component of Figure 2.3.49 on the previous page. It is not dif?cult to see that the number of tokens in the S-component is two for every reachable marking. Property 2.3.56 has many interesting consequences. The following property states that the marking of a live connected ordinary P/T net marks all of its S-components. Property 2.3.58. Let (N, s) with N = (P, T , F) be a live marked, connected ordinary P/T net in such that T is not empty. For every S-component (P0, T0 , F0 ) of N , s(P0 ) > 0.
N
N
2.3 Petri Nets
31
Proof. If N has no places the property is trivial. Therefore, assume that P is not empty. Let (P0 , T0 , F0 ) be an S-component of N such that P0 is not empty. Assume that s(P0 ) = 0. It follows from the assumption that T is not empty and De?nitions 2.3.15 (Connectedness) on Page 21 and 2.3.54 (S-component) on the preceding page that T0 is not empty. Property 2.3.56 implies that any of the places in P0 is unmarked in any marking reachable from s. Thus, it follows from De?nitions 2.3.26 (Dead transition) on Page 24 and again 2.3.54 (Scomponent) that all transitions in T0 are dead in (N, s). However, this contradicts Property 2.3.28 on Page 24, which states that a live P/T net cannot have dead transitions. Hence, s(P0 ) > 0. 2 Property 2.3.58 can be strengthened for a certain class of free-choice P/T nets. Property 2.3.59. Let (N, s) with N = (P, T , F) be a live and bounded marked, connected free-choice P/T net such that T is not empty. Let s ∈ B (P) be a marking of N . The marked P/T net (N, s ) is live if and only if, for every S-component (P0 , T0 , F0 ) of N , s (P0 ) > 0. That is, (N, s ) is live if and only if s marks every S-component of N . Proof. The implication from left to right follows immediately from Property 2.3.58 on the facing page. The other implication is a consequence of Theorem 2.3.51 (Commoner’s theorem) on Page 28 and several results concerning siphons and traps, see (D ESEL AND ESPARZA, 1995, Section 5.2) for details. 2 An S-cover of an ordinary P/T net is a set of S-components such that each place of the net is contained by at least one S-component. De?nition 2.3.60. (S-cover) Let N = (P, T , F) be an ordinary P/T net; let C be a set of S-components of N. Set C is called an S-cover of N if and only if, for every place p ∈ P, there exists an S-component (P0, T0 , F0 ) in C such that p ∈ P0 . The second important theorem of this subsection is the S-coverability theorem. Theorem 2.3.61. (S-coverability theorem) Let (N, s) be a live and bounded marked, free-choice P/T net. Net N has an S-cover. Proof. (D ESEL
AND
ESPARZA, 1995, Section 5.1)
2
Example 2.3.62. In Example 2.3.30 on Page 24, it was argued that the P/T net of Figure 2.3.29 also on Page 24 is live and bounded. Since this P/T net is free-choice, it must have an S-cover. It is not dif?cult to verify that the four subnets generated by the sets of nodes {cmd, rcmd, tcmd, pmat, pmt, omat, tprdy, sprdy, prdy, scmd}, {rdy, rcmd, bsy, sprdy}, {empty, pmat, pmt, omat}, and {imt, pmat, pmt, omat, omt, rmat} are S-components that form an S-cover. The ?rst one of these S-components is the one shown in Figure 2.3.49 on Page 29. Note that the marking in Figure 2.3.29 marks all S-components, which conforms to Property 2.3.59. The S-coverability theorem can be used to prove, for example, the following property of live and bounded free-choice P/T nets.
32
Basic Concurrency Theory
Property 2.3.63. Let (N, s) with N = (P, T , F) be a live and bounded marked, freechoice P/T net in . For every marking s ∈ B (P), net (N, s ) is bounded.
N
Proof. According to De?nition 2.3.22 (Boundedness) on Page 23, it must be shown that the set of reachable markings [N, s is ?nite. First, note that the number of tokens in marking s , s (P), is ?nite. Second, it follows from Theorem 2.3.61 (S-coverability theorem) on the preceding page that N has an S-cover C. Since the number of places of a P/T net is ?nite, it follows from De?nition 2.3.60 (S-cover) on the previous page that the number of S-components in C, |C|, is also ?nite. Since every S-component initially contains at most s (P) tokens, it follows from Property 2.3.56 on Page 30 that every reachable marking s ∈ [N, s contains at most s (P) · |C| tokens; that is, for every s ∈ [N, s , s (P) ≤ s (P) · |C|. Since the number of places of N is ?nite, it follows that [N, s is ?nite. 2 The basis for the S-coverability theorem is the notion of an S-component. S-components are de?ned in terms of state machines, as introduced in the previous subsection. In a similar way, marked graphs form the basis of so-called T-components. Analogously to the S-coverability theorem, it can be shown that live and bounded free-choice P/T nets are covered by T-components. See (D ESEL AND ESPARZA, 1995) for more details. The third and ?nal theorem of this subsection states that a reachable marking of a live and bounded connected free-choice P/T net is a home marking if and only if it marks every proper trap of the net. Theorem 2.3.64. (Home-marking theorem) Let (N, s) with N = (P, T , F) be a live and bounded marked, connected free-choice P/T net in such that T is not empty. A reachable marking s ∈ [N, s is a home marking of (N, s) if and only if, for every proper trap X ? P , s (X) > 0.
N
Proof. (D ESEL
AND
ESPARZA, 1995, Section 8.2)
2
Example 2.3.65. Consider again the P/T net of Figure 2.3.29 on Page 24 and its traps given in Example 2.3.35 on Page 25. Since the initial marking marks every proper trap of the net, it is a home marking, which conforms to the claim of Example 2.3.32 on Page 25. The Home-marking theorem can be used to prove monotonicity of home markings for live and bounded free-choice P/T nets. Property 2.3.66. (Monotonicity of home markings) Let (N, s) with N = (P, T , F) be a live and bounded marked, free-choice P/T net in . Let s and s in B (P) be two markings of N . If s is a home marking of (N, s), then s s is a home marking of (N, s s ).
N
Proof. If N has no transitions, the property is trivial. Therefore assume that T is not empty. Without loss of generality, it may also be assumed that N is connected. (If N is not connected, it is possible to consider the partitioning of connected subnets of N, similar to the proof of Property 2.3.53 (Monotonicity of liveness) on Page 29.) Assume that s is a home marking of (N, s). The goal is to use the Home-marking theorem to prove that s s is a home marking of (N, s s ). Thus, it must be shown
2.4 Process Algebra
33
that (N, s s ) is live and bounded, that s s ∈ [N, s s , and that s s marks every proper trap of N. Since (N, s) is live and bounded, Properties 2.3.53 on Page 29 and 2.3.63 on the facing page yield that (N, s s ) is live and bounded. Since s is a home marking of (N, s), it follows from De?nition 2.3.31 (Home marking) on Page 25 and Property 2.3.21 on Page 22 that s s ∈ [N, s s . It follows from the Home-marking theorem that s marks every proper trap of N and, thus, that also s s marks every proper trap of N. As a result, the conditions of the Home-marking theorem are satis?ed proving that s s is a home marking of (N, s s ). 2 Similar to Property 2.3.53 (Monotonicity of liveness) on Page 29, Property 2.3.66 does not generalize to ordinary P/T nets. Figure 4.3.49 on Page 195 shows a live and bounded ordinary P/T net with a home marking that does not satisfy the monotonicity requirement stated in Property 2.3.66. The three main theorems of this subsection, Commoner’s theorem, the S-coverability theorem, and the home-marking theorem, form the basis for several ef?cient analysis techniques for free-choice P/T nets. None of the results generalizes to ordinary P/T nets, although some of them (partially) generalize to subclasses of ordinary P/T nets that are slightly larger than free-choice P/T nets. The interested reader is referred to (D ESEL AND ESPARZA, 1995, Chapter 10).
2.4 Process Algebra
This section gives an introduction to process algebra in the style of the Algebra of Communicating Processes, abbreviated ACP, (see B ERGSTRA AND K LOP, 1984; BAETEN AND V ERHOEF, 1995; BAETEN AND W EIJLAND, 1990). Whereas Petri-net formalisms are graphical by nature, process algebras are symbolic. Process algebras are often used for the analysis of concurrent-system behavior, in particular, the comparison of behaviors. There are many different kinds of process algebras. Apart from the already mentioned ACP, the process algebras CCS (M ILNER, 1980, 1989) and CSP (H OARE, 1985) are the most wellknown. Speci?cations and veri?cations in ACP are based on an equational style of reasoning, as opposed to CCS and CSP, which are model-based. In the latter case, the starting point of the process algebra is an operational semantics. The goal is to ?nd equational laws that are valid in the semantics. In the former case, the starting point is an equational theory, which may have several operational (or non-operational) semantic interpretations. For a detailed comparison of ACP, CCS, and CSP, the reader is referred to (BAETEN AND W EIJLAND, 1990, Chapter 8). The next subsection introduces the process algebra BPA which can be used to reason about sequential processes only, but which shows the essentials of any process-algebraic theory. Section 2.4.2 extends BPA in such a way that it is possible to reason about deadlocks in a process. In Section 2.4.3, concurrency in process algebra is introduced. Section 2.4.4 presents a process algebra for reasoning about processes with silent behavior.
34
Basic Concurrency Theory
Finally, Section 2.4.5 shows how to formalize a simple form of recursion in a processalgebraic setting.
2.4.1 Basic Process Algebra
The most elementary process algebra in the style of ACP is the so-called Basic Process Algebra, abbreviated BPA. It can be used to reason about the behavior of sequential processes. As mentioned, any ACP-style process algebra is basically an equational theory. An equational theory consists of a signature and a set of axioms. The signature de?nes the sorts of the theory, a set of variables for each sort, and the functions of the theory. Functions and variables can be used to construct terms. In process algebra, terms usually represent processes. Terms not containing any variables are called closed terms. The axioms of the theory determine which terms are equal. A 0-ary function is often called a constant; other functions are often called operators. The equational theory BPA. The signature and axioms of BPA are given in Table 2.4.1. The theory is parameterized by a set of constants A, which is a set of actions. The ?rst part of Table 2.4.1 lists the sorts of BPA; the second part de?nes the operators and the third part gives the variables and lists the axioms. Note that the signature of BPA has no variables of sort A. Also note that new variables may be introduced any time when necessary. An informal explanation of the operators and the axioms is given below. BPA(A) P; A ? P + , · : P×P →P x, y, z : P; x +y = y+x (x + y) + z = x + (y + z) x +x =x (x + y) · z = x · z + y · z (x · y) · z = x · (y · z) A1 A2 A3 A4 A5
Table 2.4.1: The process algebra BPA. As mentioned, A is a set of actions. Terms of sort P represent processes. Each action is a process, namely the process that can only execute the action and then terminates. The operators + and · denote choice and sequential composition, respectively. Sequential composition binds stronger than choice. Given some processes, the operators of BPA can be used to construct new processes. If two processes x and y are composed using the choice operator, the behavior of the new process x + y may be either x or y. Process x · y ?rst performs x and, upon successful termination of x, it performs y. Thus, choice and sequential composition are two elementary operators in describing the behavior of
2.4 Process Algebra
35
sequential processes. Most of the axioms of BPA are self-explanatory. Only Axiom A4 might need some explanation. It states the right distributivity of sequential composition over choice. The converse, left distributivity, is not an axiom of the theory. As a result, processes with different moments of choice are distinguished. Example 2.2.12 on Page 10 explains why this can be useful. An equational theory like BPA de?nes an equivalence relation, namely derivability from the axioms of the theory. For any terms x and y in some given process algebra X, X x = y denotes that x = y can be derived from the axioms of X. Derivability is de?ned as follows. First, the axioms themselves can be derived from the axioms of an equational theory. Second, since derivability is an equivalence relation, it is re?exive, symmetric, and transitive. Third, if an equation is derivable from the axioms, then also any equation obtained by substituting terms for variables in this equation is derivable. Finally, any equation obtained by replacing a term in an arbitrary context by another derivably equivalent term is also derivable from the theory. The axioms of an equational theory must be chosen in such a way that derivability de?nes a meaningful equivalence relation on processes. Below, it is explained that, in the case of the theory BPA, derivability corresponds to bisimilarity. Example 2.4.2. It can be shown that BPA rcmd · ((pmat1 + pmat2 ) · omat) = rcmd · (pmat1 ·omat + pmat2 ·omat). The ?rst step is to substitute pmat1, pmat2, and omat for the variables x, y, and z in Axiom A4, which shows that BPA t1 = t2 , where t1 is the term (pmat1 + pmat2) · omat and t2 denotes the term pmat1 · omat + pmat2 · omat. The second and ?nal step consists of an application of the context rule explained above: Replacing term t1 in rcmd · t1 with the equivalent term t2 yields the desired result. The intuitive meaning of the operators, the axioms, and the induced equivalence relation given above can be formalized by giving an operational semantics. However, before going into more details about the operational semantics for BPA, a few more aspects of the theory BPA itself are explained. The main purpose of a theory as BPA is to reason about processes in an equational way. The goal is to prove a desired equality on processes by applying simple term-rewriting techniques. As a consequence, a very useful property of a process algebra is when its (closed) terms can be reduced to (unique) normal forms. If such normal forms exist, an equational proof becomes very simple. The equality of two process terms can be shown by reducing them to their normal forms. If the normal forms are equal, then, obviously, also the two processes are equal. By considering Axioms A3, 4, and 5 in Table 2.4.1 on the facing page as rewrite rules from left to right, it can be shown that closed BPA terms have normal forms. The proof and more details about term rewriting in the context of process algebra can be found in (BAETEN AND V ERHOEF, 1995). For the purpose of this thesis, it is suf?cient to know that the normal forms of closed BPA terms are contained in a very speci?c class of terms, called basic terms. De?nition 2.4.3. (Basic terms) The set of basic BPA terms, denoted B (BPA), is inductively de?ned as follows. The actions A are contained in B (BPA). Furthermore, for any a ∈ A and s, t ∈ B (BPA), also a · t and s + t are elements of B (BPA).
36
Basic Concurrency Theory
Note that not all basic terms are normal forms of closed terms. For example, basic term a+a, where a is some action in A, can be reduced by means of Axiom A3 and is, therefore, not a normal form. The set of all closed terms of X is denoted C (X) . Property 2.4.4. (Elimination) For any closed term p ∈ C (BPA), there exists a basic term t ∈ B (BPA), such that BPA p = t . Proof. It is straightforward to prove the property using Axioms A3, 4, and 5 in Table 2.4.1 on Page 34 as rewrite rules from left to right. For details, see (BAETEN AND V ERHOEF, 1995). 2 The above result is called the elimination property, because it shows that the general sequential composition · as de?ned in Table 2.4.1 on Page 34 can be eliminated from any closed term, yielding a term containing only so-called pre?x compositions. A pre?x composition is a sequential composition whose left operand is a single action (see De?nition 2.4.3 (Basic terms) on the previous page). The elimination property is useful in inductive proofs in process algebra (see Section 2.4.3). An operational semantics for BPA. The processes in the operational semantics for BPA are the closed BPA terms. It remains to give a transition relation and a termination predicate. The theory BPA does not allow to distinguish between successful termination and deadlock. In Section 2.4.2, BPA is extended in such a way that it is possible to make this distinction. The usual semantics for BPA is that termination means successful ter√ mination. For this purpose, a special process , pronounced “tick,” is introduced, which is the only process that can terminate successfully. The transition relation ?→ ? √ √ (C (BPA) ∪ { }) × A × (C (BPA) ∪ { }) can now be de?ned as the smallest relation satisfying the derivation rules in Table 2.4.5. The rules conform to the intuitive explanation given above. a : A; p, p , q, q : a ?→
a a
C (BPA);
p ?→ p p · q ?→ p · q q ?→ q p + q ?→ q
a a a a
√
p ?→
a
a
√
a
p ?→ p p + q ?→ p
a
p · q ?→ q a √ p ?→ a √ p + q ?→
q ?→
a
√ √
p + q ?→
Table 2.4.5: The transition relation for BPA. De?nition 2.4.6. (Operational semantics) The operational semantics (BPA) is the pro√ √ cess space (C (BPA) ∪ { }, A, ?→ , { }), where ?→ is the transition relation de?ned above, with strong bisimilarity as the equivalence relation.
S
2.4 Process Algebra
37
Example 2.4.7. Consider Example 2.2.5 on Page 6. The process depicted in Figure 2.2.4 (a) on Page 7 can be speci?ed in BPA by the closed term rcmd·pmat·omat. Since sequential composition is associative, brackets are omitted. It is easy to see that the semantics of this closed term, assuming the operational semantics (BPA), is indeed the desired process. The two processes depicted in Figure 2.2.4(b) and (c) cannot be expressed in BPA. The theory has no means to specify deadlocks nor does it allow iterative or other recursive speci?cations. Although BPA has no explicit concurrency operator, it is possible to specify the process of Figure 2.2.4(d) as follows: rcmd·pmat·(omat·sprdy+sprdy·omat).
S
Example 2.4.8. Consider Example 2.2.12 on Page 10. In BPA, the three processes depicted in Figure 2.2.11 on Page 9 are de?ned as (rcmd · pmat1 + rcmd · pmat2 ) · omat, rcmd · (pmat1 + pmat2) · omat, and rcmd · (pmat1 · omat + pmat2 · omat). The ?rst two terms cannot be proved equal in BPA, because the theory lacks an axiom stating the left distributivity of sequential composition over choice. The second and third process, on the other hand, are equal in BPA. As shown in Example 2.4.2 on Page 35, the desired equality follows from a single application of Axiom A4, stating the right distributivity of sequential composition over choice. Not every operational semantics is suitable for an equational theory such as BPA. The minimal requirement for a proper semantics is that the axioms of the theory must be sound for the semantics. A set of axioms is sound for a semantics only if any equality that can be derived from the axioms is also valid in the semantics. An equality between processes is valid in a semantics if and only if the processes are equivalent according to the semantic equivalence. Validity is formally de?ned as follows. Let p and q be two closed terms in some given process algebra X. For any operational semantics for X, the equation p = q is valid in , denoted |= p = q, if and only if p ≈ q, where ≈ is the equivalence in . The soundness requirement implies that the equivalence relation must be a congruence for all the operators in the algebra. That is, for a given semantic equivalence ≈ the following property must be satis?ed. Let f be any n-ary function in the signature of the process algebra, where n is some natural number; let p1 , . . . , pn , q1 , . . . , qn be closed terms of the appropriate sorts such that p1 ≈ q1 , . . . , pn ≈ qn . Then, the congruence property requires that f ( p1, . . . , pn ) ≈ f (q1, . . . , qn ).
S
S
S
S
Example 2.4.9. A simple example shows why the congruence property is necessary. Assume that ≈ is a semantic equivalence in an operational semantics for which the axioms of BPA are sound. Furthermore, assume that ≈ is not a congruence for the choice operator. This means that there exist closed BPA terms p1, p2 , q1 , and q2 satisfying i) BPA p1 = q1 and BPA p2 = q2 , and ii) p1 ≈ q1 and p2 ≈ q2 , but not satisfying p1 + p2 ≈ q1 + q2. Since BPA p1 + p2 = q1 + q2 , this clearly contradicts the soundness of BPA for the semantics. Property 2.4.10. (Congruence) Strong bisimilarity, ?, is a congruence for the operators of BPA. Proof. See (BAETEN AND V ERHOEF, 1995). Note that the proof in (BAETEN AND V ER HOEF, 1995) uses the fact that the derivation rules used to de?ne the operational semantics
38
Basic Concurrency Theory
for BPA are in the so-called path format. Although the formulation of the operational semantics in this section follows a slightly different notation, it is straightforward to give an equivalent de?nition satisfying the desired format. 2 Besides soundness, a useful property of a set of axioms of an equational theory is completeness. A set of axioms is complete if every equality that is valid in the semantics is also derivable from the axioms. The following theorem is a standard result in process algebra. Theorem 2.4.11. (Soundness and completeness) For any closed terms p, q ∈ C (BPA), BPA p = q ? (BPA) |= p = q .
S
Proof. (BAETEN
AND
V ERHOEF , 1995)
This theorem means that the semantics (BPA) de?ned in De?nition 2.4.6 on Page 36 captures all the essential aspects of BPA, as far as closed terms are considered. A consequence of the soundness result and the fact that bisimilarity preserves the branching structure of processes is that derivability also preserves the branching structure of processes, as was already mentioned earlier.
S
2
2.4.2 Basic Process Algebra with inaction
As explained in the previous subsection, BPA does not allow to distinguish between successful termination and deadlock. Therefore, in this subsection, BPA is extended to BPAδ , which is an abbreviation of Basic Process Algebra with inaction. The equational theory BPAδ . Table 2.4.12 shows the equational theory BPAδ . The ?rst entry means that BPAδ is an extension of BPA. The other entries of Table 2.4.12 have a meaning as explained before. BPAδ (A) BPA(A) δ: P x : P; x +δ =x δ·x =δ A6 A7
Table 2.4.12: The process algebra BPAδ . In BPAδ , one new process is introduced, namely δ. Process δ stands for inaction, often also called deadlock. However, the former name is best suited, as follows from Axiom A6. It says that a process which can choose between some behavior x and doing nothing is equivalent to the process that has no choice and can only do x. Hence, in the context of a choice, δ is not a true deadlock. Axiom A7 shows that δ is a deadlock in the context of a sequential composition.
2.4 Process Algebra
39
Property 2.4.14. (Elimination) For any closed term p ∈ C (BPAδ ), there is a basic term t ∈ B (BPAδ ), such that BPAδ p = t . Proof. (BAETEN
AND
De?nition 2.4.13. (Basic terms) The set of basic BPAδ terms, denoted B (BPAδ ), is inductively de?ned as follows. The actions A and process δ are contained in B (BPAδ ). Furthermore, for any a ∈ A and s, t ∈ B (BPAδ ), also a · t and s + t are elements of B (BPAδ ).
As before, BPAδ terms can be reduced to basic terms. However, the set of basic BPAδ terms differs from the set of basic BPA terms because δ is a basic BPAδ term (and can therefore be used in the construction of other basic BPAδ terms).
V ERHOEF , 1995)
2
An operational semantics for BPAδ . The processes in the operational semantics for √ BPAδ are the closed BPAδ terms. As before, a special process is introduced, which is the only process that can terminate successfully. The transition relation is the same as the √ √ transition relation for BPA. That is, ?→ ? (C (BPAδ ) ∪ { }) × A × (C (BPAδ ) ∪ { }) is the smallest relation satisfying the derivation rules in Table 2.4.5 on Page 36, where p, p , q, and q range over C (BPAδ ). This means that the new process δ cannot perform any actions, which conforms to the claim that it represents inaction. As a result, it is possible to distinguish between successful termination and deadlock. Note that the process that can only terminate successfully cannot be expressed in the theory BPAδ . It is possible to extend BPA or BPAδ with a constant called the empty process. The empty process is exactly the process that can only terminate successfully. For more details about the empty process, see (BAETEN AND V ERHOEF, 1995; BAETEN AND W EIJLAND, 1990). De?nition 2.4.15. (Operational semantics) The operational semantics (BPAδ ) is the √ √ process space (C (BPAδ ) ∪ { }, A, ?→ , { }) with strong bisimilarity as the equivalence relation. Example 2.4.16. Consider again Example 2.2.5 on Page 6. Since BPAδ is an extension of BPA, the BPAδ speci?cations of the processes in Figure 2.2.4 (a) and (d) on Page 7 are identical to the BPA speci?cations given in Example 2.4.7 on Page 37. In BPA δ , it is possible to de?ne the process depicted in Figure 2.2.4(b) as follows: rcmd·δ+rcmd·pmat· omat. Recall that it is not possible to de?ne this process in BPA (see Example 2.4.7). It is still not possible to de?ne the iterative process of Figure 2.2.4(c). As before, strong bisimilarity is a congruence for the operators of BPAδ and the axioms of BPAδ are sound and complete for the operational semantics. Property 2.4.17. (Congruence) Strong bisimilarity, ?, is a congruence for the operators of BPAδ . Proof. (BAETEN
AND
S
V ERHOEF , 1995)
Theorem 2.4.18. (Soundness and completeness) For any closed terms p, q ∈ C (BPAδ ), BPAδ p = q ? (BPAδ ) |= p = q .
2 2
S
Proof. (BAETEN
AND
V ERHOEF , 1995)
40
Basic Concurrency Theory
2.4.3 Process Algebra with inaction and renaming
One of the main goals of this thesis is to study formalisms for describing concurrent systems. However, the basic process-algebraic theories of the previous two subsections are only suitable for reasoning about sequential processes. To allow reasoning about concurrent processes, in this subsection, a concurrency operator is introduced. At the same time, a second new feature is added to the theory, namely renaming. Renaming is a general construct which can be used to de?ne operators such as an encapsulation operator and an abstraction operator. The encapsulation operator renames actions to δ, thus effectively blocking, or encapsulating, them. The encapsulation operator is introduced below. The abstraction operator renames actions to τ , thus hiding them from the environment. The abstraction operator is introduced in the next subsection, where a process algebra for processes with silent behavior is given. Extending BPAδ with concurrency and renaming yields the theory PAδ+RN, which is an abbreviation of Process Algebra with inaction and renaming. The absence of the adjective “basic” in the name expresses that the theory contains a concurrency operator. The naming conventions for ACP-style process algebras are standard (see, for example, BAETEN AND V ERHOEF , 1995; BAETEN AND W EIJLAND, 1990). The equational theory PAδ +RN. Let A be again some set of action labels. A renaming function f : (A ∪ {δ}) → (A ∪ {δ}) is any function with the restriction that f (δ) = δ. This restriction means that the inaction process can be the result of a renaming, but that it cannot be renamed itself. It is included in the domain of renaming functions only for the sake of convenience. The sort of all renaming functions is denoted F. Table 2.4.19 gives the theory PAδ+RN. The informal explanation of the operators and the axioms is given below, along with the binding precedences of the operators. PAδ +RN(A) BPAδ , F , : P×P →P ρ : F → (P → P) a : A ∪ {δ}; f : F; x, y, z : P; x y=x y+y x a x =a·x a · x y = a · (x y) (x + y) z = x z + y M1 M2 M3 M4 ρf (a) = f (a) ρf (x + y) = ρf (x) + ρf (y) ρf (x · y) = ρf (x) · ρf (y) RN1 RN2 RN3
z
Table 2.4.19: The process algebra PAδ +RN. The theory PAδ + RN is an extension of BPAδ . Three new operators are introduced. The parallel-composition operator , often called the merge operator, denotes the parallel execution of its operands. It is axiomatized using an auxiliary operator , called the
2.4 Process Algebra
41
left merge. The left merge has the same meaning as the merge except that the left process must perform the ?rst action. The axiomatization of the merge in terms of the left merge means that the interleaving view of concurrency is chosen (see also Example 2.2.5 on Page 6). Finally, for any renaming function f in F, the renaming operator ρf simply renames actions according to f . The binding precedence of the operators of PAδ +RN is as follows. The unary renaming operators bind stronger than binary operators. Sequential composition binds stronger than all other binary operators. Choice binds weaker than all other operators. The operators and axioms introduced in this subsection can be used to de?ne various other process algebras. Extending the theory BPA with all the operators and axioms of Table 2.4.19 on the preceding page yields the process algebra PA+RN. Omitting the renaming operators and the corresponding axioms from PAδ + RN or PA + RN yields the theories PAδ and PA respectively. It is also possible to extend BPA or BPAδ with only renaming. The following property states that the new operators introduced in this subsection can be eliminated from closed terms yielding an equivalent basic term. Property 2.4.20. (Elimination) i) For any closed term p ∈ C (X), where X is a process algebra in {PA, PA+RN}, there is a basic term t ∈ B (BPA), such that X p = t . ii) For any closed term p ∈ C (X), where X is a process algebra in {PAδ , PAδ +RN}, there is a basic term t ∈ B (BPAδ ), such that X p = t . Proof. The results for PA and PAδ appear in (BAETEN AND V ERHOEF, 1995). Using the techniques of (BAETEN AND V ERHOEF, 1995), the proofs for PA+RN and PAδ +RN are straightforward. 2 The next result states that the new theories are proper extensions of one of the basic theories BPA or BPAδ . It is not possible to derive any equalities between BPA or BPAδ processes from the axioms of the new theories that are not also derivable from the original theories. Property 2.4.21. (Conservative extension) i) For any closed terms p, q X p = q ? BPA ii) For any closed terms p, q X p = q ? BPAδ ∈ C (BPA) and process algebra X ∈ {PA, PA+RN}, p = q. ∈ C (BPAδ ) and process algebra X ∈ {PAδ , PAδ +RN}, p = q.
Proof. The results for PA and PAδ appear in (BAETEN AND V ERHOEF, 1995). Using the techniques of (BAETEN AND V ERHOEF , 1995), the proofs for PA + RN and PAδ + RN are straightforward. Note that the proof techniques for proving conservativity results in (BAETEN AND V ERHOEF, 1995) depend on the operational semantics given for the various process algebras. However, this does not cause problems, because the semantics given below and in the previous subsections are identical to those given in (BAETEN AND V ER HOEF, 1995). The reason for presenting the conservativity result before the operational
42
Basic Concurrency Theory
semantics is de?ned, is that the result itself is independent of the semantics. Furthermore, there are also proof techniques that do not use any speci?c semantics (see BAETEN AND W EIJLAND, 1990). 2 Renaming and merge. The theory PAδ +RN as introduced in Table 2.4.19 on Page 40 does not contain any axioms describing the interaction between the renaming operator and the merge. A meaningful and useful axiom would be the distribution of renaming over merge. The reason that such an axiom is not included in the standard de?nition of PAδ+RN is twofold. First, the elimination result given above means that, in theory, such an axiom is redundant. Second, adding both distribution of renaming over merge and communication in the style of ACP (see BAETEN AND V ERHOEF , 1995; BAETEN AND W EIJLAND, 1990) leads to an inconsistent theory. However, for the purpose of this thesis, only process algebras without communication are needed. Since distribution of renaming over the merge operator is often convenient in veri?cations, two new axioms, given in Table 2.4.22, are introduced. f : F; x, y : P; ρf (x ρf (x y) = ρf (x) ρf (y) y) = ρf (x) ρf (y) RNM1 RNM2
Table 2.4.22: Axioms for renaming, merge, and left merge. Note that Axiom RNM1 is derivable from Axioms M1 and RNM2. Hence, it might be more appropriate to refer to RNM1 as “Theorem RNM1” or “Property RNM1.” However, it is tedious to have to distinguish between RNM1 and the other axioms. Therefore, for the sake of convenience, it is referred to as “Axiom RNM1.” Axiom RNM2 is not derivable from the axioms of PAδ + RN as introduced in Table 2.4.19 on Page 40. However, by means of the inductive proof techniques introduced below, it is possible to show that it can be derived from the axioms of PAδ + RN for closed terms. Since inductive proofs are usually restricted to process algebras satisfying the elimination property, which not all process algebras in this thesis do, in the remainder, it is assumed that Axioms RNM1 and RNM2 are contained in the theory PA+RN. As a result, they are part of all extensions of PA+RN such as, for example, PAδ +RN. Note that the elimination and conservativeextension results given above are also valid for PA+RN and PAδ +RN including Axioms RNM1 and RNM2. The encapsulation operator. As mentioned earlier, the renaming operator can be used to de?ne the so-called encapsulation operator. The encapsulation operator makes it possible to block occurrences of certain actions in a given process. Blocking all occurrences of an action is done by renaming that action to δ. Let H be a set of actions from A. Let f H be a renaming function in F, which is de?ned as follows: f H (δ) = δ; for any a ∈ H , f H (a) = δ and for any a ∈ A\H , f H (a) = a. That is, the function f H renames all actions
2.4 Process Algebra
43
in H to δ and does not affect any other actions. Consequently, the resulting renaming operator ρf H exactly blocks all the actions in H . Since the operator ρf H plays an important role in many ACP-like process algebras, it has its own notation, ? H , and is usually referred to as the encapsulation operator. Table 2.4.23 lists the renaming-operator axioms for the encapsulation operator. Axiom RN1 is split into two conditional axioms D1 and D2. a : A ∪ {δ}; H :
P (A); x, y :
P; D1 D2 D3 D4 DM1 DM2
a ∈ H ? ? H (a) = a a ∈ H ? ? H (a) = δ ? H (x + y) = ? H (x) + ? H (y) ? H (x · y) = ? H (x) · ? H (y) ? H (x y) = ? H (x) ? H (y) ? H (x y) = ? H (x) ? H (y)
Table 2.4.23: The axioms for the encapsulation operator.
An operational semantics for PAδ +RN. The operational semantics for PAδ +RN contains no surprises. The processes are the closed PAδ +RN terms plus the special process √ √ √ . The transition relation ?→ ? (C (PAδ +RN) ∪ { }) × A × (C (PAδ +RN) ∪ { }) is the smallest relation satisfying the derivation rules given in Tables 2.4.5 on Page 36 and 2.4.24. In Table 2.4.5, of course, p, p , q, and q range over C (PAδ +RN). a : A; f : F; p, p , q, q : p ?→ p p q ?→ p p
a a a
C (PAδ +RN);
q ?→ q
a a
p ?→
a
a
√ p ?→
a
q ?→
a
a
√
q
a a
p q ?→ p q p ?→ p q ?→ p
f (a)
p q ?→ q p
a
p q ?→ p √
q
p ?→ p ,
f (a) = δ
ρf ( p) ?→ ρf ( p )
q ?→ q a √ p ?→ , f (a) = δ f (a) √ ρf ( p) ?→
Table 2.4.24: The transition relation for merge, left merge, and renaming. De?nition 2.4.25. (Operational semantics) The operational semantics (PAδ +RN) is √ √ the process space (C (PAδ+RN)∪{ }, A, ?→, { }) with strong bisimilarity as the equivalence relation. Property 2.4.26. (Congruence) Strong bisimilarity, ?, is a congruence for the operators of PAδ +RN.
S
44
Basic Concurrency Theory
AND
Proof. The property is a straightforward consequence of several results in (BAETEN V ERHOEF, 1995).
Theorem 2.4.27. (Soundness and completeness) For closed terms p, q ∈ C (PAδ +RN), PAδ +RN p = q ? (PAδ +RN) |= p = q .
2
S
Proof. Using the techniques of (BAETEN ward.
AND
V ERHOEF, 1995), the proof is straightfor-
2
Example 2.4.28. Consider again Example 2.2.5 on Page 6. The process depicted in Figure 2.2.4(d) on Page 7 can be speci?ed in PAδ+RN as follows: rcmd·pmat·(omat sprdy). In Example 2.4.7 on Page 37, a BPA term representing the same process has already been given. Since these two terms have the same semantics and PAδ +RN is complete for the operational semantics (PAδ +RN), it should be possible to derive the equality of the two terms from the axioms of PAδ +RN. Axioms M1 and M2 yield the desired result. It is interesting to compare the algebraic speci?cation given in this example to the P/T net given in Figure 2.3.3 on Page 18. There are two major differences between the two formalisms. P/T nets have a graphical representation and explicitly represent states. Process-algebraic terms have a purely symbolic representation and do not explicitly represent states.
S
Structural induction. A proof technique that is often used in process algebra is induction on the structure of basic terms. To illustrate this proof technique, this paragraph contains an example. In this thesis, many results in Chapter 4 are proved by means of structural induction. The example also shows why the elimination property is useful. Note that by de?nition the composition of two renaming functions yields another renaming function. Property 2.4.29. For any closed term p ∈ C (PAδ +RN) and f , g ∈ F, PAδ +RN ρf ?g( p) = ρf (ρg ( p)). Proof. It follows from Property 2.4.20 on Page 41 that there is a basic BPAδ term t such that PAδ +RN p = t. Hence, it suf?ces to show that ρf ?g(t) = ρf (ρg(t)). Given this result, it follows that PAδ +RN ρf ?g ( p) = ρf ?g (t) = ρf (ρg (t)) = ρf (ρg( p)). The proof is by induction on the structure of basic BPAδ terms. The symbol ≡ is used to denote syntactical identity of terms. i) Assume t ≡ δ or t ≡ a, for some action a ∈ A. It follows that RN1 RN1 RN1 ρf ?g (t) = f ? g(t) = f (g(t)) = ρf (g(t)) = ρf (ρg (t)). ii) Assume t ≡ a · s, for some action a ∈ A and basic term s ∈ B (BPAδ ). Then, Induction (2×) RN3 RN3 ρf ?g (a · s) = ρf ?g (a) · ρf ?g (s) = ρf (ρg (a)) · ρf (ρg (s)) = ρf (ρg(a) · ρg (s)) = ρf (ρg (a · s)). iii) Assume t ≡ u + v, for some basic terms u and v in B (BPAδ ). Then, Induction (2×) RN2 RN2 ρf ?g (u + v) = ρf ?g (u) + ρf ?g (v) = ρf (ρg (u)) + ρf (ρg (v)) = RN2 ρf (ρg(u) + ρg (v)) = ρf (ρg(u + v)).
RN3
2
2.4 Process Algebra
45
Standard concurrency and expansion. Table 2.4.30 introduces the so-called axioms of standard concurrency . These axioms state properties of the merge operator that are intuitively meaningful and often useful in veri?cations. The reason for not including them in the basic theory is that ASC2 is derivable from the axioms of PAδ+RN (see Property 2.4.31 below), whereas the other two are derivable for closed terms (see Property 2.4.32 below). The numbering of the axioms in Table 2.4.30 is not continuous, because a theory with both concurrency and communication has several more axioms of standard concurrency (see BAETEN AND V ERHOEF, 1995; BAETEN AND W EIJLAND, 1990). The axioms that are only meaningful in a context with communication are omitted. x, y, z : P; x y=y x (x y) z = x (y z) (x y) z = x (y z) ASC2 ASC4 ASC6
Table 2.4.30: The axioms of standard concurrency. Property 2.4.31. PAδ +RN ASC2.
Proof. It follows immediately from Axioms M1 and A1.
2
The proof of the following property shows another use of induction in process algebra, namely natural induction on the number of symbols in one or more terms. Just like structural induction, it is a technique that is often used in process algebra. It also shows again the usefulness of the elimination property. Property 2.4.32. For any p, q , and r in C (PAδ +RN), PAδ +RN ( p q) r = p (q r), ( p q) r = p (q r). Proof. It follows from Property 2.4.20 (Elimination) on Page 41 that it suf?ces to show the property for basic BPAδ terms. The proof is by (strong) natural induction on the number of symbols in the terms. For any closed term p ∈ C (PAδ+RN), let l( p) denote the number of symbols in p. Let n be some natural number at least three. The following two properties must be proven. (? s, t, u : s, t, u ∈ B (BPAδ ) : l(s) + l(t) + l(u) = n ? PAδ +RN ) and (? s, t, u : s, t, u ∈ B (BPAδ ) : l(s) + l(t) + l(u) = n ? PAδ +RN ). The induction hypothesis (IH) is as follows: (2.4.33) (s t) u=s (t u) (2.4.34) (s t) u = s (t u)
46
Basic Concurrency Theory
(? k : 3 ≤ k < n : (? s, t, u : s, t, u ∈ B (BPAδ ) : k = l(s) + l(t) + l(u) ? PAδ +RN (s t) u = s (t u), (s t) u = s (t u) ) ). Let s, t, and u be basic terms in B (BPAδ ) such that l(s) + l(t) + l(u) = n. The proof of Property 2.4.33 consists of a case analysis. i) Assume s (s · t) u ii) Assume s (a · v t) iii) Assume s ((v + w) (v + w) ≡ δ or s ≡ a, for some action a ∈ A. It easily follows that (s t) u = M3 M2 = s · (t u) = s (t u). ≡ a · v, for some action a ∈ A and basic term v ∈ B (BPAδ ). Then, M3 M3 IH M3 u = a · (v t) u = a · ((v t) u) = a · (v (t u)) = a · v (t u). ≡ v + w, for some basic terms v and w in B (BPAδ ). Then, M4(2×) IH(2×) M4 t) u = (v t) u + (w t) u = v (t u) + w (t u) = (t u).
M2
This completes the proof of Property 2.4.33. Since the proof does not depend on Property 2.4.34, Property 2.4.33 may be used to prove Property 2.4.34. The proof is as follows. (s t) u = { M1(2×) } (s t + t s) u + u (s t) = { M4, ASC2 } (s t) u + (t s) u + u (t s) = { Property 2.4.33 (3×) } s (t u) + t (s u) + (u t) s = { ASC2, Property 2.4.33 } s (t u) + (t u) s + (u t) s = { M4, M1(2×) } s (t u) The principle of strong natural induction implies that Properties 2.4.33 and 2.4.34 hold for all natural numbers at least three, which completes the proof of Property 2.4.32. A slightly different proof of Property 2.4.32, which does not use natural induction but structural induction, can be found in (BAETEN AND W EIJLAND, 1990). 2 For the interested reader, it is a nice exercise to prove by means of strong natural induction that, for closed PAδ+RN terms, Axiom RNM2 in Table 2.4.22 on Page 42 is derivable from the other axioms of theory PAδ +RN given in Table 2.4.19 on Page 40. It follows immediately from Properties 2.4.31 and 2.4.32 on the preceding page that the axioms of standard concurrency are valid in the operational semantics (PAδ +RN) given in De?nition 2.4.25 on Page 43.
S
Property 2.4.35. For any p, q, r ∈ C (PAδ +RN), (PAδ +RN) |= p q = q p, ( p q) r = p
S
(q r), ( p
q) r = p (q r).
2.4 Process Algebra Proof. Properties 2.4.31 and 2.4.32 and Theorem 2.4.27 (Soundness) on Page 44.
47
2
In PAδ +RN extended with the axioms of standard concurrency, it is possible to prove the following theorem, which is very useful for simplifying many calculations. It states that a parallel composition of k processes, where k is some natural number at least two, can be expanded into a choice of exactly those k alternatives where in each of the alternatives a different one of the k processes performs the initial action. For any associative binary process-algebra operator ?, some function f , some n ∈ IP, and operands x 0 , . . . , x n , the quanti?er notation (? i : 0 ≤ i ≤ n : f (x i )) is used as a shorthand notation for f (x 0) ? . . . ? f (x n ). Theorem 2.4.36. (Expansion) Let x 0 , . . . , x n be terms of sort P, where n ∈ IP. PAδ +RN+standard concurrency ( i : 0 ≤ i ≤ n : x i ) = (+ i : 0 ≤ i ≤ n : x i ( j : 0 ≤ j ≤ n ∧ j = i : x j )). Proof. The proof by induction on n is taken from (BAETEN base case, n = 1, is Axiom M1. Assume n > 1.
AND
W EIJLAND, 1990). The
( i : 0 ≤ i ≤ n : xi ) = { ASC6 (associativity of merge) } ( i : 0 ≤ i < n : xi ) xn = { M1 } ( i : 0 ≤ i < n : xi ) xn + xn ( i : 0 ≤ i < n : xi ) = { Induction } (+ i : 0 ≤ i < n : x i ( j : 0 ≤ j < n ∧ j = i : x j )) x n + xn ( i : 0 ≤ i < n : xi ) = { M4, ASC4 } (+ i : 0 ≤ i < n : x i (( j : 0 ≤ j < n ∧ j = i : x j ) x n )) + xn ( i : 0 ≤ i < n : xi ) = { ASC6 (associativity of merge); dummy change; calculus } (+ i : 0 ≤ i < n : x i ( j : 0 ≤ j ≤ n ∧ j = i : x j )) + xn ( j : 0 ≤ j ≤ n ∧ j = n : x j ) = { A2 (associativity of choice) } (+ i : 0 ≤ i ≤ n : x i ( j : 0 ≤ j ≤ n ∧ j = i : x j ))
2
2.4.4 Process Algebra with inaction, silent actions, and renaming
So far in this section, no distinction has been made between observable behavior and silent behavior. This subsection extends the process algebra PA δ +RN in such a way that it is possible to reason about processes with silent behavior. The equational theory PAτ +RN. The introduction of the silent action τ in the processδ algebraic setting developed so far, yields the process algebra PAτ + RN. The acronym δ PAτ+RN is an abbreviation of Process Algebra with inaction, silent actions, and renaming. δ
48 PAτ +RN(A) δ PAδ +RN(A) τ : A x, y, z : P; x ·τ = x x · (τ · (y + z) + y) = x · (y + z)
Basic Concurrency Theory
B1 B2
Table 2.4.37: The process algebra PAτ +RN. δ Let A be some set of action labels. Table 2.4.37 gives the theory PAτ +RN. Note that the δ second entry of Table 2.4.37 introduces the special action τ . Axioms B1 and B2 are the basis for an axiomatization of rooted branching bisimilarity (see VAN G LABBEEK AND W EIJLAND, 1996). These axioms are, of course, chosen because rooted branching bisimilarity is the equivalence used in the operational semantics given below. Together, B1 and B2 state that it is allowed to remove a silent action provided that it does not enforce an internal choice. Example 2.4.38. Consider two versions of a production unit which are speci?ed as follows: rcmd · (τ · (pmat1 + pmat2)) · omat and rcmd · (τ · pmat1 + pmat2) · omat. The ?rst production unit decides after some internal computations what source of input material to use. Clearly, the environment cannot distinguish it from a unit with behavior rcmd · (pmat1 + pmat2) · omat. In PAτ +RN, the equality follows simply from Axioms δ A5 and B1. The second production unit behaves slightly different. Based on some internal computations, it may decide autonomously that it wants to get input from source one. Thus, it removes the option to get input from the other source. The environment can detect this internal choice when input source one is left empty. When making enough runs with the unit, it may get stuck in a deadlock once in a while. The algebra PAτ +RN does δ not contain any axioms to remove the silent action in the unit’s speci?cation. In the previous subsection, renaming functions have been introduced. In the presence of silent actions, renaming functions must satisfy an additional requirement. Since silent actions are internal and unobservable, they cannot be renamed. That is, for any f in the sort of renaming functions F, f (τ ) must be τ . One of the consequences is that silent actions cannot be blocked. This implies that the de?nition of the encapsulation operator when de?ned in PAτ +RN must be adapted accordingly. The axioms in Table 2.4.23 on Page 43 δ remain the same, but H now ranges over P (A\{τ }). Silent actions can be used to de?ne a whole range of new process algebras. The most interesting ones are PAτ , PAτ +RN, and PAτ . By now, the exact de?nition of these theoδ ries should need no further elaboration. The following property states several elimination results. Property 2.4.39. (Elimination) i) For any closed term p ∈ C (X), where X is a process algebra in {PAτ , PAτ +RN}, there is a basic term t ∈ B (BPA), such that X p = t .
2.4 Process Algebra
49
ii) For any closed term p ∈ C (X), where X is a process algebra in {PAτ , PAτ +RN}, δ δ there is a basic term t ∈ B (BPAδ ), such that X p = t . Proof. The proof is identical to the proof of Property 2.4.20 on Page 41. The introduction of the silent action τ has no effect. 2 In addition to the above elimination results, various conservativity results can be proved. It goes beyond the scope of this chapter to present all these results. Basically, extending a theory with any of the operators given so far yields a conservative extension. The abstraction operator. The process algebra PAτ+RN allows us to specify processes δ with internal behavior. However, does it also provide an abstraction facility? That is, is it possible to hide certain behavior of a process from the environment? The answer is af?rmative. Hiding the occurrence of an action is established by renaming that action occurrence to τ . This means that the renaming operator can be used to de?ne an abstraction operator. The de?nition is very similar to the de?nition of the encapsulation operator in the previous subsection. Let I be a set of actions from A\{τ }. Let f I be a renaming function in F, which is de?ned as follows: f I (δ) = δ; for any a ∈ I , f I (a) = τ and for any a ∈ A\I , f I (a) = a. Note that this de?nition satis?es the requirement that f I (τ ) = τ . Function f I renames exactly all actions in I to τ . The resulting renaming operator ρf I thus effectively hides the actions in I from the environment. Because of its importance in process algebra, the operator ρf I is usually denoted τ I , and is referred to as the abstraction operator. Table 2.4.40 lists the renaming-operator axioms for the abstraction operator. a : A ∪ {δ}; I :
P (A\{τ }); x, y :
P; TI1 TI2 TI3 TI4 TIM1 TIM2
a ∈ I ? τ I (a) = a a ∈ I ? τ I (a) = τ τ I (x + y) = τ I (x) + τ I (y) τ I (x · y) = τ I (x) · τ I (y) τ I (x y) = τ I (x) τ I (y) τ I (x y) = τ I (x) τ I (y)
Table 2.4.40: The axioms for the abstraction operator. An operational semantics for PAτ + RN. The processes in the operational semantics δ √ for PAτ + RN are the closed PAτ + RN terms√ extended with the special process . The δ δ √ transition relation ?→ ? (C (PAτ +RN) ∪ { }) × A × (C (PAτ +RN) ∪ { }) is identical δ δ to the transition relation for PAδ + RN. That is, it is the smallest relation satisfying the derivation rules given in Tables 2.4.5 on Page 36 and 2.4.24 on Page 43, where in both tables p, p , q, and q range over C (PAτ +RN). The only difference with the operational δ semantics for PAδ +RN is that rooted branching bisimilarity is chosen as the equivalence relation.
50
Basic Concurrency Theory
De?nition 2.4.41. (Operational semantics) The √ operational semantics (PAτ +RN) is δ √ τ the process space (C (PAδ +RN) ∪ { }, A, ?→ , { }) with rooted branching bisimilarity as the equivalence relation. As mentioned in Section 2.2.3, the root condition in the de?nition of rooted branching bisimilarity guarantees that the equivalence is a congruence for all the algebraic operators. Property 2.4.42. (Congruence) Rooted branching bisimilarity, ?rb, is a congruence for the operators of PAτ +RN. δ Proof. Let p1 , p2 , q1 , q2 be closed PAτ + RN terms. Let R1 and R2 be rooted branchδ ing bisimulations between p1 and q1 , and p2 and q2 respectively. It must be shown that there exist rooted branching bisimulations Q1 , . . . , Q5 , such that ( p1 + p2)Q1(q1 + q2), ( p1 · p2)Q2(q1 · q2), ( p1 p2)Q3(q1 q2 ), ( p1 p2)Q4(q1 q2 ), and, such that, for any renaming function f ∈ F, ρf ( p1)Q5ρf (q1). The ?ve relations are given below. It is straightforward to verify that the relations are indeed rooted branching bisimulations. To avoid unnecessarily complex formulas, some√ notations are introduced. Let, for any √ √ √ √ √ p= p = p, and, for any f ∈ F, ρf ( ) = . p ∈ C (PAτ +RN) ∪ { }, · p = p, δ Q1 = R1 ∪ R2 ∪ {( p1 + p2, q1 + q2)}, Q2 = R2 ∪ {( p · p2 , q · q2) | pR1 q}, Q3 = {( p p , q q ) | pR1 q ∧ p R2 q }, Q4 = Q3 ∪ {( p1 p2 , q1 q2)}, Q5 = {(ρf ( p), ρf (q)) | pR1 q ∧ f ∈ F}.
S
2
τ a
b
?
a
b
Figure 2.4.43: Branching bisimilarity is not a congruence for the choice operator. Example 2.4.44. The reason for introducing the root condition in Section 2.2.3 was that branching bisimilarity is not a congruence for the algebraic choice operator, as the following example shows. Let a and b be two different actions in A. Processes τ · a and a are branching bisimilar. Figure 2.2.17 on Page 12 shows a branching bisimulation between these two processes. Clearly, also process b is branching bisimilar to itself. However, τ · a + b is not branching bisimilar to a + b. Figure 2.4.43 shows the problem when trying to construct a branching bisimulation. Process τ · a + b has a state in which only a is possible, whereas a + b does not have such a state. The problem does not occur for rooted branching bisimilarity, because τ · a and a are not rooted branching bisimilar (see also Example 2.2.18 on Page 12).
2.4 Process Algebra
51
Theorem 2.4.45. (Soundness and completeness) For closed terms p, q ∈ C (PAτ +RN), δ PAτ +RN p = q ? (PAτ +RN) |= p = q . δ δ
S
Proof. The theorem is a fairly straightforward result of Property 2.4.42, the completeness of BPAτ for rooted branching bisimilarity (see VAN G LABBEEK AND W EIJLAND, 1996) and the proof techniques in (BAETEN AND V ERHOEF, 1995). 2 Example 2.4.46. Consider Examples 2.2.12 on Page 10 and 2.2.20 on Page 13. The process in Figure 2.2.11(b) on Page 9 can be speci?ed in PAτ+RN as follows: rcmd·(pmat1 + δ pmat2) ·omat (see also Example 2.4.8 on Page 37). In Example 2.2.20, the claim has been made that the process of Figure 2.2.19(a) on Page 13 is the result of abstracting away the processing actions pmat1 and pmat2 in the process of Figure 2.2.11(b). The process of Figure 2.2.19(a) is speci?ed by the PAτ +RN term rcmd · τ · omat. In Example 2.2.20, it has δ also been shown that the resulting observable behavior is the process in Figure 2.2.19(b), which is speci?ed in PAτ +RN as rcmd ·omat. Using the abstraction operator of PAτ +RN, δ δ the abstraction of actions can be formalized and it is possible to calculate the resulting observable behavior. Let I be equal to {pmat1 , pmat2 }. The following derivation shows the desired results. τ I (rcmd · (pmat1 + pmat2 ) · omat) = { TI3,TI4 (repeatedly) } τ I (rcmd) · (τ I (pmat1 ) + τ I (pmat2 )) · τ I (omat) = { TI1,TI2 (repeatedly) } rcmd · (τ + τ ) · omat = { A3 } rcmd · τ · omat = { B1 } rcmd · omat Structural induction, standard concurrency, and expansion. Since PAτ +RN has an δ elimination result (Property 2.4.39 on Page 48), structural induction in PAτ + RN goes δ in exactly the same way as in Section 2.4.3, where an example in PAδ +RN is given. The extension of the theory PAτ +RN with the axioms of standard concurrency is also identical δ to the extension of PAδ +RN with standard concurrency. As a result, PAτ +RN has the δ same expansion theorem as the one given in Theorem 2.4.36 on Page 47.
2.4.5 Iteration in process algebra
This subsection introduces a simple form of recursion into process algebra, namely iteration, in the form of the binary Kleene star. The binary Kleene star is the original star operator as introduced in (K LEENE, 1956). The binary Kleene star is much simpler than general recursion (see BAETEN AND V ERHOEF , 1995; BAETEN AND W EIJLAND, 1990).
52
Basic Concurrency Theory
The equational theory PAτ ? + RN. Table 2.4.47 gives the theory PAτ ? + RN, Process δ δ Algebra with inaction, silent actions, renaming, and iteration. PAτ ? +RN(A) δ PAτ +RN(A) δ : P×P→ P f : F; x, y, z : P; x ? y = x · (x ? y) + y x ? (y · z) = (x ? y) · z x ? (y · ((x + y) ? z) + z) = (x + y) ? z ρf (x ? y) = ρf (x) ? ρf (y) BKS1 BKS2 BKS3 BKS4
?
Table 2.4.47: The process algebra PAτ ? +RN. δ The binary Kleene star ? was introduced in process algebra in (B ERGSTRA , B ETHKE , AND P ONSE, 1994), where also the axioms BKS1 through BKS4 appear. ((B ERGSTRA , B ETHKE , AND P ONSE, 1994) gives variants of BKS4 for the encapsulation and abstraction operators.) Axiom BKS3 is a sophisticated axiom which is needed to get a complete axiomatization of bisimilarity. Below, completeness is discussed in more detail. It is possible to extend any of the other theories given so far with the binary Kleene star. In case the basic theory does not contain the renaming operator, BKS4 is omitted. The binary Kleene star has the same binding priority as sequential composition. A disadvantage of iteration is that elimination of the binary Kleene star from closed terms is not possible anymore (see BAETEN AND V ERHOEF, 1995). As a result, inductive proofs as given in the Section 2.4.3 do not carry over to a theory containing the binary Kleene star. One consequence is that the axioms of standard concurrency ASC4 and ASC6 are no longer derivable for closed terms (see Property 2.4.32 on Page 45). Note that they can still be valid in some given operational semantics (see Property 2.4.35 on Page 46). An operational semantics for PAτ ? +RN. The processes in the operational semantics δ √ for PAτ ? +RN are the closed PAτ ? +RN terms extended with the special process . The δ δ √ √ transition relation ?→ ? (C (PAτ ? +RN) ∪ { }) × A × (C (PAτ ? +RN) ∪ { }) is the δ δ smallest relation satisfying the derivation rules given in Tables 2.4.5 on Page 36, 2.4.24 on Page 43, and 2.4.48 on the next page, where in all tables p, p , q, and q range over C (PAτ ? +RN). δ De?nition 2.4.49. (Operational semantics) The operational semantics (PAτ ? +RN) is δ √ √ the process space (C (PAτ ? +RN) ∪ { }, A, ?→ , { }) with rooted branching bisimilarity δ as the equivalence relation. Example 2.4.50. In theory PAτ ? +RN, it is ?nally possible to specify the process depicted δ in Figure 2.2.4 (c) on Page 7: (rcmd · pmat · omat ) ? δ. The non-terminating iteration is speci?ed using the binary Kleene star in combination with the inaction constant δ.
S
2.4 Process Algebra a : A; p, p , q, q : p ?→ p p ? q ?→ p · ( p ? q)
a a
53
C (PAτ ? +RN); δ
q ?→ q p ? q ?→ q
a a
p ?→
a
a
√
q ?→
a
a
√ √
p ? q ?→ p ? q
p ? q ?→
Table 2.4.48: The transition relation for the binary Kleene star. Property 2.4.51. (Congruence) Rooted branching bisimilarity, ?rb, is a congruence for the operators of PAτ ? +RN. δ Proof. For all operators of PAτ ?+RN except the binary Kleene star, the proof is identical to δ the proof of Property 2.4.42 on Page 50. Let R1 and R2 be rooted branching bisimulations between p1 and q1, and p2 and q2 , respectively, where p1 , p2 , q1 , and q2 are closed PAτ ?+ δ √ √ RN terms. Let, for any p ∈ C (PAτ ? +RN) ∪ { }, · p denote p. It is straightforward δ to verify that R2 ∪ {( p1 ? p2 , q1 ? q2)} ∪ {( p · ( p1 ? p2 ), q · (q1 ? q2 )) | pR1 q} is a rooted branching bisimulation between p1 ? p2 and q1 ? q2. 2 Theorem 2.4.52. (Soundness) For any closed terms p, q ∈ C (PAτ ? +RN), δ PAτ ? +RN p = q ? (PAτ ? +RN) |= p = q . δ δ
S
Proof. Since rooted branching bisimilarity is a congruence for the operators of PAτ ?+RN, δ it suf?ces to show the validity of each of the axioms. It is not dif?cult to construct a rooted branching bisimulation for each case. 2 There is no completeness result for PAτ ? +RN. On the contrary, the results of (S EWELL, δ 1994) show that in a setting with the binary Kleene star and inaction, no ?nite complete axiomatization for strong bisimilarity exists. The techniques of (S EWELL, 1994) can also be used to prove that in a context with the binary Kleene star and silent actions no ?nite complete axiomatization exists for (rooted) branching bisimilarity. The only completeness result for the binary Kleene star that to date exists is a result proved in (FOKKINK AND Z ANTEMA, 1994). There, it is shown that BPA? , Basic Process Algebra with the binary Kleene star, is a sound and complete axiomatization for strong bisimilarity on closed terms. In addition, there are several completeness results for restricted forms of the binary Kleene star (see VAN G LABBEEK, 1997, for an overview). Standard concurrency and expansion. Although the axioms of standard concurrency ASC4 and ASC6 are not derivable from the axioms of PAτ ? + RN, they are valid in the δ semantics (PAτ ? +RN). Axiom ASC2 is still derivable from PAτ ? +RN, and hence also δ δ valid in (PAτ ? +RN). δ
Property 2.4.53. For any p, q, r ∈ C (PAτ ? +RN), δ (PAτ ? +RN) |= p q = q p, ( p q) r = p δ
S
S
S
(q r), ( p q) r = p (q r).
Proof. Property 2.4.31 on Page 45, adapted for PAτ ? +RN, and Theorem 2.4.52 (Soundδ ness) immediately yield that (PAτ ? +RN) |= p q = q p. The following relation is δ
S
54
Basic Concurrency Theory (q r) and between
a rooted branching bisimulation both between ( p q) r and p ( p q) r and p (q r): {(( p q) r, p (q r)) | p, q, r ∈ C (PAτ ? +RN)} δ ∪ {(( p q) r, p (q r)) | p, q, r ∈ C (PAτ ? +RN)} δ √ ∪ {( p, p) | p ∈ C (PAτ ? +RN) ∪ { }}. δ
2
A consequence of Property 2.4.53 is that PAτ ? +RN+standard concurrency has the same δ expansion theorem as given in Theorem 2.4.36 on Page 47. The addition of the binary Kleene star does not in?uence the proof of this theorem. Fairness. In a theory which includes both recursion and silent actions, it is often useful to have a fairness principle. A simple form of fairness means that a process cannot always choose to do an internal action if it also has other options. For the binary Kleene star, this form of fairness can be expressed by a single axiom, namely the Fair Iteration Rule (FIR) given in Table 2.4.54. It simply states that a sequence of silent actions cannot be in?nitely long. For a treatment of other, more sophisticated forms of fairness in process algebra, the reader is referred to (BAETEN AND W EIJLAND, 1990). x : P; τ ?x = x +τ ·x FIR
Table 2.4.54: The Fair Iteration Rule. The Fair Iteration Rule is valid in the operational semantics tion 2.4.49 on Page 52. Property 2.4.55. For any p ∈ C (PAτ ? +RN), δ (PAτ ? +RN) |= τ ? p = p + τ · p. δ Proof. For any p ∈ C (PAτ ?+RN), the following relation is a rooted branching bisimulation δ between τ ? p and p + τ · p. {(τ ? p, p + τ · p) | p ∈ C (PAτ ? +RN)} δ √ ∪ {(τ ? p, p) | p ∈ C (PAτ ? +RN)} ∪ {( p, p) | p ∈ C (PAτ ? +RN) ∪ { }}. δ δ
S (PA
τ? δ +RN)
of De?ni-
S
2
Recursive equations. Since often veri?cations in process algebra result in an equation that is recursive in some given process, it is useful to have a principle that gives solutions for such recursive equations. The Recursive Speci?cation Principle for the binary Kleene star (RSP? ) given in Table 2.4.57 on the next page is a derivation rule which gives a solution in terms of the binary Kleene star for some restricted set of recursive equations. Axiom RSP? uses the notion of a guard which is de?ned as follows. Informally, a term is a guard if it cannot terminate successfully without performing at least one observable action.
2.4 Process Algebra
55
De?nition 2.4.56. (Guard) A closed PAτ ?+RN term p is a guard if and only if, using the δ axioms of PAτ ? +RN, it can be rewritten into an equivalent term of any of the following δ forms: i) δ or a, for any a ∈ A\{τ }; ii) q · r, for closed PAτ ? +RN terms q and r where either q or r or both are guards; δ iii) q + r, for any closed PAτ ? +RN terms q and r where both q and r are guards. δ
x, y, z : P; x = y · x + z, y is a guard x = y?z RSP?
Table 2.4.57: The Recursive Speci?cation Principle for the binary Kleene star.
Example 2.4.58. De?nition 2.4.56 states that silent actions cannot act as guards. The following example shows the reason for this restriction. Let a and b be two different actions in A not equal to τ . Axioms A5, A6, and B1 easily yield that τ · a = τ · (τ · a) + δ and τ · b = τ · (τ · b) + δ. Assume that the silent action is a guard. Then, it follows from RSP? that τ · a = τ ? δ and τ · b = τ ? δ. Hence, τ · a = τ · b, which is clearly a contradiction when a and b are different. The derivation rule RSP? is valid in the operational semantics
S (PA
τ? δ +RN).
Property 2.4.59. For any p, q, r ∈ C (PAτ ? +RN) such that q is a guard, δ (PAτ ? +RN) |= p = q · p + r ? (PAτ ? +RN) |= p = q ? r . δ δ
S
S
Proof. Let p, q, and r be closed PAτ ? +RN terms such that q is a guard; let R be a rooted δ branching bisimulation between p and q· p +r. It can be shown that the following relation which uses the transitive closure of R, denoted R+ , is a rooted branching bisimulation between p and q ? r: √ {( p, q ? r)} ∪ R+ ∪ {(s, q ? r) | s ∈ C (PAτ ? +RN) ∪ { } ∧ s R+ p} δ √ ∪ {(s, t · (q ? r)) | s ∈ C (PAτ ? +RN) ∪ { } ∧ t ∈ C (PAτ ? +RN) ∧ s R+ t · p}. δ δ An explanation of this relation and the details of the proof can be found in (BASTEN AND VOORHOEVE , 1995a). 2 Note that in the above proof a rooted branching bisimulation is constructed explicitly. In a process-algebraic theory with general recursion another proof strategy could be followed, namely the one used in (BAETEN AND W EIJLAND, 1990) and (BAETEN AND V ERHOEF, 1995) to show that an operational semantics satis?es the general Recursive Speci?cation Principle RSP. Any semantics satisfying RSP also satis?es RSP? .
56
Basic Concurrency Theory
An example veri?cation. To clarify the use of FIR and RSP? , this paragraph contains an example veri?cation using these two axioms. The calculations show how to verify an implementation of a system against its speci?cation. The veri?cation is an example of a typical application of process algebra. Assume that the manager of a factory for the production of certain goods wants to have a production unit satisfying the following simple speci?cation. PU spec = (imat · omat) ? δ. (2.4.60)
Speci?cation PU spec states that the production unit performs two actions that are visible to the environment. First, it starts with getting input material (action imat). Second, after it has internally processed the input, it produces output material (omat). Of course, the input and output should satisfy certain requirements, but speci?cation PU spec abstracts away from such details. The iteration in the speci?cation means that the unit should repeat the above two steps inde?nitely (see Axioms BKS1 and A6). A supplier has a production unit PU available of which the behavior can be described as follows. PU = (imat · (ppmat ? fmat1 ) · (pmat1 pmat2 ) · omat · imat · (ppmat ? fmat2) · (pmat1 pmat2 ) · omat ) ? δ. (2.4.61)
As required by the speci?cation, unit PU performs a non-terminating iteration. Internally, the unit has two trays for unprocessed material. Each time the unit receives input material (imat), it performs a number of preprocessing steps (ppmat) and forwards the material to one of the two trays (fmat1, fmat2). Each processing step, the unit alternates between the two trays, starting with the ?rst one. The number of preprocessing steps, if any at all, is always limited. The unit executes two processing actions on input material (pmat1 and pmat2). These processing actions can be done in parallel. If both processing actions are completed, the unit produces output material (omat). The supplier claims that the production unit satis?es the speci?cation PU spec of Property 2.4.60. Of course, the factory manager wants to verify the claim. Since she is pro?cient in process algebra, she quickly performs a few calculations. Let I be the set of actions {ppmat, fmat1 , fmat2 , pmat1 , pmat2 }. Hiding these actions in the behavior PU should yield speci?cation PU spec . Formally, the proof requirement is speci?ed as follows. τ I (PU) = PU spec. (2.4.62) The following derivation hides the actions in I in the behavior PU and eliminates the resulting silent steps. Note that it is allowed to use Axiom FIR because the number of preprocessing actions is limited. τ I (PU) = { De?nition 2.4.61; TI1, 2, 4, TIM1, BKS4 (repeatedly) } (imat · (τ ? τ ) · (τ τ ) · omat · imat · (τ ? τ ) · (τ = { FIR (2×), M1, M2(2×) }
τ ) · omat) ? δ
2.5 Conclusions (imat · (τ + τ · τ ) · (τ · τ + τ · τ ) · omat · imat · (τ + τ · τ ) · (τ · τ + τ · τ ) · omat )?δ = { B1, A3 (repeatedly) } (imat · omat · imat · omat) ? δ Summarizing, τ I (PU) = (imat · omat · imat · omat) ? δ.
57
(2.4.63)
This is almost the desired result. Informally, the non-terminating iteration of some actions should be equal to the non-terminating iteration of twice these actions. Let p ∈ C (PAτ ? + δ RN) be a guard (see De?nition 2.4.56 on Page 55). { BKS1(2×) } p · ( p · ( p ? δ) + δ) + δ = { A6, A5 } ( p · p) · ( p ? δ) + δ Hence, it follows from RSP? that p ? δ = ( p · p) ? δ. (2.4.64) = p?δ
Property 2.4.64 proves the informal claim made above. Applying Property 2.4.64 to Result 2.4.63 easily yields the proof requirement of Property 2.4.62 on the preceding page. τ I (PU) = PU spec. Hence, the factory manager is satis?ed and decides to take the production unit. (2.4.65)
2.5 Conclusions
This chapter has given an introduction to basic concurrency theory. None of the material is new in itself. The main purpose of this chapter is to present it in a common framework. Thus, it provides a basis for the remaining chapters of this thesis. Section 2.2 has introduced a very natural way to describe concurrent systems, namely transition systems. The notion of an operational semantics has been de?ned. This notion is elementary to the remainder of this thesis. Any formalism for describing concurrent systems introduced in this thesis is given a meaning in the framework of transition systems by providing it with an operational semantics. In Section 2.3, the formalism of Place/Transition nets has been introduced. This formalism is a member of the large class of formalisms for modeling concurrent systems called Petri nets. Petri nets combine an intuitive graphical representation with strong analysis techniques. A class of Petri nets that is particularly suitable for the ef?cient analysis of properties of concurrent systems is the class of free-choice P/T nets.
58
Basic Concurrency Theory
Section 2.4 has given an introduction to ACP-style process algebras. Process algebras are symbolic formalisms for describing and analyzing concurrent-system behavior. They are particularly useful for the comparison of behaviors, for example, to verify an implementation against a speci?cation. The remainder of this thesis studies topics combining and integrating Petri nets and process algebra, using transition systems as a common framework.
3
Algebraic Veri?cation of Modular Nets
3.1 Introduction
An essential property of any formalism for modeling and analyzing complex concurrent systems is compositionality. A formalism is compositional if it allows the system designer to structure a formal model of a system into component models of subsystems in such a way that properties of the system as a whole can be derived from the properties of the components. Unfortunately, labeled P/T nets as introduced in Chapter 2 are not suited for compositional design. They lack a structuring mechanism to divide models of concurrent systems into components. Process algebra, on the other hand, supports compositional design of concurrent systems. When the behavior of the subsystems of a concurrent system is described by means of algebraic terms, the behavior of the entire system can be described by composing these terms, using the suitable operators in the process algebra. The goal of this chapter is to show how Petri nets and process algebra can be integrated into a formalism supporting compositional design of concurrent systems, combining the strengths of both formalisms. The resulting formalism is such that the combination of Petri nets and process algebra provides a better understanding of the system under development than any of the two formalisms in isolation. The chapter is organized as follows. Section 3.2 brie?y sketches a design method that provides the framework for the underlying integrated formalism. The design method emphasizes the strengths of both Petri nets and process algebra. Sections 3.3 through 3.6 present the formalism itself. The notion of modular P/T nets is introduced. Several algebraic semantics of modular P/T nets are given that allow a system designer to verify their behavior against an algebraic speci?cation. The theory is a revised and improved version of the theory in (BASTEN AND VOORHOEVE , 1995b). To validate the design method and the underlying theory, in Sections 3.7 and 3.8, the results of two case studies are discussed. Finally, Section 3.9 presents some conclusions and open problems. It also contains a discussion of related work. 59
60
Algebraic Veri?cation of Modular Nets
3.2 Design Method
First of all, it should be noted that it is not the intention of this section to present a complete design method that can be used for the design of real-world concurrent systems. The goal is merely to provide a framework for the formalism presented in the remaining sections. In concurrent systems, the order in which communications between different parts of the system occur is often crucial. Petri nets and process algebra are both formalisms that focus on the dynamic behavior of systems. Therefore, the theory presented in this chapter is particularly useful for the design of concurrent systems where the communication protocol between the various parts of the system plays an important role. It is not very well suited for data-oriented applications or applications where most of the computations are performed by a single system component without much communication with other parts of the system. This does not mean that issues related to the data structures being used in the implementation of the system and the correctness of computations local to some speci?c part of the system are less important. However, other formalisms, such as assertional reasoning based on predicate logic and model checking techniques, are more useful for those purposes. Petri nets and process algebra complement each other very well. Petri nets have an intuitive, graphical representation and are well suited to describe the dynamic behavior of a system including the states in which the system can be. Colored Petri nets, in particular, provide a strong formalism for modeling concurrent systems. Petri nets are very useful for purposes of system validation and simulation. In addition, the analysis techniques that are available for Petri nets can be used to show that a system satis?es some given property. Process algebra, on the other hand, is a compositional, purely symbolic formalism, designed to compare the dynamic behavior of different systems. By applying term rewriting techniques and equational reasoning, it can be veri?ed whether an implementation satis?es a given speci?cation, where both speci?cation and implementation are algebraic terms. Based on the above observations, a very simple design method is introduced that consists of four separate activities. Each activity is explained in more detail below. i) Specify the behavior or behavioral properties of the concurrent system. ii) Construct a (colored-)Petri-net model of the system. iii) Use simulation to validate the speci?cation and to test whether the Petri net conforms to the speci?cation. iv) Verify the correctness of the net with respect to its behavioral speci?cation using process algebra. Behavioral speci?cation. In the early stages of system design, it is useful to specify in a concise way the order in which the actions in a concurrent system can occur. A process algebra or a simple speci?cation language based on process-algebraic principles is well suited for this purpose. In this step, only behavioral properties are speci?ed. Other details of the system are addressed when designing the Petri-net model of the system.
3.2 Design Method
61
Petri-net model. Once a designer who is familiar with the method of this chapter has a clear understanding of the dynamic behavior of a system, he or she usually has no dif?culty to construct a Petri net of which the behavior conforms to the speci?cation of the system. For any non-trivial concurrent system, many more aspects than the order in which actions may occur are important. Examples of such aspects are the timing of actions, the data structures that are used in the implementation, and the algorithms needed for the local computations. These aspects are usually addressed in this stage of the design process. This means that, in general, a colored-Petri-net formalism is used to de?ne the Petri-net model of the system. Simulation. The Petri-net model of a concurrent system can be simulated using tools such as ExSpect (ASPT, 1994), Design/CPN (J ENSEN ET AL ., 1991), or PEP (B EST AND G RAHLMANN, 1995). The speci?cation and the net model can be validated and corrected, if necessary. Simulation is an excellent means to discover the more obvious mistakes in both the behavioral speci?cation and the Petri-net model. However, by means of simulation only, it is usually impossible to guarantee that all errors are discovered. Note that simulation can also be used for other purposes, such as performance analysis. Although performance analysis may be very useful for many applications, it is not an important activity in the design method proposed here, which focuses on behavioral correctness. Veri?cation. In the veri?cation phase, the Petri-net model and, if necessary, also the behavioral speci?cation are formally translated into a process-algebra expression. By means of term rewriting techniques and equational reasoning, it is veri?ed whether the behavior of the net conforms to its speci?cation. This step is useful to discover the more subtle mistakes in a speci?cation and the corresponding Petri net. The presentation of the four activities suggests an ordering. In an ideal situation, they are indeed applied in the order presented. However, the experience of the case studies presented in Sections 3.7 and 3.8 shows that, in practice, they are seldom clearly separated. Systems design is a complex process where one often works on several of the four activities simultaneously. If one discovers an error during one step, it may be necessary to redo some of the work in other steps. Even more important, if one follows a top-down design strategy, it is possible to ?rst design and verify a system on a high level of abstraction before adding more detail. When adding a detailed level of abstraction, the design cycle is repeated. The next four sections present basic theoretical results, integrating Petri nets and process algebra, that are needed in the modeling and veri?cation phases of the above design method. Although in practice, a colored-Petri-net formalism is needed, the results in this chapter are restricted to an uncolored formalism, called modular P/T nets. Modular P/T nets extend P/T nets as de?ned in Chapter 2 with a hierarchy construct. As mentioned, such a construct is essential in compositional design. The extension of the theory to colored Petri nets remains for future investigation. In Sections 3.7 and 3.8, where two case
62
Algebraic Veri?cation of Modular Nets
studies are discussed, a very simple language for behavioral speci?cations is introduced. In these sections, the role of simulation in the method is also explained in more detail.
3.3 P/T-Net Components
The basis of a modular P/T net is the so-called P/T-net component. P/T-net components are the building blocks used to construct a modular P/T net. Figure 3.3.1 shows an example of a P/T-net component. P/T-net components strongly resemble standard P/T nets as introduced in Chapter 2. The only difference is that, for P/T-net components, the set of places is divided into internal places and pins. The graphical representation of a P/T-net component uses a dashed box to divide the set of places into internal places and pins. Pins are depicted as double circles. The idea is that pins are connectors to the environment. The environment can interact with the P/T-net component by removing tokens from or putting tokens into its pins. Since transition labels do not play an important role in the theory of this chapter, unlabeled P/T nets, as de?ned in De?nition 2.3.39 on Page 26, are taken as the starting point for this chapter. The extension with transition labels is straightforward. cmd rdy rcmd tcmd imt
3
prdy
sprdy bsy empty tprdy omt
pmat pmt
omat
Figure 3.3.1: The graphical representation of a P/T-net component. De?nition 3.3.2. (P/T-net component) A P/T-net component is a pair C = (N, I ), where N = (P, T , F, W ) is a P/T net as de?ned in De?nition 2.3.39 on Page 26 and where I ? P is the set of internal places. For any P/T-net component C, the set P\I is the set of pins of the component, also called the interface of the component, denoted ifc(C). For any transition t ∈ T , its bag of internal input places iit is de?ned as it |` I ; its bag of observable input places oit is de?ned as it |`ifc(C). The bags of internal and observable output places, denoted iot and oot, respectively, are de?ned likewise. Example 3.3.3. Figure 3.3.1 shows an example of a P/T-net component modeling a production unit. Its interface is the set of pins {cmd, prdy, imt, omt}. The bag of input places
3.3 P/T-Net Components
63
of transition rcmd, ircmd, is equal to [cmd, rdy]; its bag of output places orcmd is equal to [tcmd, bsy]. Consequently, its internal input places iircmd and its internal output places iorcmd are the bags [rdy] and [tcmd, bsy], respectively; its bag of observable input places oircmd is the singleton bag [cmd] and the bag of its observable output places oorcmd is the empty bag 0. De?nition 3.3.4. (Marked P/T-net component) A marked P/T-net component is a triple (N, I, s), where (N, I ) is a P/T-net component as de?ned above and where s is a bag over I denoting the internal marking of the net component. The set of all marked P/T-net components is denoted .
C
Pins are not considered in the marking of a P/T-net component, because the goal is to determine the behavior of such a component under the assumption that the environment is responsible for consuming tokens from and producing tokens on pins. It is assumed that the environment has always tokens available when they are needed by a P/T-net component. It is also assumed that the environment is always willing to receive any tokens that the component might produce. Therefore, transition enabling is de?ned in such a way that it does not depend on pins. De?nition 3.3.5. (Transition enabling) Let (N, I, s) be a marked P/T-net component, where N = (P, T , F, W ). A transition t ∈ T is enabled, denoted (N, I, s)[t , if and only if each internal input place p of t contains at least as many tokens as its cardinality in iit. That is, (N, I, s)[t ? iit ≤ s. Example 3.3.6. Consider again the marked P/T-net component in Figure 3.3.1 on the facing page. Its pins cmd, prdy, imt, and omt do not contain any tokens, since only internal places can be marked in a P/T-net component. In the initial marking depicted in the ?gure, only transition rcmd is enabled. The ?ring rule for P/T-net components is very similar to the ?ring rule for labeled P/T nets (see De?nition 2.3.7 on Page 18). There are two differences. The ?rst one is that the ?ring rule for P/T-net components only affects tokens in internal places. The second difference is the action function. As already mentioned, the environment and a P/T-net component interact via the pins of the component. From the point of view of the environment, it is therefore most appropriate to de?ne the behavior of a P/T-net component in terms of the production and consumption of tokens. In a single action, any number of tokens can be consumed or produced. This means that an action is uniquely determined by two bags of tokens, one denoting the consumed tokens and one denoting the produced tokens. As a result, actions are no longer atomic, as in the previous chapter, but they are structured. For this reason, actions of P/T-net components are also called multi-actions. Recall that transition names, place names, and hence also token identi?ers, are taken from the universe of identi?ers U introduced in Section 2.3.2. De?nition 3.3.7. (Multi-actions) The set of multi-actions A is de?ned as B (U) × B (U), the set of all pairs of bags over U.
64
Algebraic Veri?cation of Modular Nets
Similar to Section 2.3.2, for any P/T-net component C = (N, I ) with N = (P, T , F, W ), an action function αC : T → A is a function assigning to each transition of C a corresponding multi-action. Since it is always clear from the context to which P/T-net component an action function refers, in the remainder, the subscript of action functions is omitted. De?nition 3.3.8. (Firing rule) The ?ring rule [ ? × A × is the smallest relation satisfying for any (N, I, s) in , with N = (P, T , F, W ) and action function α : T → A, and any t ∈ T , (N, I, s)[t ? (N, I, s) [α(t) (N, I, s ? iit iot).
C
C
C
When analyzing the behavior of a P/T-net component in isolation, it is useful to be able to look inside the component as though it were a glass box. This means that all consumptions and productions of tokens that result from ?ring a transition are visible. When using a component in a compositional design, on the other hand, it is often useful to assume that its internal structure is hidden as in a black box. The environment observes the actions of the P/T-net component projected onto its pins. When formalizing the semantics for P/Tnet components, the action function in the de?nition of the ?ring rule determines which point of view is taken. De?nition 3.3.9. (Action functions) Let (N, I ) with N = (P, T , F, W ) be a P/T-net component.
Glass-box action function: For any transition t ∈ T , α g (t) is equal to (it, ot). Black-box action function: For any transition t ∈ T , αb (t) is de?ned as (oit, oot).
As for labeled P/T nets, the ?ring rule is the basis for the operational semantics for P/T-net components. The semantics de?ned in this chapter do not distinguish between successful termination and deadlock. In this respect, they adhere to the usual semantics given for Petri nets (see also Section 2.3.2). The following de?nition gives the glass-box semantics for P/T-net components. De?nition 3.3.10. (Operational glass-box semantics) The glass-box behavior of marked P/T-net components is formalized by the operational semantics g ( ). It consists of the process space ( , A, [ , ?), where the ?ring rule is instantiated with the glass-box action function α g . The equivalence on processes is strong bisimilarity.
C
S C
s0 rcmd s1 pmat s2 sprdy s3 omat
s0 s1 s2 s3
= [rdy, empty] = [bsy, tcmd, empty] = [bsy, pmt] = [bsy, tprdy, empty]
Figure 3.3.11: The operational semantics of the production-unit component.
3.4 Algebraic Semantics for P/T-Net Components
65
Example 3.3.12. Figure 3.3.11 on the facing page shows the operational glass-box semantics for the P/T-net component of Figure 3.3.1 on Page 62. The ?ring rule is depicted by arrows. Processes are identi?ed with their markings. The transition identi?er t is used as an abbreviation of the corresponding multi-action α g (t). For example, rcmd is an abbreviation of ([cmd, rdy], [tcmd, bsy]). The next de?nition gives the black-box semantics for P/T-net components. As may be expected, it uses rooted branching bisimilarity as the equivalence relation. It is important to note that the silent multi-action in A is the pair (0, 0). De?nition 3.3.13. (Operational black-box semantics) The black-box behavior of P/Tnet components is formalized by the operational semantics b ( ). It consists of the process space ( , A, [ , ?), where the ?ring rule is instantiated with the black-box action function αb . The equivalence on processes is rooted branching bisimilarity.
C
S C
Example 3.3.14. Consider again Figure 3.3.11 on the facing page. Let the identi?er t of a transition be an abbreviation of αb (t), which is the pair (oit, oot). For example, rcmd is an abbreviation of ([cmd], 0). Under this assumption, Figure 3.3.11 shows the semantics for the P/T-net component of Figure 3.3.1 on Page 62 in the black-box semantics b( ).
S C
3.4 Algebraic Semantics for P/T-Net Components
In the previous section, two different operational semantics for P/T-net components have been de?ned, namely the operational glass-box semantics and the operational black-box semantics. This section presents two algebraic semantics for P/T-net components. It is shown that the algebraic semantics are consistent with the two operational semantics of the previous section.
3.4.1 Glass-box semantics
The equational theory PA? . The algebraic glass-box semantics for P/T-net compoδλ nents is de?ned in an extension of the process algebra PA? , Process Algebra with inaction δ and iteration. The theory PA? is de?ned by combining the appropriate ingredients introδ duced in Chapter 2. It is extended with the so-called state operator λ yielding the theory PA? , for Process Algebra with inaction, state operator, and iteration. The state operaδλ tor is an operator which has a memory to explicitly describe the state of a process. For a detailed treatment of the state operator, see (BAETEN AND V ERHOEF , 1995; BAETEN AND W EIJLAND, 1990). The state operator used to de?ne an algebraic semantics for P/Tnet components is called the causal state operator. A variant of the causal state operator ?rst appeared in (BAETEN AND B ERGSTRA, 1993). Table 3.4.1 on the following page presents the theory PA? which is as always parameterized by a set of actions. It is instanδλ tiated with the set of multi-actions A de?ned in the previous section (De?nition 3.3.7 on Page 63). The following auxiliary functions on multi-actions in A are de?ned. For any
66
Algebraic Veri?cation of Modular Nets
action a = (c, p) in A, ca is equal to c and de?nes the consumption of a; pa is p and de?nes the production of a. PA? (A) δλ PA? (A) δ
λ : (P (U) × B (U)) → (P → P) a : A; I : P (U); s : B (U); x, y : P;
I λs (δ) = δ I ca |` I ≤ s ? λs (a) = a I ca |` I ≤ s ? λs (a) = δ I I I λs (a · x) = λs (a) · λs?ca|`I pa|`I (x) I I I λs (x + y) = λs (x) + λs (y)
CSO1 CSO2 CSO3 CSO4 CSO5
Table 3.4.1: The process algebra PA? . δλ
I For I, s, and x as in Table 3.4.1, the term λs (x) can be thought of as the P/T-net component x with internal places I and marking s. The operator is axiomatized by means of ?ve axioms. Axioms CSO2, CSO3, and CSO4 are the most interesting ones. The other two should be clear without further explanation. Axiom CSO2 can be read as follows. It states that an action may occur provided that its consumption from internal places is available in the marking. Axiom CSO3 says that if not enough tokens are available, an action cannot be executed and results in a deadlock. Axiom CSO4 states that the result of executing an action is that the consumption is removed from the marking, whereas the production in internal places is added to the marking. If the marking does not contain enough tokens to execute the action, then the combination of Axioms CSO3 and A7 guarantees that the result is a deadlock. Note the correspondence between the causal state operator and the ?ring rule for P/T-net components.
An operational semantics for PA? . The theory PA? is given an operational semantics δλ δλ in the standard way (see Section 2.4). The processes in the operational √ semantics for the ? ? theory PAδλ are the closed PAδλ terms extended with √ special process . The transition the √ relation ?→ ? (C (PA? )∪{ })×A×(C (PA? )∪{ }) is the smallest relation satisfying δλ δλ the appropriate derivation rules given in Tables 2.4.5 on Page 36, 2.4.24 on Page 43, 2.4.48 on Page 53, and 3.4.2 on the next page, where in all tables p, p , q, and q range over C (PA? ). δλ De?nition 3.4.3. (Operational semantics) The operational semantics (PA? ) is the proδλ √ √ cess space (C (PA? ) ∪ { }, A, ?→ , { }) with strong bisimilarity as the equivalence reδλ lation. Property 3.4.4. (Congruence) Strong bisimilarity, ?, is a congruence for the operators of PA? . δλ
S
3.4 Algebraic Semantics for P/T-Net Components a : A; I :
67
P (U); s : B (U);
p ?→ p
a I ?→ λs a pa|I ( p `
p, p :
C (PA? ); δλ
p ?→
a
√
a
I λs
ca| I ( p) `
)
I λs
ca|I ( p) `
?→
√
Table 3.4.2: The transition relation for the causal state operator. Proof. It follows from the format of the derivation rules in Tables 2.4.5, 2.4.24, 2.4.48, 2 and 3.4.2 (see BAETEN AND V ERHOEF, 1995). Theorem 3.4.5. (Soundness) For any closed terms p, q ∈ C (PA? ), δλ PA? p = q ? (PA? ) |= p = q . δλ δλ
S
Proof. Since bisimilarity is a congruence for the operators of PA? , it is suf?cient to show δλ the validity of each of the axioms of PA? . It is not dif?cult to construct a bisimulation for δλ 2 each case. As explained in Section 2.4.5, there is no completeness result for PA? . δλ Standard concurrency and expansion. The theory PA? can be extended with the axδλ ioms of standard concurrency in exactly the same way as in Section 2.4.5. It is not dif?cult to see that the rooted branching bisimulations given in the proof of Property 2.4.53 on Page 53 are also strong bisimulations. Recursive equations. The theory PA? is extended with the principle RSP? in the same δλ way as in Section 2.4.5. An algebraic semantics for P/T-net components. At this point, all ingredients needed to de?ne an algebraic semantics for P/T-net components are present. Each P/T-net component is translated into a closed PA? term with the same operational behavior as the compoδλ nent, assuming that the glass-box semantics for P/T-net components is chosen. The idea is to start by de?ning the unrestricted behavior of a component. That is, its behavior when every transition is always enabled. Then, the causal state operator instantiated with the marking of the component is used to restrict the behavior to all possible ?ring sequences. The unrestricted behavior of a single transition is the non-terminating iteration of its consumption and production of tokens. The unrestricted behavior of a net component is the parallel execution of all its transitions. De?nition 3.4.6. (Algebraic glass-box semantics) Let C = (N, I, s) be a P/T-net component in , where N = (P, T , F, W ). The algebraic glass-box semantics for C, denoted C g [[C]], is de?ned as follows: C g [[C]] = λsI ( t : t ∈ T : α g (t) ? δ), where α g is the glass-box action function de?ned in De?nition 3.3.9 on Page 64. Note that
C
68
Algebraic Veri?cation of Modular Nets
α g is not an operator of the theory PA? . Hence, α g (t), where t is a transition in T , is not a δλ term in the algebra. However, the value of α g (t) is a multi-action in A and, hence, a term in PA? . Therefore, in the above de?nition, α g (t) should be interpreted as the function δλ value and not as a syntactical term. Example 3.4.7. Let C be the P/T-net component of Figure 3.3.1 on Page 62. As before, the identi?er of a transition t of C is used as an abbreviation of α g (t). Let I be the set of internal places of C, {rdy, bsy, tcmd, tprdy, empty, pmt}. The algebraic glass-box semantics of C is now as follows: I λ[rdy,empty] (rcmd ? δ pmat ? δ sprdy ? δ omat ? δ). Assuming the glass-box semantics for P/T-net components, a component C and its algebraic representation C g [[C]] have the same operational semantics. That is, any action that a component can perform can be simulated by its algebraic semantics and vice versa. Furthermore, since a component cannot terminate successfully, its algebraic semantics cannot terminate successfully either. This means that the algebraic semantics of a net component √ cannot evolve into the special process . In other words, in a process space combining P/T-net components and closed PA? terms, a P/T-net component and its algebraic semanδλ tics are strongly bisimilar. Recall that ≡ denotes syntactical equality of closed terms. Theorem 3.4.8. Assume the semantics for P/T-net components is the operational glassbox semantics g ( ) of De?nition 3.3.10 on Page 64. For any P/T-net components (N, I, s) and (N, I, s ) in , closed term p in C (PA? ), and action a ∈ A, δλ i) (N, I, s) [a (N, I, s ) ? C g [[(N, I, s)]] ?→ C g [[(N, I, s )]],
a
S C C
ii) iii)
a C g [[(N, I, s)]] ?→ p ? (? s : s ∈ B (I ) : p ≡ C g [[(N, I, s )]] ∧ (N, I, s) [a a √ C g [[(N, I, s)]] ?→ .
(N, I, s )),
Proof. Let N be equal to (P, T , F, W ). i) Assume (N, I, s) [a (N, I, s ). It follows from the de?nitions of the semantics g ( ) for P/T-net components (De?nition 3.3.10 on Page 64) and the ?ring rule (De?nition 3.3.8 also on Page 64) that there must be a transition u in T , enabled in marking s, such that a = α g (u) and s = s ? iiu iou. De?nition 3.3.5 (Transition enabling) on Page 63 yields that iiu ≤ s. It follows from De?nition 3.3.9 (Action function α g ) on Page 64 that ca = iu and pa = ou. Hence, ca |` I = iiu and pa |` I = iou. Consequently, s = s ? iiu iou = s ? ca |` I pa |` I . The following steps follow from the derivation rules in Tables 2.4.5 on Page 36, 2.4.24 on Page 43, 2.4.48 on Page 53, and 3.4.2 on the previous page. The fact that a √ a ?→ implies that a a ? δ ?→ a ? δ. Since u ∈ T and a = α g (u), a ( t : t ∈ T : α g (t) ? δ) ?→ ( t : t ∈ T : α g (t) ? δ).
S C
3.4 Algebraic Semantics for P/T-Net Components It follows from the expression derived above for s that a I I λs ( t : t ∈ T : α g (t) ? δ) ?→ λs ( t : t ∈ T : α g (t) ? δ). Hence, De?nition 3.4.6 (Algebraic semantics) on Page 67 yields a C g [[(N, I, s)]] ?→ C g [[(N, I, s )]], which concludes the ?rst part of the proof.
69
ii) Assume C g [[(N, I, s)]] ?→ p. De?nition 3.4.6 (Algebraic semantics) on Page 67 yields a I λs ( t : t ∈ T : α g (t) ? δ) ?→ p. Recall that the transition relation ?→ in the operational semantics (PA? ) (De?niδλ tion 3.4.3 on Page 66) is de?ned as the smallest relation satisfying a set of derivation rules. Therefore, it follows from the derivation rules for the causal state operator in I Table 3.4.2 on Page 67 that process λs ( t : t ∈ T : α g (t) ? δ) can only perform an a action if there is a closed term q ∈ C (PA? ) such that ca |` I ≤ s, δλ I p ≡ λs?ca|`I pa|`I (q), and a ( t : t ∈ T : α g (t) ? δ) ?→ q. In the following, empty merge quanti?cations must be omitted. In addition, for the sake of simplicity, closed terms that are equal up to symmetry and associativity of the merge are considered syntactically equal. The derivation rules for the merge operator in Table 2.4.24 on Page 43 yield that there must be a transition u ∈ T and a closed term r ∈ C (PA? ) such that δλ q ≡ r ( t : t ∈ T ∧ t = u : α g (t) ? δ) and a α g (u) ? δ ?→ r. It follows from the derivation rules for the Kleene star in Table 2.4.48 on Page 53 that a = α g (u) and r ≡ α g (u) ? δ. Hence, it follows from the de?nition of α g (De?nition 3.3.9 on Page 64) that ca = iu and pa = ou. Therefore, s ? ca |` I pa |` I = s ? iiu iou. Summarizing the results so far yields I p ≡ λs?iiu iou ( t : t ∈ T : α g (t) ? δ), which by De?nition 3.4.6 (Algebraic semantics) on Page 67 means that p ≡ C g [[(N, I, s ? iiu iou)]]. Since ca |` I ≤ s, it follows that iiu ≤ s. It follows from the de?nition of transition enabling for P/T-net components (De?nition 3.3.5 on Page 63), the de?nition of the ?ring rule (De?nition 3.3.8 on Page 64), and the fact that α g (u) = a that (N, I, s) [a (N, I, s ? iiu iou), which completes the second part of the proof. a √ iii) Assume C g [[(N, I, s)]] ?→ . It is straightforward to derive from De?nition 3.4