
Intitulé:
FirstOrder Logic, Collapsible Pushdown Graphs and Automaticity du groupe Graphes et Logique

Date  20110503 11:0012:00 
Titre  FirstOrder Logic, Collapsible Pushdown Graphs and Automaticity 
Résumé  A higherorder pushdown automaton is a device endowed with a stack of nested
stacks. Inductively an order1 stack is that of a conventional pushdown
automaton. An order(n+1) stack is a stack of ordern stacks. The transition
graphs of such automata are wellunderstood. They are intimately related to
the Caucal hierarchy, which subsumes a variety of interesting graphs and whose
members all enjoy decidable MSO theories.
It appears necessary to extend higherorder pushdown automata with additional
structure in the form of `links' if we are to obtain a model of computation
capable of generating the same class of trees as `higherorder recursion
schemes'natural systems of rewrite rules on nonterminals bearing higher
order types. Walukiewicz and others established this at order2 in an ICALP
2005 paper, whilst Hague et al. generalised this to all orders in LICS 2008.
The latter paper revealed the disappointing fact that order2 CPDA transition
graphs have undecidable MSO theories. They left open the question of first
order logic.
Initial progress on this was made by Kartzow in a STACS 2010 paper in which he
showed that order2 CPDA graphs are tree automatic and hence have decidable FO
theories. In this talk I will explain some somewhat surprising results that
show firstorder logic to be undecidable at order3 and above. Some of these
results are particularly strongfor example order4 graphs generated by a
CPDA that use just order2 links suffer undecidable firstorder modelchecking
problems even when we restrict ourselves to sentences with no quantifier
alternation!
I will also mention some positive results. We have rebuilt Kartzow's work via
a notion of automaticity based on nestedwords. This offers some advantages
over treeautomaticity in that it allows us to capture precisely the order2
CPDA graphs and also account for the difference between noncollapsible and
standard order2 automata in terms of our notion of automaticity. It also
suggests a notion of prefix rewrite system that does at order 2 what
traditional rational prefix rewrite systems do for standard pushdown automata.
If time permits, I will briefly outline some future work that is planned for
next year. This is inspired by the results above and proposes replacing
collapsible pushdown stacks with iterative stacks of nestedwords. We hope
this might offer a neater framework in which to work as it would restore the
inductive structure enjoyed by noncollapsible higherorder stacks.

Lieu  salle 76 
Orateur  Christopher Broadbent 
Email  chbroadbent@googlemail.com 
Url  Oxford University 
Aucun document lié à cet événement.
Retour Retour à l'index
 