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 Trace Semantics from Labelled Transition Systems	102
	3.3.3 Development Relations	103
	3.3.3.1 Basic Equivalence Relations	103
	3.3.3.2 Refinement Relations and Induced Equivalences	114
	3.4 Verification Tools	119
	3.4.1 Overview of CADP	120
	3.4.2 Bisimulation Checking in CADP	121
	4 True Concurrency Models: Event Structures	123
	4.1 Introduction	123
	4.2 The Basic Approach – Event Structures	125
	4.3 Event Structures and pbLOTOS	130
	4.4 An Event Structures Semantics for pbLOTOS	133
	4.5 Relating Event Structures to Labelled Transition Systems	141
	4.6 Development Relations	144
	4.7 Alternative Event Structure Models	152
	4.8 Summary and Discussion	156
	5 Testing Theory and the Linear Time – Branching Time Spectrum	158
	5.1 Trace-refusals Semantics	158
	5.1.1 Introduction	158
	5.1.2 The Basic Approach	160
	5.1.2.1 Example 1	161
	5.1.2.2 Example 2	161
	5.1.2.3 Example 3	161
	5.1.2.4 Example 4	162
	5.1.3 Deriving Trace-refusal Pairs	162
	5.1.3.1 Deriving Trace-refusals from Labelled Transition Systems	162
	5.1.3.2 Direct Denotational Semantics	163
	5.1.4 Internal Behaviour	163
	5.1.5 Development Relations: Equivalences	169
	5.1.6 Nonequivalence Development Relations	171
	5.1.6.1 Conformance	171
	5.1.6.2 Reduction	173
	5.1.6.3 Extension	174
	5.1.7 Explorations of Congruence	175
	5.1.8 Summary and Discussion	176
	5.2 Testing Justification for Trace-refusals Semantics	177
	5.3 Testing Theory in General and the Linear Time – Branching Time Spectrum	178
	5.3.1 Sequence-based Testing	179
	5.3.2 Tree-based Testing	180
	5.4 Applications of Trace-refusals Relations in Distributed Systems	183
	5.4.1 Relating OO Concepts to LOTOS	183
	5.4.2 Behavioural Subtyping	184
	5.4.2.1 Relating LOTOS Relations and Subtyping	186
	5.4.2.2 Functionality Extension and Undefined	188
	5.4.2.3 Adding Unde.nedness to LOTOS Specifications	192
	5.4.3 Viewpoints and Consistency	194
	5.4.3.1 Consistency Definition	195
	5.4.3.2 Consistency in LOTOS	197
	5.4.3.3 Discussion	197
	Part III Concurrency Theory – Further Untimed Notations	198
	6 Beyond pbLOTOS	200
	6.1 Basic LOTOS	200
	6.1.1 Disabling	200
	6.1.2 Generalised Choice	203
	6.1.3 Generalised Parallelism	204
	6.1.4 Verbose Specification Syntax	205
	6.1.5 Verbose Process Syntax	205
	6.1.6 Syntax of bLOTOS	206
	6.2 Full LOTOS	207
	6.2.1 Guarded Choice	208
	6.2.2 Specification Notation	208
	6.2.3 Process Definition and Invocation	209
	6.2.4 Value Passing Actions	209
	6.2.4.1 Value Passing and Synchronisation	212
	6.2.4.2 Value Passing and Internal Behaviour	213
	6.2.4.3 Illustration of Value Passing	215
	6.2.5 Local Definitions	217
	6.2.6 Selection Predicates	217
	6.2.7 Generalised Choice	218
	6.2.8 Parameterised Enabling	219
	6.2.9 Syntax of fLOTOS	221
	6.2.10 Comments	221
	6.3 Examples	222
	6.3.1 Communication Protocol	222
	6.3.2 Dining Philosophers	225
	6.4 Extended LOTOS	228
	7 Comparison of LOTOS with CCS and CSP	230
	7.1 CCS and LOTOS	232
	7.1.1 Parallel Composition and Complementation of Actions	232
	7.1.2 Restriction and Hiding	235
	7.1.3 Internal Behaviour	236
	7.1.4 Minor Di.erences	236
	7.2 CSP and LOTOS	237
	7.2.1 Alphabets	237
	7.2.2 Internal Actions	239
	7.2.3 Choice	240
	7.2.3.1 Deterministic Choice (also Called Guarded Alternative)	240
	7.2.3.2 External Choice	241
	7.2.3.3 Nondeterministic Choice	241
	7.2.4 Parallelism	242
	7.2.5 Hiding	242
	7.2.6 Comparison of LOTOS Trace-refusals with CSP Failures-divergences	243
	7.2.6.1 Divergence	243
	7.2.6.2 Development Relations and Congruence	245
	8 Communicating Automata	248
	8.1 Introduction	248
	8.2 Networks of Communicating Automata	249
	8.2.1 Component Automata	249
	8.2.2 Parallel Composition	251
	8.2.2.1 Basic Notation	251
	8.2.2.2 Formal Definition	252
	8.2.3 Example Specifications	254
	8.2.4 Semantics and Development Relations	255
	8.2.5 Verification of Networks of Communicating Automata	256
	8.2.5.1 Computation Tree Logic (CTL)	256
	8.2.5.2 Model-checking CTL	261
	8.2.6 Relationship to Process Calculi	261
	8.2.6.1 Encoding Networks of CAs into Process Calculi	261
	8.2.6.2 Comparing Communicating Automata Networks and Process Calculi	263
	8.3 Infinite State Communicating Automata	265
	8.3.1 Networks of Infinite State Communicating Automata	266
	8.3.1.1 Component Automata	266
	8.3.1.2 Parallel Composition	267
	8.3.2 Semantics of ISCAs as Labelled Transition Systems	269
	Part IV Concurrency Theory – Timed Models	271
	9 Timed Process Calculi, a LOTOS Perspective	273
	9.1 Introduction	273
	9.2 Timed LOTOS – The Issues	274
	9.2.1 Timed Action Enabling	274
	9.2.2 Urgency	279
	9.2.3 Persistency	282
	9.2.4 Nondeterminism	283
	9.2.5 Synchronisation	284
	9.2.6 Timing Domains	285
	9.2.7 Time Measurement	285
	9.2.8 Timing of Nonadjacent Actions	286
	9.2.9 Timed Interaction Policies	287
	9.2.10 Forms of Internal Urgency	288
	9.2.11 Discussion	290
	9.3 Timed LOTOS Notation	290
	9.3.1 The Language	290
	9.3.2 Example Specifications	293
	9.4 Timing Anomalies in tLOTOS	295
	9.5 E-LOTOS, the Timing Extensions	297
	10 Semantic Models for tLOTOS	299
	10.1 Branching Time Semantics	299
	10.1.1 Timed Transition Systems	299
	10.1.2 Operational Semantics	301
	10.1.3 Branching Time Development Relations	311
	10.2 True Concurrency Semantics	316
	10.2.1 Introduction	316
	10.2.2 Timed Bundle Event Structures	317
	10.2.3 Causal Semantics for tLOTOS	320
	10.2.3.1 Inaction, Successful Termination and Action Prefix	321
	10.2.3.2 Delay, Hiding and Relabelling	322
	10.2.3.3 Choice	324
	10.2.3.4 Enabling	324
	10.2.3.5 Parallel Composition	325
	10.2.3.6 Process Instantiation	328
	10.2.4 Anomalous Behaviour	330
	10.2.5 Discussion	332
	11 Timed Communicating Automata	333
	11.1 Introduction	333
	11.2 Timed Automata – Formal Definitions	335
	11.2.1 Syntax	336
	11.2.1.1 Example: A TA Specification for the Multimedia Stream	336
	11.2.2 Semantics	337
	11.2.2.1 Runs	340
	11.2.2.2 Parallel Composition	340
	11.2.2.3 A TTS Semantics for Timed Automata	342
	11.2.2.4 Discussion: Urgency in Timed Automata and tLOTOS	343
	11.3 Real-time Model-checking	344
	11.3.1 Forward Reachability	345
	11.3.1.1 Symbolic States and Operations on Zones	346
	11.3.1.2 The Forward Reachability Graph	349
	11.3.1.3 A Forward Reachability Algorithm	351
	11.3.1.4 Difference Bound Matrices (DBMs): A Data Structure to Represent Zones	352
	11.3.2 Example: Reachability Analysis on the Multimedia Stream	353
	11.3.3 Issues in Real-time Model-checking	354
	12 Timelocks in Timed Automata	358
	12.1 Introduction	358
	12.2 A Classification of Deadlocks in Timed Automata	360
	12.2.1 Discussion: Justifying the Classi.cation of Deadlocks	361
	12.2.2 Discussion: Timelocks in Process Calculi	362
	12.3 Time-actionlocks	363
	12.3.1 Timed Automata with Deadlines	364
	12.3.1.1 Formal Definitions: Timed Automata with Deadlines	365
	12.3.2 Example: A TAD Specification for the Multimedia Stream	369
	12.4 Zeno-timelocks	370
	12.4.1 Example: Zeno-timelocks in the Multimedia Stream	370
	12.4.2 Nonzenoness: Syntactic Conditions	372
	12.4.3 Nonzenoness: A Sufficient-and-Necessary Condition	379
	12.5 Timelock Detection in Real-time Model-checkers	385
	12.5.1 Uppaal	385
	12.5.2 Kronos	387
	13 Discrete Timed Automata	388
	13.1 Infinite vs. Finite States	388
	13.2 Preliminaries	391
	13.2.1 Fair Transition Systems and Invariance Proofs	392
	13.2.2 The Weak Monadic Second-order Theory of 1 Successor ( WS1S) and MONA	394
	13.3 Discrete Timed Automata – Formal definitions	395
	13.3.1 Syntax	395
	13.3.2 Example: A DTA Specification for the Multimedia Stream	397
	13.3.3 Semantics	398
	13.4 Verifying Safety Properties over DTAs	400
	13.5 Discussion: Comparing DTAs and TIOAs with Urgency	405
	References	407
	Appendix	418
	14.1 Enabling as a Derived Operator	418
	14.2 Strong Bisimulation Is a Congruence	418
	14.3 Weak Bisimulation Congruence	423
	14.4 Timed Enabling as a Derived Operator	428
	14.5 Hiding is Not Substitutive for Timed Bisimulations	429
	14.6 Substitutivity of Timed Strong Bisimulation	429
	14.7 Substitutivity of Timed Rooted Weak Bisimulation	431
	Index	438