A Presheaf Semantics for Quantified Temporal Logics

TL;DR

This paper introduces a novel semantics for quantified temporal logics using presheaf models, enhancing the understanding of system components without restricting behavior.

Contribution

It proposes a presheaf-based semantic framework for quantified temporal logics, addressing expressiveness challenges without imposing behavioral restrictions.

Findings

Develops a semantics based on counterpart models and relational presheaves.

Provides a formal foundation for reasoning about system components.

Enhances the expressiveness of quantified temporal logics.

Abstract

Temporal logics stands for a widely adopted family of formalisms for the verification of computational devices, enriching propositional logics by operators predicating on the step-wise behaviour of a system. Its quantified extensions allow to reason on the properties of the individual components of the system at hand. The expressiveness of the resulting logics poses problems in correctly identifying a semantics that exploit its features without resorting to the imposition of restrictions on the acceptable behaviours. In this paper we address this issue by means of counterpart models and relational presheaves.