|
Evènement pour le groupe Graphes et Logique
Date | 2011-05-03 11:00-12:00 |
Titre | First-Order Logic, Collapsible Pushdown Graphs and Automaticity |
Résumé | A higher-order pushdown automaton is a device endowed with a stack of nested-
stacks. Inductively an order-1 stack is that of a conventional pushdown
automaton. An order-(n+1) stack is a stack of order-n stacks. The transition
graphs of such automata are well-understood. 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 higher-order 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 `higher-order recursion
schemes'---natural systems of rewrite rules on non-terminals bearing higher-
order types. Walukiewicz and others established this at order-2 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 order-2 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 order-2 CPDA graphs are tree automatic and hence have decidable FO
theories. In this talk I will explain some somewhat surprising results that
show first-order logic to be undecidable at order-3 and above. Some of these
results are particularly strong---for example order-4 graphs generated by a
CPDA that use just order-2 links suffer undecidable first-order model-checking
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 nested-words. This offers some advantages
over tree-automaticity in that it allows us to capture precisely the order-2
CPDA graphs and also account for the difference between non-collapsible and
standard order-2 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 nested-words. We hope
this might offer a neater framework in which to work as it would restore the
inductive structure enjoyed by non-collapsible higher-order stacks.
|
Lieu | salle 76 |
Orateur | Christopher Broadbent |
Email | chbroadbent@googlemail.com |
Url | Oxford University |
Aucun document lié à cet événement. RetourRetour à l'index
| |