Temporal Logic and Model Checking for Operator Precedence Words

The aim of model checking consists in the automated verification of properties concerning the behavior of a software or hardware system. The complexity of the properties to be verified and, ultimately, of the behaviors to be modeled, depends on the formalism used to express such properties. The most classical of these logic formalisms, namely LTL, CTL and CTL*, can only tackle properties that can be described as regular languages. As such, they can express simple temporal consequence, past and future eventuality and necessity. However, they are constrained into the linear structure of regular languages. Recently, the literature in the field has seen the attempt at overcoming this restriction by exploiting larger families of structured languages, such as visibly pushdown languages, which enable the modeling of nested structures. The work presented in this thesis aims to represent a significant step forward in this direction, by considering the class of Operator Precedence Languages. They were introduced by R. W. Floyd with the purpose of generating efficient parsing algorithms for programming languages. For this reason, they can represent a rather large variety of syntactic structures, even with a shape not immediately visible. Nonetheless, they enjoy the fundamental closure properties that make them appropriate for model checking. On this premise, we present a novel temporal logic formalism suitable to express and automatically verify properties on operator precedence languages. We explore the expressive power of this formalism by proving that it is at least as expressive as its main counterpart for visibly pushdown languages, while being based on a significantly more powerful language family. Finally, we give an automata theoretic procedure for model checking, for both finite and infinite words.

Lo scopo del model checking consiste nella verifica automatica di proprietà riguardanti il comportamento di un sistema hardware o software. La complessità delle proprietà da verificare e dei comportamenti da modellare dipende dal formalismo utilizzato per esprimere tali proprietà. I più classici di questi formalismi logici, in particolare LTL, CTL e CTL*, possono soltanto rappresentare proprietà riconducibili ai linguaggi regolari. Quindi, possono esprimere la semplice conseguenza temporale, l'eventualità e la necessità passate e future. Comunque, sono limitati alla struttura lineare dei linguaggi regolari. Recentemente, la letteratura in questo campo ha visto il tentativo di superare questa restrizione sfruttando famiglie più vaste di linguaggi strutturati, come i visibly pushdown languages, che permettono di modellare strutture annidate. Il lavoro presentato in questa tesi mira ad essere un significativo passo avanti in questa direzione, considerando la classe degli operator precedence languages. Essi furono originariamente introdotti da R. W. Floyd con l'intento di generare algoritmi di parsing efficienti per i linguaggi di programmazione. Per questo, possono rappresentare una varietà di strutture sintattiche piuttosto vasta, anche se dotate di una forma non immediatamente visibile. Ciononostante, godono delle fondamentali proprietà di chiusura che li rendono appropriati per il model checking. Con tale premessa, presentiamo un nuovo formalismo di logica temporale adatto a esprimere e a verificare automaticamente proprietà sugli operator precedence languages. Esploriamo la potenza espressiva di questo formalismo dimostrando che esso è almeno espressivo tanto quanto la sua principale controparte sui visibly pushdown languages, essendo inoltre basato su una classe di linguaggi ben più vasta. Infine, proponiamo una procedura per il model checking basata sulla teoria degli automi, su parole sia finite sia infinite.