logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-09182021-131748


Tipo di tesi
Tesi di laurea magistrale
Autore
LOMURNO, GIUSEPPE
URN
etd-09182021-131748
Titolo
Counterpart semantics for First-Order Linear Temporal Logic
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Prof. Gadducci, Fabio
Parole chiave
  • counterpart semantics
  • linear temporal logic
  • logic
  • proof system
  • quantified temporal logic
  • semantics
Data inizio appello
08/10/2021
Consultabilità
Tesi non consultabile
Riassunto
First-Order Linear Temporal Logic (FOLTL) is the extension of the well-known propositional Linear Temporal Logic with first-order quantification. Its interpretation is classically over Kripke-frames, that is, a set of time-points or worlds and an accessibility relation, the properties of which determine the axioms of the logic. However, such interpretation suffers limitations, since it requires restrictions on the accessibility relation between worlds. We introduce a novel semantics for FOLTL based on counterpart relations, i.e. families of partial homomorphisms between algebras. This approach overcomes most limitations, completely removing the trans-world identity problem and thus streamlining the modeling of dynamic creation, deletion and merging of entities. We also provide the logic with a Hilbert-style deductive system, and we conclude with consideration about completeness, decidability and possible extensions.
File