Graphs and Graph Transformation

Contact: Milan Lopuhaä-Zwakenberg

Graphs are an essential tool for modeling high-tech systems. The complexity of a graph can be measured in many ways, from simple metrics like the number of nodes and edges, to more complicated ones such as algebraic connectivity and treewidth. The goal of this project is to study which complexity metrics are relevant in modeling: What do measure, and how easy are they to compute? And does a metric actually tell us what we want to know?

Although no company is involved, it is possible to devote (part of) the project to a case study such as Facebook or the Dutch railway system.

Supervisor: Arend Rensink

Term Rewriting and Graph Rewriting are rule-based modelling formalisms, both with solid theoretical foundations and relatively mature tool support. Both can be used to specify system behaviour, in a similart way: the initial and subsequent system states are captured by structures that can be modified (rewritten) by rules. The main difference lies in the nature of those structures, which (as the names imply) are syntactical terms in one case, and graphs in the other.

In a strict sense, terms can be seen as (syntax) trees, which are themselves special cases of graphs; in that sense, graph rewriting is the more general and hence more powerful of the two. As usual, however, generality comes at a price, in this case involving the complexity of rule application: term rewriting is potentially more efficient than graph rewriting. However, how large the difference is for practical purposes is less evident.

In this project, the relation between term rewriting and graph rewriting is investigated on a practical level, namely by implementation a translation from specifications in Maude, a term rewriting tool, to specifications in GROOVE, a graph rewriting tool, and comparing the performance of the two tools on the basis of a set of case studies. The implementation should be based on a semantically sound transformation between the formalisms. Thus, the outcome of the project should be:

• A theoretical basis for the transformation of term rewrite rules to graph rewrite rules
• An implementation of this transformation from Maude format to GROOVE format
• A set of experiments on the basis of existing Maude models, showing the relative performance of the two

References

• Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude
• Maude tool page
• Modelling and analysis using GROOVE
• GROOVE tool page

Supervisor: Milan Lopuhaä-Zwakenberg

Many problems related to graphs are NP-hard: no algorithm that is fast on all graphs is known to exist, or even expected to exist. Nevertheless, such problems often have good heuristics: techniques that work well in most cases, even if their worst-case behaviour is still slow. In this project, you will develop and implement new heuristics for an existing NP-hard graph problem, such as:

• The Hamilton path and/or Hamilton cycle problem;
• The vertex cover problem;
• The graph cover problem.

Supervisor: Milan Lopuhaä-Zwakenberg

Many properties of graphs can be expressed in first-order logic; therefore, developing a model checker for first-order logic on graphs is extremely important for the flexible analysis of large graphs. While it is known that first-order checking on graphs is in general (PSPACE-)hard, recent work has shown that algorithms that work fast on typical graphs are theoretically possible, even if these algorithms will not be able to handle all cases in polynomial time. However, while these algorithms are described mathematically, no implementation has been attempted yet.

The aim of this master project is to develop precisely this implementation. It is very likely that the most straightforward implementation will work, but will leave a lot to be desired complexity-wise. Therefore, the student will have to develop methods to keep the performance feasible.