title: Extensions of the first-order modal mu-calculus

The first-order modal mu-calculus is a highly expressive logic that
is particularly suited for reasoning about systems in which data
plays a non-trivial role. While most reasonable properties can
easily be expressed in this logic, there are certain properties
that are less trivially expressed, or even impossible. In this
assignment you are to identify properties that cannot (easily) be
expressed in the first-order modal mu-calculus, but that can be
expressed in other logics. Examples could be certain classes of
hyper properties, that simultaneously reason about multiple paths.
Moreover, you are to investigate extensions of the first-order modal
mu-calculus that would allow you to express such properties after
all. A starting point could be the study of hybrid modal logics.