| Introduction | p. 1 |
| The Petri Box Calculus | p. 7 |
| An Informal Introduction to CCS | p. 8 |
| An Informal Introduction to Petri Nets | p. 9 |
| The Structure and Behaviour of PBC Expressions | p. 11 |
| Sequential Composition | p. 14 |
| Synchronisation | p. 15 |
| Synchronisation and Parallel Composition | p. 21 |
| Other PBC Operators | p. 24 |
| Modelling a Concurrent Programming Language | p. 25 |
| Literature and Background | p. 28 |
| Syntax and Operational Semantics | p. 29 |
| Standard PBC Syntax | p. 29 |
| Structured Operational Semantics | p. 33 |
| The Basic Setup | p. 35 |
| Equivalence Notions | p. 37 |
| Elementary Actions | p. 41 |
| Parallel Composition | p. 42 |
| Choice Composition | p. 45 |
| Sequential Composition | p. 46 |
| Synchronisation | p. 47 |
| Standard PBC Synchronisation | p. 47 |
| Auto-synchronisation and Multilink-synchronisation | p. 50 |
| Step-synchronisation | p. 52 |
| Basic Relabelling | p. 53 |
| Restriction | p. 54 |
| Scoping | p. 55 |
| Iteration | p. 58 |
| Recursion | p. 59 |
| Extensions | p. 62 |
| Generalised Iterations | p. 62 |
| Data Variables | p. 64 |
| Generalised Control Flow Operators | p. 66 |
| Generalised Communication Interface Operators | p. 67 |
| Extended PBC Syntax | p. 69 |
| Examples of Transition Systems | p. 69 |
| Literature and Background | p. 71 |
| Petri Net Semantics | p. 73 |
| Compositionality and Nets | p. 73 |
| Labelled Nets and Boxes | p. 75 |
| An Example | p. 75 |
| Actions and Relabellings | p. 76 |
| Labelled Nets | p. 77 |
| Equivalence Notions | p. 82 |
| Boxes | p. 86 |
| Net Refinement | p. 90 |
| Operator Boxes | p. 90 |
| Intuition Behind Net Refinement | p. 92 |
| Place and Transition Names | p. 95 |
| Formal Definition of Net Refinement | p. 97 |
| Remarks on Net Refinement | p. 99 |
| Properties | p. 101 |
| Discussion | p. 103 |
| Petri Net Semantics of PBC | p. 104 |
| Elementary Actions | p. 106 |
| Parallel Composition | p. 106 |
| Choice Composition | p. 107 |
| Sequential Composition | p. 109 |
| Basic Relabelling | p. 110 |
| Synchronisation | p. 110 |
| Restriction | p. 119 |
| Scoping | p. 120 |
| Iteration | p. 120 |
| Data Variables | p. 123 |
| Generalised Control Flow Operators | p. 124 |
| Generalised Communication Interface Operators | p. 126 |
| Generalised Iterations | p. 127 |
| Refined Operators | p. 129 |
| Literature and Background | p. 132 |
| Adding Recursion | p. 133 |
| Inclusion Order on Labelled Nets | p. 133 |
| Solving Recursive Equations | p. 135 |
| Using Fixpoints to Solve Recursive Equations | p. 137 |
| Places and Transitions in Net Solutions | p. 140 |
| An Example of the Limit Construction | p. 144 |
| Deriving Seed Boxes | p. 145 |
| A Closed Form of the Maximal Solution | p. 151 |
| Minimal Solutions | p. 153 |
| Finitary Equations and Finite Operator Boxes | p. 157 |
| Finitary Equation | p. 157 |
| Finite Operator Box | p. 159 |
| Further Examples | p. 161 |
| Unbounded Parallel Composition | p. 161 |
| Rear-unguardedness | p. 162 |
| Concurrency Within Unbounded Choice | p. 164 |
| Extreme Unguardedness | p. 166 |
| (Non)use of Empty Nets in the Limit Construction | p. 167 |
| Solving Systems of Recursive Equations | p. 167 |
| Approximations, Existence, and Uniqueness | p. 168 |
| A Closed Form of the Maximal Solution | p. 169 |
| Guarded Systems | p. 171 |
| Literature and Background | p. 172 |
| S-invariants | p. 173 |
| S-invariants, S-components, and S-aggregates | p. 174 |
| S-invariants | p. 176 |
| S-components | p. 181 |
| S-aggregates | p. 182 |
| The Synthesis Problem for Net Refinement | p. 183 |
| Composing S-invariants | p. 185 |
| Multiplicative Distribution Functions | p. 190 |
| Ex-binary S-invariants | p. 193 |
| Rational Groupings | p. 195 |
| The Synthesis Problem for Recursive Systems | p. 200 |
| Name Trees of Nets in the Maximal Solution | p. 201 |
| Composing S-invariants for Recursive Boxes | p. 202 |
| Coverability Results | p. 209 |
| Finite Precedence Properties | p. 216 |
| Process Semantics | p. 218 |
| Finite Precedence of Events | p. 222 |
| Finiteness of Complete Processes | p. 225 |
| Literature and Background | p. 226 |
| The Box Algebra | p. 227 |
| SOS-operator Boxes | p. 227 |
| A Running Example | p. 232 |
| Properties of Factorisations | p. 232 |
| The Domain of Application of an SOS-operator Box | p. 234 |
| Static Properties of Refinements | p. 235 |
| Markings of Nets | p. 239 |
| Structured Operational Semantics of Composite Boxes | p. 241 |
| Soundness | p. 243 |
| Similarity Relation on Tuples of Boxes | p. 245 |
| Completeness | p. 248 |
| Solutions of Recursive Systems | p. 253 |
| Behavioural Restrictions | p. 255 |
| A Process Algebra and its Semantics | p. 259 |
| A Running Example: the DIY Algebra | p. 262 |
| Infinite Operators | p. 264 |
| Denotational Semantics | p. 267 |
| Structural Similarity Relation on Expressions | p. 270 |
| Transition-based Operational Semantics | p. 279 |
| Consistency of the Two Semantics | p. 286 |
| Label-based Operational Semantics | p. 287 |
| Partial Order Semantics of Box Expressions | p. 290 |
| Literature and Background | p. 294 |
| PBC and Other Process Algebras | p. 295 |
| (Generalised) PBC is a Box Algebra | p. 295 |
| PBC Without Loops | p. 295 |
| Safe Translation of the Ternary PBC Iteration | p. 299 |
| PBC with Generalised Loops | p. 306 |
| Other Process Algebras | p. 308 |
| CCS | p. 310 |
| TCSP | p. 311 |
| COSY | p. 311 |
| Literature and Background | p. 312 |
| A Concurrent Programming Language | p. 313 |
| Syntax of Razor | p. 313 |
| Programs and Blocks | p. 315 |
| Declarations | p. 315 |
| Commands and Actions | p. 316 |
| Guarded Commands | p. 316 |
| Expressions and Operators | p. 317 |
| Syntactic Variations | p. 317 |
| Semantics of Razor | p. 318 |
| Programs, Blocks, and Declarations | p. 319 |
| Basic Channel Processes | p. 321 |
| Command Connectives | p. 324 |
| Actions and Guarded Commands | p. 325 |
| Three Razor Programs | p. 329 |
| Adding Recursive Procedures | p. 332 |
| Some Consequences of the Theory | p. 336 |
| Proofs of Distributed Algorithms | p. 340 |
| A Final Set of Petri-Net-Related Definitions | p. 340 |
| Peterson's Mutual Exclusion Algorithm | p. 342 |
| Dekker's and Morris's Mutual Exclusion Algorithms | p. 346 |
| Literature and Background | p. 347 |
| Conclusion | p. 349 |
| Appendix: Solutions of Selected Exercises | p. 351 |
| References | p. 362 |
| Index | p. 369 |
| Table of Contents provided by Publisher. All Rights Reserved. |