Floyd languages for infinite words

Nowadays many software systems are designed to work without interruption: for instance operating systems are required to provide continuously their services to the users, and web applications and verification of critical and concurrent systems represent a typical scenario where endless computations are involved. The behavior of systems operating forever can be formally specified by means of omega-languages, a class of languages defined as sets of infinite words of symbols. Theory on omega-languages dates back to the sixties, with the pioneering works of Büchi and Muller on finite-state automata able to recognize infinite strings. More recently, omega-languages have been studied as an extension of Visibly Pushdown Languages (VPL), a class of deterministic context-free languages which model strings as nested words of symbols. This work of thesis follows this line of research with the aim of investigating Floyd languages (FL), a traditional formalism introduced in 1963 by R.Floyd and recently rediscovered and further investigated, generalizing them to languages of infinite words. FLs are one of the early classes of Deterministic Context-Free (DCF) languages and are defined by operator precedence grammars, renamed Floyd Grammars (FG). Research on FLs began decades ago (from the first work of Floyd) and has been then interrupted after the introduction of advanced parsing techniques for more expressive languages, as LR(k). Renewal of interest in the study of FLs, which motivates the investigation carried on in this thesis, derived from the discovery of recent surprising results: along the path of research on parentheses-like languages resumed with the definition of VPLs and their characterization in terms of a class of automata (named Visibly Pushdown Automata), recent studies revealed the potential of FLs, proving that FLs are a proper superclass of VPLs and represent the largest known DCF family closed under all classical operations enjoyed by regular languages. Furthermore, FLs have been recently characterized by means of a complementary class of stack-based automata (Floyd Automata) and this result leads quite naturally to a further extension of FLs to omega-languages, opening new perspectives for the introduction of this class of languages in several application contexts, as infinite-state model-checking. The main issue of this thesis is, thus, the investigation of this novel class of omega-languages and the focus of this study consists in the characterization of suitable abstract machines to define these languages. Research on the theoretical properties enjoyed by Floyd omega-languages, which is the subject matter of this thesis, indeed, represents a fundamental step towards applicability of this formalism to domains as verification of properties of critical systems by means of advanced model-checking techniques.

Molti dei moderni sistemi software sono progettati per funzionare per sempre: si pensi alle applicazioni web o embedded o ai sistemi operativi, che hanno come tipico requisito di garantire ai loro utenti la continua disponibilità di determinati servizi, ed ogni loro interruzione viene percepita come un vero e proprio fallimento. Le proprietà di sistemi che compiono ininterrottamente le loro elaborazioni senza fine possono essere naturalmente specificate e verificate ricorrendo ai concetti e ai formalismi propri della teoria dei linguaggi omega, una classe di linguaggi formali composti da parole di lunghezza infinita. Gli studi sui linguaggi omega risalgono agli anni Sessanta, quando Büchi e Muller presentarono i loro lavori pionieristici su automi in grado di riconoscere sequenze infinite di simboli. Più recentemente, lo studio sugli omega linguaggi è stato ripreso con l'estensione, al campo dei linguaggi di parole infinite, dei Visibly Pushdown Languages (VPL), una classe di linguaggi deterministici context-free che rappresentano le stringhe finite di un linguaggio come parole dotate di una struttura più ricca di quella che una sequenza lineare di simboli può conferire ("nested word"). Proseguendo questa linea di ricerca nell'ambito dei linguaggi formali, questo lavoro di tesi mira ad investigare le proprietà dei Linguaggi di Floyd (FL), un formalismo classico introdotto nel 1963 da R.Floyd, estendendo questa famiglia di linguaggi al mondo dei linguaggi infiniti. Gli FL rappresentano una delle prime classi di linguaggi deterministici context-free (DCF) e sono definiti da grammatiche a precedenza di operatori (operator precedence grammars). Storicamente, dopo la loro introduzione nel 1963, lo studio sugli FL venne interrotto con l'emergere di formalismi più potenti ed espressivi per il parsing dei linguaggi di programmazione, come LR(k). L'interesse sui FL riprese solo successivamente, in seguito a nuove ricerche sui linguaggi caratterizzati da una struttura a parentesi delle loro parole, quali i linguaggi di mark-up, e recentemente si è mostrato come proprio i VPL siano una sottoclasse stretta dei FL, e come questi ultimi rappresentino la più ampia famiglia nota di linguaggi DCF chiusi rispetto a tutte le operazioni tipiche dei linguaggi regolari. Inoltre, gli FL sono stati caratterizzati in termini di una classe equivalente di automi, ed è proprio questo fondamentale risultato a consentire l'estensione dei Linguaggi di Floyd al campo della teoria omega, aprendo interessanti prospettive per la loro introduzione in numerosi contesti applicativi, in particolare come un formalismo adatto per il model checking a stati infiniti. Il tema centrale di questa tesi è lo studio di questa nuova classe di linguaggi omega, con l'obiettivo di darne una definizione appropriata attraverso adeguati formalismi operazionali, in linea con la teoria omega classica, e questo rappresenta un primo determinante passo per future applicazioni di questa famiglia di linguaggi nell'ambito della verifica automatica di proprietà di sistemi attraverso model-checking.