In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking.
In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such as TCTL. Yet, the state of the art of timed mu-calculi is underdeveloped.
In this talk, I will introduce a timed mu-calculus that is more expressive than existing timed mu-calculi, and that is the first timed mu-calculus that is more expressive than TCTL over arbitrary timed automata.

This is joint work with Rance Cleaveland and Peter Fontana.