Introduction to Process Algebra

1. Introduction......Page 10
2.1 Basic Process Terms......Page 16
2.2 Transition Rules for BPA......Page 17
2.3 Bisimulation Equivalence......Page 19
2.4 Axioms for BPA......Page 21
3.1 Parallelism and Communication......Page 28
3.2 Left Merge and Communication Merge......Page 30
3.3 Axioms for PAP......Page 31
3.4 Deadlock and Encapsulation......Page 36
4.1 Guarded Recursive Specifications......Page 42
4.2 Transition Rules for Guarded Recursion......Page 44
4.3 Recursive Definition and Specification Principles......Page 47
4.4 Completeness for Regular Processes......Page 50
4.5 Approximation Induction Principle......Page 53
5.1 Rooted Branching Bisimulation Equivalence......Page 58
5.2 Guarded Linear Recursion Revisited......Page 62
5.3 Axioms for the Silent Step......Page 64
5.4 Abstraction Operators......Page 68
5.5 An Example with Buffers......Page 71
5.6 Cluster Fair Abstraction Rule......Page 74
6.1 Alternating Bit Protocol......Page 80
6.2 Bounded Retransmission Protocol......Page 89
6.3 Verification Techniques......Page 99
6.4 Tools......Page 100
7.1 Renaming......Page 106
7.2 State Operator......Page 108
7.3 Priorities......Page 114
7.4 Further Extensions......Page 118
A.1 Signatures......Page 122
A.2 Axiomatisations......Page 123
A.3 Initial Models......Page 124
A.4 Term Rewriting......Page 126
B.1 Transition System Specifications......Page 132
B.2 The Meaning of Negative Premises......Page 134
B.3 Bisimulation as a Congruence......Page 138
B.4 Branching Bisimulation as a Congruence......Page 141
B.5 Conservative Extension......Page 145
B.6 Modal Logics......Page 147
Solutions to Selected Exercises......Page 150
References......Page 164
Index......Page 176