2017, Amaldev Manuel’s visit

With Paul Gastin we worked on reversible regular languages. These are regular languages that are recognised by semigroups with an involution. We found out previously that many classes of these languages have natural logical characterisations in terms of predicates that are not oriented (like between(x,y,z), neighbour(x,y), etc.). In fact many of the correspondences (FO-aperiodic, MSO-finite, etc.) lift to the new setting. But the situation is different for classes like reversible threshold testable. The work focussed on how to prove these correspondences using categories.

With Stefan Goeller we worked on characterising the data complexity of mu-calculus model checking in terms of the games they yield.

With Thomas Colcombet we worked on deciding a subclass of mu-calculus defined using the comp-operator.