Higher-order recursion schemes and the monadic closure

Date: Thursday, November 25, 2010
Speaker: Olivier Serre
Venue: IST Austria

Starts at 15:30

In this talk I will first introduce the notion ofhigher-order recursion schemes and give the tightconnection that exists with automata theory. In thiswork, we use schemes as a way to produce an infinitetree: with any schemes one associate a (unique) infinitetree. A paper by Luke Ong [LICS’06] establishes that anytree generated in such a way has a decidable second ordertheory.

We present here a stronger result, namely that given a tree tdescribed by a scheme and an MSO formula phi, the treet_phi, obtained by marking thos nodes in t where phiholds, can be (effectively) generated by a scheme. Acorollary of this result is that the trees generated byschemes are closed by successive application of an MSOinterpretation followed by unfolding.

The talk will be based on the following papers:

  • Arnaud Carayol, Matthew Hague, Antoine Meyer, Luke Onget Olivier Serre. Winning regions of higher-orderpushdown games, in Proceedings of the Twenty-Third AnnualIEEE Symposium on Logic in Computer Science, LICS 2008,IEEE Computer Society, pp.193-204, 2008.
  • Matthew Hague, Andrzej Murawski, Luke Ong et OlivierSerre. Collapsible Pushdown Automata and RecursionSchemes, in Proceedings of the Twenty-Third Annual IEEESymposium on Logic in Computer Science, LICS 2008, IEEEComputer Society, pp.452-461, 2008.
  • Christopher Broadbent, Arnaud Carayol, Luke Ong etOlivier Serre. Recursion Schemes and Logical Reflection,in Proceedings of the Thwenty-fifth Annual IEEE Symposiumon Logic in Computer Science, LICS 2010, IEEE ComputerSociety, pp. 120-129, 2010.

(Very) Short Bio:

Olivier Serre is a full-time researcher employed by CNRSin LIAFA (University Paris 7 & CNRS) since October2005. He is also a part-time assistant professor at EcolePolytechnique. Previously he did a PhD (2001-2004) underthe direction of Anca Muscholl and Jean-Eric Pin. Hismain research interests are games in computer science,automata theory, infinite states system and logic.

Posted in RiSE Seminar