Exercise 4: Model Checking (Without Time)

1. Give an example of model checking based on the model you have developed and using the algorithm described by Bérard et al. (2001)[34]:chapt.3
2. Make a proposal how we could implement such an algorithm with either Java or C++ or Prologue.