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).
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.
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.)
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 two functors:
- Powerset functor $P(A \times X)$ with $X$ finite state space.
- Distribution functor $(DX + 1)^A$ with $X$ finite state space and $1$ represents termination
- (In future: Mealy machines and finite determinisitc automata)
Input Transition System View:
Add Functor View:
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.