|
|
|
Background on Concurrency Theory |
|
|
3 | (16) |
|
Concurrency Is Everywhere |
|
|
3 | (1) |
|
Characteristics of Concurrent Systems |
|
|
4 | (2) |
|
Classes of Concurrent Systems |
|
|
6 | (3) |
|
|
6 | (1) |
|
|
7 | (1) |
|
Probabilistic Choice Axis |
|
|
8 | (1) |
|
|
9 | (1) |
|
|
9 | (4) |
|
|
13 | (6) |
|
Part II Concurrency Theory -- Untimed Models |
|
|
|
|
19 | (36) |
|
|
19 | (1) |
|
|
20 | (2) |
|
|
20 | (2) |
|
|
22 | (1) |
|
|
22 | (30) |
|
|
26 | (2) |
|
|
28 | (1) |
|
|
29 | (1) |
|
|
30 | (4) |
|
|
34 | (7) |
|
|
41 | (6) |
|
Sequential Composition and Exit |
|
|
47 | (3) |
|
|
50 | (2) |
|
|
52 | (3) |
|
Basic Interleaved Semantic Models |
|
|
55 | (50) |
|
A General Perspective on Semantics |
|
|
55 | (8) |
|
|
55 | (2) |
|
|
57 | (4) |
|
|
61 | (2) |
|
What Makes a Good Semantics? |
|
|
63 | (1) |
|
|
63 | (13) |
|
|
63 | (3) |
|
|
66 | (7) |
|
|
73 | (2) |
|
|
75 | (1) |
|
Labelled Transition Systems |
|
|
76 | (25) |
|
|
76 | (2) |
|
|
78 | (7) |
|
|
85 | (16) |
|
|
101 | (4) |
|
|
102 | (1) |
|
Bisimulation Checking in CADP |
|
|
103 | (2) |
|
True Concurrency Models: Event Structures |
|
|
105 | (36) |
|
|
105 | (2) |
|
The Basic Approach -- Event Structures |
|
|
107 | (5) |
|
Event Structures and pbLOTOS |
|
|
112 | (3) |
|
An Event Structures Semantics for pbLOTOS |
|
|
115 | (8) |
|
Relating Event Structures to Labelled Transition Systems |
|
|
123 | (3) |
|
|
126 | (8) |
|
Alternative Event Structure Models |
|
|
134 | (4) |
|
|
138 | (3) |
|
Testing Theory and the Linear Time -- Branching Time Spectrum |
|
|
141 | (44) |
|
|
141 | (19) |
|
|
141 | (2) |
|
|
143 | (2) |
|
Deriving Trace-refusal Pairs |
|
|
145 | (1) |
|
|
146 | (6) |
|
Development Relations: Equivalences |
|
|
152 | (2) |
|
Nonequivalence Development Relations |
|
|
154 | (4) |
|
Explorations of Congruence |
|
|
158 | (1) |
|
|
159 | (1) |
|
Testing Justification for Trace-refusals Semantics |
|
|
160 | (1) |
|
Testing Theory in General and the Linear Time -- Branching Time Spectrum |
|
|
161 | (5) |
|
|
162 | (1) |
|
|
163 | (3) |
|
Applications of Trace-refusals Relations in Distributed Systems |
|
|
166 | (19) |
|
Relating OO Concepts to LOTOS |
|
|
166 | (1) |
|
|
167 | (10) |
|
Viewpoints and Consistency |
|
|
177 | (8) |
|
Part III Concurrency Theory -- Further Untimed Notations |
|
|
|
|
185 | (30) |
|
|
185 | (7) |
|
|
185 | (3) |
|
|
188 | (1) |
|
|
189 | (1) |
|
Verbose Specification Syntax |
|
|
190 | (1) |
|
|
190 | (1) |
|
|
191 | (1) |
|
|
192 | (15) |
|
|
193 | (1) |
|
|
193 | (1) |
|
Process Definition and Invocation |
|
|
194 | (1) |
|
|
194 | (8) |
|
|
202 | (1) |
|
|
202 | (1) |
|
|
203 | (1) |
|
|
204 | (2) |
|
|
206 | (1) |
|
|
206 | (1) |
|
|
207 | (6) |
|
|
207 | (3) |
|
|
210 | (3) |
|
|
213 | (2) |
|
Comparison of LOTOS with CCS and CSP |
|
|
215 | (18) |
|
|
217 | (5) |
|
Parallel Composition and Complementation of Actions |
|
|
217 | (3) |
|
|
220 | (1) |
|
|
221 | (1) |
|
|
221 | (1) |
|
|
222 | (11) |
|
|
222 | (2) |
|
|
224 | (1) |
|
|
225 | (2) |
|
|
227 | (1) |
|
|
227 | (1) |
|
Comparison of LOTOS Trace-refusals with CSP Failures-divergences |
|
|
228 | (5) |
|
|
233 | (28) |
|
|
233 | (1) |
|
Networks of Communicating Automata |
|
|
234 | (16) |
|
|
234 | (2) |
|
|
236 | (3) |
|
|
239 | (1) |
|
Semantics and Development Relations |
|
|
240 | (1) |
|
Verification of Networks of Communicating Automata |
|
|
241 | (5) |
|
Relationship to Process Calculi |
|
|
246 | (4) |
|
Infinite State Communicating Automata |
|
|
250 | (11) |
|
Networks of Infinite State Communicating Automata |
|
|
251 | (3) |
|
Semantics of ISCAs as Labelled Transition Systems |
|
|
254 | (7) |
|
Part IV Concurrency Theory -- Timed Models |
|
|
|
Timed Process Calculi, a LOTOS Perspective |
|
|
261 | (26) |
|
|
261 | (1) |
|
Timed LOTOS -- The Issues |
|
|
262 | (16) |
|
|
262 | (5) |
|
|
267 | (3) |
|
|
270 | (1) |
|
|
271 | (1) |
|
|
272 | (1) |
|
|
273 | (1) |
|
|
273 | (1) |
|
Timing of Nonadjacent Actions |
|
|
274 | (1) |
|
Timed Interaction Policies |
|
|
275 | (1) |
|
Forms of Internal Urgency |
|
|
276 | (2) |
|
|
278 | (1) |
|
|
278 | (5) |
|
|
278 | (3) |
|
|
281 | (2) |
|
Timing Anomalies in tLOTOS |
|
|
283 | (2) |
|
E-LOTOS, the Timing Extensions |
|
|
285 | (2) |
|
Semantic Models for tLOTOS |
|
|
287 | (34) |
|
|
287 | (17) |
|
|
287 | (2) |
|
|
289 | (10) |
|
Branching Time Development Relations |
|
|
299 | (5) |
|
True Concurrency Semantics |
|
|
304 | (17) |
|
|
304 | (1) |
|
Timed Bundle Event Structures |
|
|
305 | (3) |
|
Causal Semantics for tLOTOS |
|
|
308 | (10) |
|
|
318 | (2) |
|
|
320 | (1) |
|
Timed Communicating Automata |
|
|
321 | (26) |
|
|
321 | (2) |
|
Timed Automata -- Formal Definitions |
|
|
323 | (9) |
|
|
324 | (1) |
|
|
325 | (7) |
|
|
332 | (15) |
|
|
333 | (8) |
|
Example: Reachability Analysis on the Multimedia Stream |
|
|
341 | (1) |
|
Issues in Real-time Model-checking |
|
|
342 | (5) |
|
Timelocks in Timed Automata |
|
|
347 | (30) |
|
|
347 | (2) |
|
A Classification of Deadlocks in Timed Automata |
|
|
349 | (3) |
|
Discussion: Justifying the Classification of Deadlocks |
|
|
350 | (1) |
|
Discussion: Timelocks in Process Calculi |
|
|
351 | (1) |
|
|
352 | (7) |
|
Timed Automata with Deadlines |
|
|
353 | (5) |
|
Example: A TAD Specification for the Multimedia Stream |
|
|
358 | (1) |
|
|
359 | (15) |
|
Example: Zeno-timelocks in the Multimedia Stream |
|
|
359 | (2) |
|
Nonzenoness: Syntactic Conditions |
|
|
361 | (7) |
|
Nonzenoness: A Sufficient-and-Necessary Condition |
|
|
368 | (6) |
|
Timelock Detection in Real-time Model-checkers |
|
|
374 | (3) |
|
|
374 | (2) |
|
|
376 | (1) |
|
|
377 | (20) |
|
Infinite vs. Finite States |
|
|
377 | (3) |
|
|
380 | (4) |
|
Fair Transition Systems and Invariance Proofs |
|
|
381 | (2) |
|
The Weak Monadic Second-order Theory of 1 Successor (WS1S) and MONA |
|
|
383 | (1) |
|
Discrete Timed Automata -- Formal definitions |
|
|
384 | (5) |
|
|
384 | (2) |
|
Example: A DTA Specification for the Multimedia Stream |
|
|
386 | (1) |
|
|
387 | (2) |
|
Verifying Safety Properties over DTAs |
|
|
389 | (5) |
|
Discussion: Comparing DTAs and TIOAs with Urgency |
|
|
394 | (3) |
|
|
397 | (12) |
|
|
409 | (20) |
|
Enabling as a Derived Operator |
|
|
409 | (1) |
|
Strong Bisimulation Is a Congruence |
|
|
409 | (5) |
|
Weak Bisimulation Congruence |
|
|
414 | (5) |
|
Timed Enabling as a Derived Operator |
|
|
419 | (1) |
|
Hiding is Not Substitutive for Timed Bisimulations |
|
|
420 | (1) |
|
Substitutivity of Timed Strong Bisimulation |
|
|
420 | (2) |
|
Substitutivity of Timed Rooted Weak Bisimulation |
|
|
422 | (7) |
Index |
|
429 | |