Temporal Logic Specifications: Expressiveness, Satisfiability and Realizability

The main topic of this thesis concerns temporal logics, with particular attention to their expressive power and to the satisfiability and realizability problems. Temporal logics are nowadays a well-established formalism for expressing properties about sequences. Their connection with first- and second-order logic, automata and formal verification makes temporal logics not only a powerful theoretical framework, but also a valuable tool in practical scenarios (e.g., for the specification of con- current systems). On the theoretical side, one typical problem when dealing with a temporal logic is to characterize exactly its expressive power, that is to give the set of all and only the properties that it can formalize. On a more practical side, there are two important problems that are considered when using temporal logics as specification languages: (i) the satisfiability problem, that is finding whether a given formula admits at least one model; and (ii) the realizability problem, namely to find whether a given formula is implementable. In formal verification, satisfiability can be used as a sanity check for detecting vacuous specifications (i.e., valid or unsatisfiable formulas), while realizability can be used to check the existence of correct-by-construction implementations (and their consequent synthesis). In this thesis, we try to stay in the intersection between the theoretical and the practical sides of temporal logics, by accompanying the theoretical results (whenever possible) with algorithms, implementations and experimental evaluations. Theory: We introduce three fragments of Linear Temporal Logic with Past (LTL+P) and study their expressive power: (i) for the first fragment (called LTLEBR+P), we prove that it is expressively complete with respect to the (semantically) safety fragment of LTL+P (a safety property is a property in which a violation is irremediable); (ii) the second fragment (called LTLEBR) is obtained from LTLEBR+P by removing past operators; we prove that LTLEBR is strictly less expressive than full LTLEBR+P; (iii) the third fragment is called GR-EBR and it is an extension of LTLEBR+P for expressing properties beyond the safety fragment; we compare its expressive power with the Temporal Hierarchy of Manna and Pnueli. In addition we propose a first-order syntactical characterization (called Safety-FO) that captures the semantically safety fragment of the first-order logic of one successor: this result can be considered as the version of Kamp’s Theorem for safety properties. Problems and Algorithms: We consider the satisfiability problem of LTL+P and the realizability problem from LTLEBR+P and GR-EBR specifications. Particular attention is devoted to the use of symbolic algorithms instead of classical explicit-state ones. We implement all the algorithms that we propose and we compare them with competitor tools. From the outcomes of the experimental evaluations, it is often evident that our symbolic techniques can solve instances of sizes that are prohibitive for the other tools based on an explicit-state representation. Last but not least, we consider an industrially relevant problem in the context of real-time requirements (i.e., properties expressing not only the ordering between events but also the amount of time elapsed between two events). We define and formalize the compatibility problem of timed requirements, give symbolic algorithms for this problem, and implement and evaluate the proposed procedure.

L’argomento principale di questa tesi riguarda le logiche temporali, con particolare attenzione alla loro potenza espressiva e ai problemi di soddisfacibilità e realizzabilità. Le logiche temporali sono oggigiorno un formalismo ben consolidato per esprimere proprietà su sequenze. La loro connessione con logiche al primo e second’ordine, con gli automi e con la verifica formale ha reso le logiche temporali non solo un potente framework teorico, ma anche un prezioso strumento pratico (per esempio per la specifica di sistemi concorrenti). Sul lato teorico, uno dei tipici problemi quando si lavora con una logica temporale è di caratterizzare esattamente la sua potenza espressiva, cioè di dare l’insieme di tutte e sole le proprietà che essa è in grado di formalizzare. Su un lato più pratico, ci sono due importanti problemi che vengono considerati quando si usano le logiche temporali come linguaggi di specifica: (i) il problema di soddisfacibilità, cioè stabilire se la formula data ammette almeno un modello; e (ii) il problema di realizzabilità, cioè stabilire se la formula data è implementabile. In verifica formale, la soddisfacibilità può essere usata come un controllo per individuare specifiche vacue (cioè formule valide o insoddisfacibili), mentre la realizzabilità può essere usata per controllare l’esistenza di implementazioni corrette per costruzione (e la loro conseguente sintesi). In questa tesi, cerchiamo di porci nell’intersezione tra il lato teorico e quello pratico delle logiche temporali, accompagnando i risultati teorici (quando possibile) con algoritmi, implementazioni e valutazioni sperimentali. Teoria: Introduciamo tre frammenti della Logica Temporale Lineare con Passato (LTL+P) e studiamo la loro potenza espressiva: (i) per il primo frammento (chiamato LTLEBR+P) dimostriamo che è espressivamente completo rispetto al frammento safety semantico di LTL+P (una proprietà si dice essere di safety se ogni sua violazione è irrimediabile); (ii) il secondo frammento (chiamato LTLEBR) è ottenuto da LTLEBR+P rimuovendo gli operatori al passato; dimostriamo che LTLEBR è strettamente meno espressivo di LTLEBR+P (iii) il terzo frammento `e chiamato GR-EBR ed è un’estensione di LTLEBR+P per esprimere proprietà che vanno oltre al frammento safety; confrontiamo la sua potenza espressiva con la Temporal Hierarchy di Manna e Pnueli. Inoltre proponiamo una caratterizzazione sintattica al prim’ordine (chiamata Safety-FO) che cattura il frammento safety semantico della logica al prim’ordine con un successore: questo risultato può essere considerato come la versione del Teorema di Kamp per proprietà safety. Problemi e Algoritmi: Consideriamo il problema di soddisfacibilità per LTL+P ed il problema di realizzabilità per specifiche di LTLEBR+P e GR-EBR. Particolare attenzione è rivolta all’uso di algoritmi simbolici al posto di quelli classici espliciti. Implementiamo tutti gli algoritmi che abbiamo proposto e li confrontiamo con gli altri tool concorrenti. Dai risultati delle valutazioni sperimentali, è spesso evidente che le nostre tecniche simboliche riescono a risolvere istanze di dimensioni che sono proibitive per gli altri tool basati su una rappresentazione esplicita. Ultimo, ma non per importanza, consideriamo un problema di rilevanza industriale nel contesto di requisiti real-time (cioè proprietà che esprimono non solo l’ordine tra gli eventi ma anche la quantità di tempo passata tra i due). Definiamo e formalizziamo il problema di compatibilità di requisiti temporizzati, diamo degli algoritmi simbolici per questo problema, e implementiamo e valutiamo la procedura proposta.