Temporal logics encompass a family of formalisms for the verification of computational devices, and its quantified extensions allow to reason about the properties of individual components of a system. The expressiveness of these logics poses problems in identifying a semantics that exploits its features without imposing restrictions on the acceptable behaviours. We address this issue by introducing a counterpart-based semantics and we provide a categorical presentation of such semantics in terms of relational presheaves.
A Presheaf Semantics for Quantified Temporal Logics
Trotta D.
2023
Abstract
Temporal logics encompass a family of formalisms for the verification of computational devices, and its quantified extensions allow to reason about the properties of individual components of a system. The expressiveness of these logics poses problems in identifying a semantics that exploits its features without imposing restrictions on the acceptable behaviours. We address this issue by introducing a counterpart-based semantics and we provide a categorical presentation of such semantics in terms of relational presheaves.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
Presheaf_sem.pdf
Accesso riservato
Descrizione: versione pubblicata
Tipologia:
Published (Publisher's Version of Record)
Licenza:
Accesso privato - non pubblico
Dimensione
396.64 kB
Formato
Adobe PDF
|
396.64 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
