Corelab Seminar

Antonis Achilleos
The complexity of identifying characteristic formulas for μHML

We examine the complexity of determining whether a formula οf the maximal-fixed-point fragment of the Henessy Milner logic with recursion characterizes a process up to bisimulation equivalence. We discover that the problem is EXP-complete. The decision procedure that establishes this upper bound is based on a two-player game.