In the mCRL2 toolset, formal properties are specified in the modal mu-calculus with data. This formalism allows the use of quantifiers (∀ and ∃) to bind data variables. However, when a user puts a quantifier in the wrong place, our current set of tools maybe unable to solve the resulting model checking problem. An example …continue reading