Preface
Acknowledgments
Introduction
Welcome
Who Is This Book For?
What Is Covered inΒ This Book?
Your Feedback andΒ Errata
Contents
1 Introducing mCRL2
1.1 What is mCRL2 All About?
1.2 History of mCRL2
1.3 Why mCRL2?
1.4 Learning mCRL2
1.5 Other Educational Material
1.6 The mCRL2 Toolkit
1.7 Other Toolsets
2 Automata to Represent Behaviour
2.1 Why Make Models?
2.2 Developing Models in mCRL2
2.2.1 Hello-World Example
2.2.2 Using the Terminal
2.2.3 State-Space and Actions
2.3 Using the GUI
3 Communicating Processes
3.1 Communication Among Actions
3.1.1 A Coffee Vending Machine
3.2 Deadlock
3.3 Synchronous Versus Asynchronous Communication
3.4 Blocking and Renaming Actions
3.5 Hiding Actions
4 Behavioural Equivalences
4.1 Trace Equivalence
4.1.1 Weak Trace Equivalence
4.2 Strong Bisimulation
4.3 Branching Bisimulation
4.4 Divergence Preserving Branching Bisimulation
5 Data Types and Data-Dependent Behaviour
5.1 Sending/Receiving Data
5.1.1 Operators on Data
5.2 Conditions
5.3 Data Structures
5.3.1 Lists
5.3.2 Sets
5.3.3 Bags
5.4 User Defined Functions
5.4.1 Defining Constants
5.4.2 Ξ»-Expressions
5.5 Constructors of a Data Type
5.6 Defining a Struct Data Type
5.7 Modelling the Alternating Bit Protocol
5.8 Modelling Milner's Cyclic Scheduler
6 Model-Checking
6.1 Hennessy-Milner Logic
6.2 Model-Checking with mCRL2
6.2.1 Parameterised Boolean Equation System
6.3 Action Formulas
6.4 Regular Formulas
6.5 Formulas with Data and Quantifiers
6.6 What to do if Model-Checking Becomes Time Consuming?
6.6.1 Reduce the Problem Size
6.6.2 Optimising and Transforming a PBES
6.6.3 Model-Check Explicit State Spaces
6.6.4 CADP
6.6.5 LTSmin and Pbessolvesymbolic
7 The Modal Β΅-Calculus
7.1 Minimal Fixed Points
7.1.1 Minimal Fixed Point Formulas with Data
7.2 Maximal Fixed Points
7.2.1 Maximal Fixed Points with Data
7.3 Combining Minimal and Maximal Fixed Points
7.4 Modelling a Movable Patient Support Unit and Its Requirements
7.4.1 Formal Specification
7.4.2 Requirements Analysis
8 Linear Processes and Parameterised BESs
8.1 Linear Processes
8.2 Optimising an LPS
8.2.1 Rewriting a Linear Process
8.2.2 Constant Elimination
8.2.3 Parameter Elimination
8.2.4 Sum Instantiation and Sum Elimination
8.2.5 Action Renaming
8.2.6 Unfolding Parameters
8.3 Parameterised Boolean Equation Systems
8.4 Optimising PBESs
8.4.1 Rewriting PBESs
8.4.2 Constant Elimination
8.4.3 Parameter Elimination
9 Applications: Puzzles and Games
9.1 Magic Square
9.2 Bridge Crossing
9.3 Weight Bars Crossing
9.4 The Wolf, the Goat and Cabbage
9.5 Jumping Frogs
9.6 Tic-Tac-Toe
10 Applications: Distributed Algorithms
10.1 Heartbeat Protocols
10.2 The Binary Heartbeat Protocol
10.3 The Static Heartbeat Protocol
10.4 The Expanding and the Dynamic Heartbeat Protocol
Appendix A Specifications of Protocols in mCRL2
A.1 Binary Heartbeat Protocol
A.2 Static Heartbeat Protocol
Appendix B Solutions
Appendix References
Index