2023/05/05 by Fabio Gadducci, Gadducci, Fabio, Andrea Laretto +3
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2305.03832
openalex publication_date 2023/05/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the counterpart paradigm, thus allowing our logic to represent the creation, duplication, merging, and deletion of elements of a graph as well as how its topology changes over time. We then introduce a positive normal forms presentation, thus simplifying the actual process of verification. We provide the syntax and semantics of our logics with a computer-assisted formalisation using the proof assistant Agda, and we round up the paper by highlighting the crucial aspects of our formalisation and the practical use of quantified temporal logics in a constructive proof assistant.