# name
On Languages and a Strictly Positive Fragment of Linear Temporal Logic

# metadata.dc.description[].value
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2023-2024. Tutor:  Joost Johannes Joosten

# metadata.dc.description.abstract[].value
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.

# metadata.dc.source[].value
Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

# metadata.dc.subject.classification[].value
Tractament del llenguatge natural (Informàtica)

# metadata.dc.subject.other[].value
Natural language processing (Computer science)

# metadata.dc.title[].value
On Languages and a Strictly Positive Fragment of Linear Temporal Logic