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