Introduction to Process Algebra Book

1	Introduction	1
2	Basic Process Algebra	7
2.1	Basic Process Terms	7
2.2	Transition Rules for BPA	8
2.3	Bisimulation Equivalence	10
2.4	Axioms for BPA	12
3	Algebra of Communicating Processes	17
3.1	Parallelism and Communication	17
3.2	Left Merge and Communication Merge	19
3.3	Axioms for PAP	20
3.4	Deadlock and Encapsulation	25
4	Recursion	31
4.1	Guarded Recursive Specifications	31
4.2	Transition Rules for Guarded Recursion	33
4.3	Recursive Definition and Specification Principles	36
4.4	Completeness for Regular Processes	39
4.5	Approximation Induction Principle	42
5	Abstraction	47
5.1	Rooted Branching Bisimulation Equivalence	47
5.2	Guarded Linear Recursion Revisited	51
5.3	Axioms for the Silent Step	53
5.4	Abstraction Operators	57
5.5	An Example with Queues	60
5.6	Cluster Fair Abstraction Rule	63
6	Protocol Verifications	69
6.1	Alternating Bit Protocol	69
6.2	Bounded Retransmission Protocol	78
6.3	Specification and Verification Techniques	88
6.4	Tools	92
7	Extensions	97
7.1	Renaming	97
7.2	State Operator	99
7.3	Priorities	105
App. A	Equational Logic	109
A.1	Signatures	109
A.2	Axiomatisations	110
A.3	Initial Models	111
A.4	Term Rewriting	113
App. B	Structural Operational Semantics	119
B.1	Transition System Specifications	119
B.2	The Meaning of Negative Premises	121
B.3	Bisimulation as a Congruence	125
B.4	Branching Bisimulation as a Congruence	128
B.5	Conservative Extension	131
B.6	Modal Logics	133
	Solutions to Selected Exercises	137
	References	151
	Index	161