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.