A PBES can be solved by iterating to the least or greatest fixpoint in a (trans)finite number of steps. So I thought “Why not add that as a tool to mCRL2?”. This turned into `pbesiteration`.
We will briefly explain fixpoint iteration in the context of PBESs and describe how the tool works.
At first, this was just an attempt for me to develop some skills around the mCRL2 code base. It turned out to be an interesting example of how making tools work in practice is as crucial for success as achieving new theoretical results.