Document type
Master thesisPublication date
Publication license
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/215189
On Languages and a Strictly Positive Fragment of Linear Temporal Logic
Journal Title
Authors
Director/Tutor
Journal ISSN
Volume Title
Related resource
Abstract
This thesis explores various characterizations of regular and star-free languages and in troduces a novel syntactic fragment of Linear Temporal Logic (LTL), called Strictly Pos itive Linear Temporal Logic (SPLTL), inspired by the Reflection Calculus. The opening
chapter provides a comprehensive survey of regular languages, characterized by regular
expressions, regular grammars, finite automata, and Monadic Second-Order logic over
words. We conclude the exposition with a detailed proof of Büchi’s Theorem, which
bridges automata and logic. The discussion then shifts to star-free languages, emphasiz ing their representation using LTL. An exhaustive proof of the Completeness Theorem
for LTL is also provided.
The principal contribution of this thesis is the definition and analysis of SPLTL, which
aims to achieve improved complexity compared to LTL. We establish several foundational
results for SPLTL and show its soundness concerning the standard semantic framework
of LTL. However, proving the completeness of SPLTL presents difficulties, primarily due
to the absence of the disjunction operator in the SPLTL formalization.
Despite these challenges, we think that this thesis introduces valuable insights and
results that lay the groundwork for future research. It paves the way for a more in-depth
investigation into the completeness of SPLTL and its potential applications.
Description
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2023-2024. Tutor: Joost Johannes Joosten
Subject (English)
Citation
Citation
ACEVEDO, Lucas Uzías. On Languages and a Strictly Positive Fragment of Linear Temporal Logic. [consulted: 18 of June of 2026]. Available at: https://hdl.handle.net/2445/215189