Specification and verification of a linear-time temporal logic for graph transformation
From MaRDI portal
Publication:6535505
DOI10.1007/978-3-031-36709-0_2zbMATH Open1545.6807MaRDI QIDQ6535505
Andrea Laretto, Davide Trotta, Fabio Gadducci
Publication date: 12 January 2024
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Temporal logic (03B44) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Expressiveness and complexity of graph logic
- The monadic second-order logic of graphs. XII: Planar graphs and planar maps
- Isabelle/HOL. A proof assistant for higher-order logic
- The Lean 4 theorem prover and programming language
- Monadic second-order incorrectness logic for GP 2
- Verifying graph programs with monadic second-order logic
- The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
- A tableau construction for finite linear-time temporal logic
- Counterpart Semantics for a Second-Order μ-Calculus
- Auto in Agda
- Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D.
- Sesqui-Pushout Rewriting
- A Temporal Graph Logic for Verification of Graph Transformation Systems
- Dependently Typed Programming in Agda
- An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
- Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic
- Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions
- Correct Hardware Design and Verification Methods
- Relational and partial variable sets and basic predicate logic
- Types for Proofs and Programs
- Metric temporal graph logic over typed attributed graphs
- Real-time policy enforcement with metric first-order temporal logic
Related Items (1)
This page was built for publication: Specification and verification of a linear-time temporal logic for graph transformation
