On Languages and a Strictly Positive Fragment of Linear Temporal Logic

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.