It helped me a great deal to have the book and use the mCRL2 tool extensively. The assignments are very tricky to the point of being frustrating; however, with perseverance, the success made me really feel good about learning this material. I suppose that the tricky quizzes are necessary to emphasize the point that modeling processes is fundamentally a tricky business. So in this regard, this course delivers a valuable experience. Since the book was published, the mCRL2 syntax has changed -- the rename operator is litterally "rename({a->b}, process)", not "comm({a->b}, process)" as described in the book.

Interesting course about model checking, but maybe it would be helpful to have more examples and sometimes more detailed explanations about some concepts.