Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction

DOI10.1007/978-3-031-09843-7_10MaRDI QIDQ6487310zbMATH OpenFDO

Authors Sven Schneider, Maria Maximova, Holger Giese

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-09843-7_10

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• \(k\)-inductive invariant checking for graph transformation systems
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Inductive invariant checking with partial negative application conditions
• Compositional analysis of probabilistic timed graph transformation systems
• A framework for the verification of infinite-state graph transformation systems

Cites work

• -adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation
• \(k\)-inductive invariant checking for graph transformation systems
• Compositional analysis of probabilistic timed graph transformation systems
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Fundamentals of algebraic graph transformation
• Graph and model transformation. General framework and applications
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1059243 (Why is no real title available?)
• On the border of causality: contact and confusion
• Petri nets, event structures and domains. I
• Probabilistic timed graph transformation systems
• Verifying monadic second-order properties of graph programs

Cited in

(4)

• Inductive invariant checking with partial negative application conditions
• \(k\)-inductive invariant checking for graph transformation systems
• Formal verification of invariants for attributed graph transformation systems based on nested attributed graph conditions
• Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic

This page was built for publication: Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6487310)