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.

翻译：我们提出一种用于推理有向图演化的一阶线性时序逻辑。该逻辑语义基于对应范式，从而能够描述图中元素的创建、复制、合并与删除，以及拓扑结构随时间的变化。为简化实际验证过程，我们进一步引入正规范形式表示。我们利用证明助手Agda对逻辑的语法和语义进行了计算机辅助形式化，并通过强调形式化的关键方面以及量化时序逻辑在构造性证明助手中的实际应用来总结本文。