Checking Graph-Transformation Systems for Confluence
Abstract
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.26.367
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.26.367.347
Hosted By Universitätsbibliothek TU Berlin.