Gralog is a tool for editing and visualising graphs and other graphical structures such as transition systems, automata and (parity) games. Through its plugin interface it allows the extension of the project and the implementation of algorithms on graphical structures and it provides powerful tools for visualising these algorithms. Currently, various algorithms from logic, automata and game theory (parity games, cops and robber games) have been implemented.

It is written in Java and therefore should run on most operating systems and architectures.

Its principle developers are Sebastian Ordyniak and Stephan Kreutzer with plugins contributed by Lukas Moll. The project has been supported by the Deutsche Forschungsgemeinschaft (DFG) grant KR 2898/1-3.

The main purpose of Gralog is to assist research and education in logic, games and graph algorithms.

  • To assist in teaching, Gralog provides methods for visualising the results and runs of algorithms on graphical structures as well as methods for visualising the evaluation of logical formulae and the winner of graph based games such as parity games. See the description of the individual modules for more on the teaching aspect and visualisation.
  • In terms of research, the aim of Gralog is to provide a platform or framework in which algorithms related to logic, games or graphs can be implemented easily. Based on the powerful Java Collection Classes, the graph library used and a growing number of implemented features, implementing an algorithm in a Gralog plugin is sometimes almost as writing pseudo code. Good examples for this are the algorithms for determining the winner in a finite game or a parity game.

Release
A preliminary release of Gralog and its plugins can be found on sourcefore follwing this link.
However, we are currently implementing significant changes to all parts of Gralog. This includes changes to the plugin interface, providing documentation and example plugins designed to assist in developing own plugins. It is expected to release a completely new and greatly expanded version early September 2008.

Gralog consists of a core library and a range of plugins.

The Core Library

  • The core library provides a graphical user interface for displaying and editing graphs and other structures based on graphs such as labelled transition systems, automata or arenas for games and parity games.
  • In addition to its graph editor features, the core library provides an interface for plugin development. Plugins can provide additional types of structures but more commonly plugins provide algorithms and generators for already existing types of structures. The gralog interface aims to allow for plugin development with minimal initial learning overhead.
  • The core library uses the graph library JGraphT for its principle graph data structures and the JGraph library to display and layout graphs.

The Plugins. Gralog currently contains the following plugins.

  • Logic. The logic plugin provides methods for evaluating formulas of the modal mu-calculus on transition systems and for evaluating first-order logic formulas on undirected and directed graphs as well as on transition systems. The main feature is the that the evaluation of such formulas can be visualised so as to assist students in learning to work with the logics.
  • Finite Games. This module provides a linear time algorithm for determining the winner in simple games (reachability games).
  • Parity Games. This module provides parity games as data structure and implements the strategy improvement algorithm by Jurdzinksi and Vöge for determining the winner of a parity game.
    Again, the plugin provides intuitive means of visualising the way the algorithm performs.
  • DAG-width. This modules provides very basic algorithms to compute the number of cops needed in a cops and robber game on directed graphs and to compute an associated DAG-decomposition.