A Presheaf Semanticsfor Quantified Temporal Logics

Temporal logics stands for a widely adopted family of formalisms forthe verification of computational devices, enriching propositional logics by oper-ators predicating on the step-wise behaviour of a system. Its quantified extensionsallow to reason on the properties of the individual components of the system athand. The expressiveness of the resulting logics poses problems in correctly iden-tifying a semantics that exploit its features without resorting to the imposition ofrestrictions on the acceptable behaviours. In this paper we address this issue bymeans of counterpart models and relational presheaves.