Document type
Master thesisPublication date
Publication license
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/207695
On interval logics and stopwatches in model-checking real-time systems
Journal Title
Authors
Director/Tutor
Journal ISSN
Volume Title
Related resource
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.
Description
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2021-2022. Tutor: Joost Johannes Joosten i Moritz Müller
Subject (English)
Citation
Citation
LÓPEZ CHAMOSA, Marina. On interval logics and stopwatches in model-checking real-time systems. [consulted: 14 of August of 2026]. Available at: https://hdl.handle.net/2445/207695