T-BEG

Overview: T-BEG: A Generic Tool for Games and the Construction of Distinguishing Formulas

Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. Our tool T-BEG is developed to work in the general setting of coalgebra and focuses on generic algorithms for computing the winning strategies of both players in a bisimulation game.

Therefore, T-BEG goes beyond labelled transition systems and allows to treat coalgebras in general (under the restrictions that we impose). That is, we exploit the categorical view to create generic algorithms.  As shown in Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas the coalgebraic game defined in (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras provides us with a generic algorithm to compute the winning strategies.

In our tool the user can either slip into the role of the spoiler $S$ or of the duplicator $D$, playing on some coalgebra $\alpha\colon X\to FX$ against the computer. The tool computes the winning strategy (if any) and follows this winning strategy if possible.  We have also implemented the construction of the distinguishing formula for two non-bisimilar states.

For more information we refer to Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas.

The development of this tool is part of the BEMEGA project (related publications).

System requirements

Getting started with T-BEG

T-BEG is a Windows tool offering a complete graphical interface, developed in Microsoft's Visual Studio using C#, especially Generics.

In order to run T-BEG, download it via the provided link and unzip the files. After that you need to run the tbeg.exe file in TBeg/bin/Release.

Compiling T-BEG

T-BEG is implemented in C# and can be compiled as 32-bit (64-bit)  (to our knowledge without any additional restrictions). It should be noted that new classes implementing the interface Functor.cs, have to be added to the file config_Functor, to enable the integration into T-BEG.

External Libaries and Projects

The vizualisation is handled via https://www.nuget.org/packages/Microsoft.Msagl.GraphViewerGDI under the MIT-License.

(For source code generation we use CodeDOM.)

Usage

We give here a brief overview of the three views within T-BEG:

First of all we want to note, that the current implementation offers four functors:

  • Labelled transition systems $P(A \times X)$ with $X$ finite state space.
  • Probabilistic systems $(DX + 1)^A$ with $X$ finite state space and $1$ represents termination
  • Update: Mealy machines and finite determinisitc automata

T-BEG views:

Input Transition System View:​

​
Here the user must first select a specific functor and then either specify each individual transition or load an already available system.
​​

Game View:

​
This is the ga​me view, where the user can select two states, choose a role and start the game.
​​
​

Add Functor View:

​Input Transition System View
In this mask, the user can implement his / her functor.
​​

We refer to the manual for more details.

 

Input and output

For loading and storing methods please use .ts to mark your files while implementing your functor. 

Tool material:

  • T-BEG
    Complete program folders including executable in /bin/Release
  • Demo (small introduction)
  • A webinterface  developed by Shiyam Sivam is in progress.

Developer

T-BEG is developed and maintained by Christina Mika-Michalski and Barbara König.

Disclaimer

T-BEG is currently in alpha stage. If you find any bugs or other unexpected behaviour, please send an e-mail.

Of course, the software is provided "as-is", without any implied or expressed waranty of any kind. So don't sue me if it doesn't work as expected.