[TYPES] Paper announcements: MSO theory of hyperalgebraic trees is decidable

[Klaus Aehlig]

Dear colleagues,

We have the pleasure to announce that the following two papers
contain independent proofs of the following result.

The monadic second-order theory of a hyperalgebraic tree, i.e.,
a tree defined by an arbitrary second-order grammar, is decidable.
This solves an open problem posed at TLCA'01.

With best wishes,

Klaus Aehlig, aehlig at mathematik.uni-muenchen.de
Teodor Knapik, knapik at univ-nc.nc
Jolie G de Miranda, jgdm at comlab.ox.ac.uk
Damian Niwinski, niwinski at mimuw.edu.pl
Luke Ong, lo at comlab.ox.ac.uk
Pawel Urzyczyn, urzy at mimuw.edu.pl
Igor Walukiewicz, igw at labri.fr

------------------------------ Paper 1 --------------------------------

Title:       The Monadic Second Order Theory of Trees Given by Arbitrary
             Level Two Recursion Schemes Is Decidable

Authors:      Klaus Aehlig, Jolie G de Miranda, Luke Ong
             Oxford University Computing Laboratory
             (Klaus Aehlig is on leave from
              Mathematisches Institut Universitaet Muenchen)

Abstract:    A tree automaton can simulate the successful runs of a
             word or tree automaton working on the underlying word or
             tree of a second order lambda-tree. In particular the
             monadic second order theory of trees given by arbitrary,
             rather than only by safe recursion schemes of level 2
             is decidable. This solves the level 2 case of an open
             problem by Knapik, Niwinski and Urzyczyn.

URL: http://www.mathematik.uni-muenchen.de/~aehlig/pub/04-mso.ps

------------------------------ Paper 2 --------------------------------

Title: Unsafe grammars, panic automata, and decidability

Authors: Teodor Knapik, Université de la Nouvelle Calédonie,
         Damian Niwinski, Pawel Urzyczyn, Warsaw University,
         Igor Walukiewicz, Universite Bordeaux-1

Abstract: We show that the monadic second-order theory of any hyperalgebraic
          tree, i.e., an infinite tree generated by a higher-order grammar of
          level 2, is decidable. Thus, for grammars of level 2, we can remove
          the safety restriction from our previous decidability result,
          although the question if this extends to higher levels remains open.
          The proof goes via a characterization of (possibly unsafe) second-
          order grammars by a new variant of higher-order pushdown automata,
          which we call "panic automata". In addition to the standard pop_1
          and pop_2 operations, these automata have an option of a destructive
          move called "panic".  To show that the MSO theory of a tree
          recognized by a panic automaton is decidable, we give a reduction
          to a suitable parity game, which itself can be MSO-defined within
          a 2-tree. We then use the decidability of the MSO theory of a 2-tree.

URL: http://www.labri.fr/Perso/~igw/Papers/igw-amazonka.ps
------------------------------------------------------------------------------