| Preface |
|
v | |
|
|
|
1 | (30) |
|
|
|
1 | (17) |
|
|
|
2 | (7) |
|
The Theories BPA and BPAδ |
|
|
9 | (4) |
|
|
|
13 | (5) |
|
Algebra of Communicating Processes |
|
|
18 | (13) |
|
|
|
19 | (3) |
|
|
|
22 | (5) |
|
|
|
27 | (1) |
|
Some Calculations: Message-Passing System |
|
|
28 | (2) |
|
|
|
30 | (1) |
|
|
|
31 | (40) |
|
|
|
32 | (21) |
|
|
|
32 | (7) |
|
|
|
39 | (4) |
|
|
|
43 | (3) |
|
|
|
46 | (3) |
|
|
|
49 | (1) |
|
|
|
49 | (4) |
|
|
|
53 | (1) |
|
Algebra of Communicating Processes |
|
|
53 | (15) |
|
|
|
54 | (4) |
|
|
|
58 | (5) |
|
|
|
63 | (1) |
|
Some Calculations: PAR Protocol |
|
|
64 | (3) |
|
|
|
67 | (1) |
|
|
|
68 | (3) |
|
|
|
68 | (1) |
|
Relative Timing versus Absolute Timing |
|
|
69 | (2) |
|
|
|
71 | (52) |
|
|
|
72 | (15) |
|
|
|
72 | (5) |
|
|
|
77 | (6) |
|
|
|
83 | (4) |
|
Algebra of Communicating Processes |
|
|
87 | (18) |
|
|
|
87 | (4) |
|
|
|
91 | (5) |
|
|
|
96 | (1) |
|
Some Calculations: Fischer's Protocol |
|
|
97 | (6) |
|
|
|
103 | (2) |
|
Discrete Initial Abstraction |
|
|
105 | (7) |
|
|
|
105 | (3) |
|
|
|
108 | (3) |
|
|
|
111 | (1) |
|
Time-Dependent Conditions |
|
|
112 | (5) |
|
|
|
112 | (2) |
|
|
|
114 | (3) |
|
|
|
117 | (6) |
|
|
|
117 | (1) |
|
Relating ACPdat to ACPdrt and ACPdat |
|
|
118 | (2) |
|
|
|
120 | (1) |
|
Discrete Time versus Continuous Time |
|
|
121 | (2) |
|
Continuous Relative Timing |
|
|
123 | (36) |
|
|
|
124 | (17) |
|
|
|
124 | (6) |
|
|
|
130 | (5) |
|
|
|
135 | (2) |
|
|
|
137 | (4) |
|
Algebra of Communicating Processes |
|
|
141 | (14) |
|
|
|
141 | (3) |
|
|
|
144 | (5) |
|
|
|
149 | (1) |
|
|
|
149 | (4) |
|
Example: Bottle Filling System |
|
|
153 | (2) |
|
|
|
155 | (4) |
|
|
|
155 | (1) |
|
Relating ACPsrt I to ACPdrt |
|
|
155 | (1) |
|
Generalized Relative Delay |
|
|
156 | (3) |
|
Continuous Absolute Timing |
|
|
159 | (46) |
|
|
|
159 | (17) |
|
|
|
160 | (5) |
|
|
|
165 | (5) |
|
|
|
170 | (3) |
|
|
|
173 | (3) |
|
Algebra of Communicating Processes |
|
|
176 | (16) |
|
|
|
176 | (3) |
|
|
|
179 | (5) |
|
|
|
184 | (1) |
|
|
|
184 | (3) |
|
Example: Railroad Crossing System |
|
|
187 | (3) |
|
|
|
190 | (2) |
|
Standard Initial Abstraction |
|
|
192 | (3) |
|
|
|
192 | (1) |
|
|
|
193 | (2) |
|
Time-Dependent Conditions |
|
|
195 | (5) |
|
|
|
196 | (1) |
|
|
|
197 | (3) |
|
|
|
200 | (5) |
|
|
|
201 | (1) |
|
Relating ACPsatI to ACPsrtI and ACPsatI |
|
|
201 | (1) |
|
Relating ACPsatI to CPdat |
|
|
202 | (3) |
|
|
|
205 | (26) |
|
|
|
205 | (3) |
|
|
|
208 | (9) |
|
|
|
209 | (3) |
|
Algebra of Communicating Processes |
|
|
212 | (2) |
|
|
|
214 | (3) |
|
|
|
217 | (1) |
|
|
|
217 | (4) |
|
|
|
218 | (1) |
|
Algebra of Communicating Processes |
|
|
219 | (1) |
|
|
|
220 | (1) |
|
|
|
221 | (1) |
|
Continuous Relative Timing |
|
|
221 | (5) |
|
|
|
221 | (3) |
|
Algebra of Communicating Processes |
|
|
224 | (1) |
|
|
|
225 | (1) |
|
Continuous Absolute Timing |
|
|
226 | (5) |
|
|
|
226 | (1) |
|
Algebra of Communicating Processes |
|
|
227 | (1) |
|
|
|
228 | (2) |
|
|
|
230 | (1) |
|
|
|
231 | (10) |
|
|
|
232 | (3) |
|
|
|
235 | (2) |
|
|
|
237 | (4) |
| A. Soundness and Completeness of ACPdrt |
|
241 | (10) |
|
|
|
241 | (2) |
|
|
|
243 | (5) |
|
|
|
248 | (3) |
| B. Background Material |
|
251 | (24) |
|
Basic Equational Logic and SOS Theory |
|
|
251 | (10) |
|
|
|
251 | (5) |
|
|
|
256 | (5) |
|
|
|
261 | (9) |
|
TSSs with Negative Premises |
|
|
262 | (1) |
|
Variable Binding Operators |
|
|
263 | (3) |
|
Conservativity and Completeness |
|
|
266 | (1) |
|
|
|
267 | (1) |
|
Given Sorts and Parametrization |
|
|
268 | (2) |
|
Non-negative Real Numbers |
|
|
270 | (5) |
| References |
|
275 | (4) |
| Glossary |
|
279 | (6) |
| Index |
|
285 | |