The 'Safety' Restriction

Jolie de Miranda

(Oxford)

Higher-order grammars were first introduced in the 1980s by Goerdt as a means of generating languages. A higher-order grammar consists of a set of typed rewrite rules and is classified as being of level n if the highest type level occurring in it is n. Level-0 grammars correspond to the regular languages and level-1 grammars correspond to the context-free. The infinite hierarchy of languages generated by higher-order grammars is often considered to be a more natural alternative to the Chomsky hierarchy of languages.

Recently (Knapik, Niwinski, Urzyczyn 2001), the definition of higher-order grammars has been adjusted to generate more general structures: potentially infinite term trees, and this has generated much interest from communities in infinite-state verification.

In this talk we consider higher-order grammars in both settings (language-theoretic and verification-oriented) and consider the "safety problem". In both settings it has been shown that many good algorithmic and behavioural properties hold provided that the "safety" restriction is satisifed; here safety is a syntactic restriction on the rewrite rules of the higher-order grammar. However, very little is (was) known about the state of unsafe grammars. My thesis has made an attempt to rectify this situation.
Tuesday 8th November 2005, 14:00
Robert Recorde Room
Department of Computer Science