Evènement pour le groupe Graphes et Logique

Date 2011-05-03  11:00-12:00
TitreFirst-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.  
Lieusalle 76 
OrateurChristopher Broadbent 
UrlOxford University 

Aucun document lié à cet événement.

Retour à l'index