<p>This book helps readers easily learn basic model checking by presenting examples, exercises and case studies. The toolset mCRL2 provides a language to specify the behaviour of distributed systems, in particular where there is concurrency with inter-process communication. This language allows us to analyse a distributed system with respect to its functional requirements. For example, biological cells, supply chain management systems, patient support platforms, and communication protocols.</p>The underlying technique is based on verifying requirements through model checking. The book explains the syntax of mCRL2 and offers modelling tips and tricks.<p></p>