Solving decision problems using parameterised Boolean equation systems

In the mCRL2 toolset, model checking problems are solved by first encoding
them into parameterised Boolean equation systems (PBES) and then finding
the solution to this PBES. However, PBESs are very expressive and can be
used to encode more types of decision problems. For example, one can also
encode equivalence problems and scheduling problems in the framework
of PBESs. The goal of this assignment is to further investigate the
expressiveness of PBESs. Possible directions are: defining an encoding
of the longest common substring problem in PBES [1] or encoding PBESs
that express whether a certain mu-calculus formula is satisfiable [2],
i.e., whether there is a model that satisfies the formula. Inspiration
can also be drawn from common problems in the SAT/SMT-solving world.

[1]: Hutagalung M., Lange M. (2014) Model Checking for String
Problems. In: Hirsch E.A., Kuznetsov S.O., Pin J.E., Vereshchagin
N.K. (eds) Computer Science - Theory and Applications. CSR 2014. Lecture
Notes in Computer Science, vol 8476. Springer.

[2]: Friedmann, Oliver and Lange, Martin and Latte, Markus -
Satisfiability Games for Branching-Time Logics, lmcs:761 - Logical
Methods in Computer Science, October 16, 2013, Volume 9, Issue 4.