On interval logics and stopwatches in model-checking real-time systems

Abstract

Our thesis focuses on the model-checking problem, which is at the heart of both formal verification of software and algorithmic law. In general, this computational problem consists of deciding whether a given structure fulfills a given property expressed by a sentence in a logic1. These structures and logics can take many forms. We speak of algorithmic law whenever the application of that particular law is intended to be performed by a computer on a data set representing a real case. In the field of algorithmic law one needs an algorithm to decide whether a particular real case is legal or not. For a model-checking approach, the law is formalized by a sentence in some logic, whereas a case is viewed as a word structure. In the field of formal verification of software, whose goal is to test whether a program works correctly, the verification task is naturally formalized as a modelchecking problem by associating a structure to every program, and a sentence in a suitable logic to every desired property of the program [4]. The model-checking framework often allows to transform a complex and informal question into the formally precise computational problem of whether K ⊨ φ, where the input K is in some class of structures K and the input φ is in some language L. As a result, it is of practical interest in many realworld applications, providing both simple procedures and mathematical proofs of correctness. Thus, the computational complexity of the mentioned problem is of central importance. In our thesis, we discuss different formalisms as inputs of the model-checking problem to analyze their complexity. In particular, the model-checking problem of linear-temporal properties is studied, both in the presence of discrete and continuous time, with an automata-theoretic approach. The strategy in this setting is to reduce questions about models and sentences, to questions about automata, and then provide an answer using standard decision procedures for automata.