|title:||Fair exploration in GROOVE|
|keywords:||Graph tranformation, fairness, GROOVE|
|topics:||Graphs , Logics and semantics|
GROOVE is a tool (written in Java), developed at the FMT group, centered around the use of simple graphs and their transformation for modelling system behviour, for instance of object-oriented software. Graph transformation is done through a set of transformation rules, each of which describes a specific change in a graph, together with a strategy that determines which of those rules can be applied at any given moment. This gives a variety of possible executions.
An important criterion in such a strategy is fairness: the property that if a rule can be applied somewhere, it will eventually be applied there. Fairness is important in many modeling situations, as it allows you to reason about basic things like: tasks sent out will eventually return as completed, or the time on the clock will eventually progress (to the next minute for example).
Currently, this type of fairness is not natively supported by GROOVE. The assignment is to provide a solution or workaround for this. To do this, you can proceed in one of two directions:
- Encode fairness using the existing strategies and features of GROOVE, or show that this cannot be done, This would be a rather theoretical topic.
- implement fairness as a strategy in GROOVE (or a new primitive with which this is possible). This would be a more practical topic.
By doing this project you will:
- learn about graph transformation in the context of GROOVE
- learn about fairness in the context of GROOVE
There are no prerequisites, but an affinity with graphs is a plus.