Analysing Graph Programs for Confluence
Graph transformation is concerned with rule based manipulation of graphs. It is intrinsically non deterministic in the sense that for a given input, several different outputs are possible. However, due to the richness of interactions between individual transformations, the computation can exhibit global determinism. This property is called confluence (or "dont care" nondeterminism) and allows us to view graph transformation as a function between inputs and outputs, an important property in application areas like model transformation. Several extensions to graph transformations have been developed that enrich the computation model such as labels, application conditions and explicit control over transformations. However, the theory behind static confluence checking has not always kept up with this evolution. The graph programming language GP, developed at York, is an experimental domainspecific language for high level problem solving on graphs and graph like structures, and implements the above extensions. The simple syntax and concise formal semantics of GP facilitate the reasoning on programs. However, it is not yet known how to obtain proofs of confluence for GP programs, which is the main aim of my research. Confluence analysis opens up the possibility of several improvements. First, it impacts the run time efficiency without compromising the semantics of transformations if one cares only of the resulting outputs for a given input, then a confluent computation can only ever produce a unique result. Furthermore, if a confluent computation fails once, then all possible executions will fail. Moreover, if a programmer intended for a program to be functional, then a counter example to confluence can trigger a development iteration. Current state of the art in confluence analysis is that of AGG and Groove. AGG is a development environment for attributed graph transformation systems that aims to provide tools for specifying and rapid prototyping of applications with complex, graph structured data. It supports confluence checking to the point of constructing conflicts and dependencies between rules, but without automated analysis. Groove is an object oriented modelling environment supported by graph transformation. It is currently one of the fastest graph transformation system. A recent development added a confluence checker that is based generation and analysis of conflicts that is only partially correct. Literature on graph transformation, graph programming and static confluence analysis is presented. Initial results of an attribution algorithm for GP labels are discussed together with early investigations of confluence analysis for graph programs. A proposal is formed, based on the surveyed literature and these initial results. The overall goals are presented together with specific success criteria and strategy for achieving them.