A step up in expressiveness of decidable fixpoint logics

Fixpoint logics can express dynamic, recursive properties, but often fail to have decidable satisfiability. A notable exception to this is the family of well-behaved "guarded" fixpoint logics.

In this talk, I will describe this family of guarded logics, and discuss recent work showing that one of the main restrictions imposed in the past can be lifted to get an even richer decidable fixpoint logic. Along the way, I will mention some of the technical tools involving tree automata that we use.

This talk is based on joint work with Michael Benedikt and Pierre Bourhis.