POMC. A model checking tool for operator precedence languages on omega-words

Model Checking of systems (both hardware and software) is a prominent research area in the Formal Verification field, with many practical applications. Operator Precedence Languages (OPL) are, so far, the most expressive class of languages which can be suitably used in model checking due to their monadic second order characterization, the decididability of the containment problem, and the property of closure under intersection. Therefore, despite they were introduced in the sixties by Robert W. Floyd and then almost abandoned, their study has been recently resumed. On their basis, the First-Order complete Precedence Oriented Temporal Logic (POTL) and a model checking tool, the Precedence Oriented Model Checker (POMC), have been introduced to verify specifications written in POTL on Operator Precedence Automata (OPAs), which are Pushdown Automata appropriately modified to recognize OPLs. In this thesis we improve the performances of POMC and extend its functionalities with a model checking algorithm for Operator Precedence Büchi Automata, i.e. automata accepting omega-OPLs, when omega indicates that the languages is composed of infinite words. We prove its efficiency and its utility with some experiments.

Il "Model Checking" (controllo di modello) di sistemi (sia hardware che software) è una rilevante area di ricerca nel settore della Verifica Formale, con numerose applicazioni pratiche. I Linguaggi a Precedenza d'Operatore (OPL, in inglese) sono, allo stato attuale, la classe di linguaggi più espressiva che può essere opportunamente impiegata nel Model Checking grazie al fatto che è caratterizzabile in termini di una Logica Monadica del Secondo Ordine, il problema del contenimento è decidibile per essa, ed è chiusa rispetto all'intersezione. Dunque, sebbene sia stata introdotta sessanta anni fa da Robert W. Floyd e da allora quasi abbandonata, il loro studio è stato ripreso di recente: sulla loro base sono stati presentati la Logica Temporale a Precedenza d'Operatore (POTL, in inglese), che è completa rispetto al primo ordine, e uno strumento di model checking, chiamato Model Checker a Precedenza d'Operatore (POMC, in inglese), allo scopo di verificare specifiche scritte in POTL su Automi a Precedenza d'Operatore (OPA, in inglese), che appunto sono automi a pila che riconoscono gli OPL. In questa tesi abbiamo migliorato le prestazioni di POMC e esteso le sue funzionalità con un algoritmo di Model Checking per Automi di Büchi a Precedenza d'Operatore , cioè automi che accettano omega-OPL, dove omega indica che il linguaggio è composto da stringhe infinite. Abbiamo infinite dimostrato la sua efficienza e la sua utilità con alcuni esperimenti.