Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems: Full Version

Barbara König; Arend Rensink; Lara Stoltenow; Fabian Urrigshardt

doi:10.48550/arXiv.2504.08617

Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems: Full Version

Barbara König, Arend Rensink, Lara Stoltenow, Fabian Urrigshardt

Formal Methods and Tools

Research output: Working paper › Preprint › Academic

21 Downloads (Pure)

Abstract

This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

Original language	English
Publisher	ArXiv.org
Number of pages	28
DOIs	https://doi.org/10.48550/arXiv.2504.08617
Publication status	Published - 11 Apr 2025

Keywords

Reachability Analysis, CEGAR, Reactive Systems, Abstract Interpretation, Graph Transformation

Access to Document

10.48550/arXiv.2504.08617Licence: CC BY

2504.08617v1Final published version, 809 KBLicence: CC BY

1 Conference contribution

Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems
König, B., Rensink, A., Stoltenow, L. & Urrigshardt, F., 13 Jun 2025, Graph Transformation - 18th International Conference, ICGT 2025, Held as Part of STAF 2025, Proceedings: 18th International Conference, ICGT 2025, Held as Part of STAF 2025, Koblenz, Germany, June 11–12, 2025, Proceedings. Endrullis, J. & Tichy, M. (eds.). Springer, p. 157-176 20 p. (Lecture Notes in Computer Science; vol. 15720 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Cite this

@techreport{c57e1fabdb2b4438b065785d0a46f586,

title = "Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems: Full Version",

abstract = "This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.",

keywords = "Reachability Analysis, CEGAR, Reactive Systems, Abstract Interpretation, Graph Transformation",

author = "Barbara K{\"o}nig and Arend Rensink and Lara Stoltenow and Fabian Urrigshardt",

year = "2025",

month = apr,

day = "11",

doi = "10.48550/arXiv.2504.08617",

language = "English",

publisher = "ArXiv.org",

type = "WorkingPaper",

institution = "ArXiv.org",

}

TY - UNPB

T1 - Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems

T2 - Full Version

AU - König, Barbara

AU - Rensink, Arend

AU - Stoltenow, Lara

AU - Urrigshardt, Fabian

PY - 2025/4/11

Y1 - 2025/4/11

N2 - This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

AB - This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.

KW - Reachability Analysis, CEGAR, Reactive Systems, Abstract Interpretation, Graph Transformation

U2 - 10.48550/arXiv.2504.08617

DO - 10.48550/arXiv.2504.08617

M3 - Preprint

BT - Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems

PB - ArXiv.org

ER -

Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems: Full Version

Abstract

Keywords

Access to Document

Fingerprint

Research output

Counterexample-Guided Abstraction Refinement for Generalized Graph Transformation Systems

Cite this