2015/11/03 by Detlef Plump, Plump, Detlef, Christopher Bak +1 · 1 citation
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Software Testing and Debugging Techniques
paper · pdf · doi:10.14279/tuj.eceasst.54.780
openalex publication_date 2024/03/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30
In general, it is undecidable whether a terminating graph-transformation system is confluent or not. We introduce the class of coverable hypergraph-transformation systems and show that confluence is decidable for coverable systems that are terminating. Intuitively, a system is coverable if its typing allows to extend each critical pair with a non-deletable context that uniquely identifies the persistent nodes of the pair. The class of coverable systems includes all hypergraph-transformation systems in which hyperedges can connect arbitrary sequences of nodes, and all graph-transformation systems with a sufficient number of unused edge labels.