GEAR Modelchecker

Jump to: navigation, search
Error creating thumbnail: Unable to save thumbnail to destination

GEAR – Game-based Easy and Reverse Model Checking

GEAR is a game-based model checking tool that can be used to check finite systems. It has been primarily developed for usage as a Java ABC plugin although it supports stand-alone operation as well (via a command-line interface).

Natively, GEAR supports only the modal μ-calculus to express temporal logic properties for the systems in question. However, a powerful macro mechanism allows developers to specify temporal logic operators that can be translated into a modal μ-calculus equivalent which can then be used for actual model checking. The macro facilities also provide means to actually extend the expressiveness of the used language since macros can define their semantics directly (i.e. a subset of the model's nodes). The underlying concept is that of symbolic expressions.

The systems (also called models) used by GEAR are easily adaptable as well. A simple interface needs to be implemented to provide support for new models based on Kripke transition systems (also known as labelled Kripke structures, LKS) which constitute a generalization of both Kripke structures and labeled transition systems. These systems specify both labelled states and labelled transitions.

The key features of the plugin implementation are:

  • Easy maintenance of formulas and descriptions.
  • Reverse checking: find the sub-expressions satisfied at a given node.
  • Full integration with the formula builder plugin
  • Visualization of counter examples by error paths in the model.
  • Easy usage of the plugin by providing seperate views on the model checking process (namely an advanced and a basic view).
  • Readily available macro packages for the Computation Tree Logic (CTL)
  • Visualization and interaction of underlying game-based algorithm as SIB-Graph.

jETI integration

The integration of GEAR with the jETI tool server is currently realized via remote usage of the command line interface. There is a page detailing the necessary steps to get GEAR working on a jETI tool server. The first jETI implementation has been developed by Marc Njoku.


Documentation is available at the project's website where you can find a manual, GEAR's Java API specification and several Flash-based online tutorials explaining plugin usage. Please report any bugs or feature requests to our bug tracker. The discussion page and the GEAR mailing list can be used for discussion about features and aspects of the tool.

GEAR is developed and maintained by Marco Bakera.