## Introduction to Process AlgebraAutomated and semi-automated manipulation of so-called labelled transition systems has become an important means in discovering flaws in software and hardware systems. Process algebra has been developed to express such labelled transition systems algebraically, which enhances the ways of manipulation by means of equational logic and term rewriting. The theory of process algebra has developed rapidly over the last twenty years, and verification tools have been developed on the basis of process algebra, often in cooperation with techniques related to model checking. This textbook gives a thorough introduction into the basics of process algebra and its applications. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 Introduction | 1 |

2 Basic Process Algebra | 7 |

22 Transition Rules for BPA | 8 |

23 Bisimulation Equivalence | 10 |

24 Axioms for BPA | 12 |

3 Algebra of Communicating Processes | 17 |

32 Left Merge and Communication Merge | 19 |

33 Axioms for PAP | 20 |

62 Bounded Retransmission Protocol | 78 |

63 Specification and Verification Techniques | 88 |

64 Tools | 92 |

7 Extensions | 97 |

72 State Operator | 99 |

73 Priorities | 105 |

A Equational Logic | 109 |

A2 Axiomatisations | 110 |

34 Deadlock and Encapsulation | 25 |

4 Recursion | 31 |

42 Transition Rules for Guarded Recursion | 33 |

43 Recursive Definition and Specification Principles | 36 |

44 Completeness for Regular Processes | 39 |

45 Approximation Induction Principle | 42 |

5 Abstraction | 47 |

52 Guarded Linear Recursion Revisited | 51 |

53 Axioms for the Silent Step | 53 |

54 Abstraction Operators | 57 |

55 An Example with Queues | 60 |

56 Cluster Fair Abstraction Rule | 63 |

6 Protocol Verifications | 69 |

A3 Initial Models | 111 |

A4 Term Rewriting | 113 |

B Structural Operational Semantics | 119 |

B2 The Meaning of Negative Premises | 121 |

B3 Bisimulation as a Congruence | 125 |

B4 Branching Bisimulation as a Congruence | 128 |

B5 Conservative Extension | 131 |

B6 Modal Logics | 133 |

Solutions to Selected Exercises | 137 |

151 | |

161 | |

### Common terms and phrases

ACPr with guarded alternating bit protocol atomic actions axiomatisation axioms Baeten basic process terms branching bisimulation equivalence branching bisimulation relation CFAR channel closed terms concurrent systems congruence conservative extension data packet datum deadlock defined Definition denoted derived equality relation equivalence relation Example execute Exercise finite function symbol Glabbeek guarded linear recursion guarded recursive specification Hence induction initial transitions intuition J.A. Bergstra linear recursive specification model checking modulo AC modulo bisimulation equivalence modulo rooted branching natural numbers negative premises normal form operational semantics ordinal numbers panth format positive after reduction process algebra process graph proof of Theorem protocol r-transitions RBB cool format read(d recursive equations regular process renaming rewrite rules right-hand side rooted branching bisimulation Sender sends signature silent step solution sound source-dependent three-valued stable model transition rules truly silent TSSs unary unary function verification weight(s X=aX Xi\E Xi\Ei