| Preface | 6 |
---|
| Contents | 17 |
---|
| Part I Introduction | 23 |
---|
| 1 Background on Concurrency Theory | 24 |
| 1.1 Concurrency Is Everywhere | 24 |
| 1.2 Characteristics of Concurrent Systems | 25 |
| 1.3 Classes of Concurrent Systems | 27 |
| 1.3.1 Basic Event Ordering | 27 |
| 1.3.2 Timing Axis | 28 |
| 1.3.3 Probabilistic Choice Axis | 29 |
| 1.3.4 Mobility Axis | 30 |
| 1.4 Mathematical Theories | 30 |
| 1.5 Overview of Book | 34 |
| Part II Concurrency Theory – Untimed Models | 35 |
---|
| 2 Process Calculi: LOTOS | 37 |
| 2.1 Introduction | 37 |
| 2.2 Example Specifications | 38 |
| 2.2.1 A Communication Protocol | 38 |
| 2.2.2 The Dining Philosophers | 40 |
| 2.3 Primitive Basic LOTOS | 40 |
| 2.3.1 Abstract Actions | 44 |
| 2.3.2 Action Prefix | 46 |
| 2.3.3 Choice | 47 |
| 2.3.4 Nondeterminism | 48 |
| 2.3.5 Process Definition | 52 |
| 2.3.6 Concurrency | 59 |
| 2.3.6.1 Independent Parallelism | 59 |
| 2.3.6.2 General Form | 61 |
| 2.3.6.3 Example | 64 |
| 2.3.6.4 Why Synchronous Communication? | 64 |
| 2.3.7 Sequential Composition and Exit | 65 |
| 2.3.8 Syntax of pbLOTOS | 68 |
| 2.4 Example | 70 |
| 3 Basic Interleaved Semantic Models | 73 |
| 3.1 A General Perspective on Semantics | 73 |
| 3.1.1 Why Semantics? | 73 |
| 3.1.2 Formal Definition | 75 |
| 3.1.3 Modelling Recursion | 79 |
| 3.1.4 What Makes a Good Semantics? | 81 |
| 3.2 Trace Semantics | 81 |
| 3.2.1 The Basic Approach | 81 |
| 3.2.2 Formal Semantics | 84 |
| 3.2.2.1 Preliminaries: Traces | 84 |
| 3.2.2.2 A Denotational Trace Semantics for pbLOTOS | 85 |
| 3.2.3 Development Relations | 91 |
| 3.2.3.1 Trace Preorder | 91 |
| 3.2.3.2 Trace Equivalence | 93 |
| 3.2.4 Discussion | 93 |
| 3.3 Labelled Transition Systems | 94 |
| 3.3.1 The Basic Approach | 94 |
| 3.3.2 Formal Semantics | 96 |
| 3.3.2.1 Preliminaries: Labelled Transition Systems | 96 |
| 3.3.2.2 An Operational Semantics for LOTOS | 97 |
| 3.3.2.3 Deriving Trac
|