Abstract
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.
Type
Publication
In Recent Trends in Algebraic Development Techniques (WADT2022)
Davide Trotta
Postdoc
I am a mathematician, and my research is mainly focused on categorical logic and its applications in theoretical computer science.