un)boundedness - logic, automata and games with countdow

I will present extensions of: the modal fixpoint calculus, parity games, and parity automata - designed to capture (un)boundedness-related phenomena. The extensions lift the classical logic~games~automata correspondence beyond regular properties - in particular the logic and automata define the same languages. I will discuss results and conjectures regarding expressive power and decidability. This is a joint work with Mikołaj Bojańczyk and Bartek Klin, and the model extends the ideas of Hella, Kuusisto and Rönnholm.