Game-theoretic Simulation Checking Tool

Model checking is one of the most commonly used methods for checking program correctness. In this method, one verifies a program model given by the Kripke structure (labeled transition system) rather than the program itself. The specification is usually given as a temporal logic formula. In many subtasks of model checking, it is necessary to use relations that are defined on the set of program models and preserve the satisfiability of temporal logic formulas. There exist many relations of this kind, which are called simulation relations. In the present paper, we introduce a tool designed to check a wide class of simulation relations between finite models of programs. This tool is based on the simulation checking game-theoretic approach. The tool consists of two components. The first component is the formal language, which allows one to define various simulation relations in terms of an antagonistic two-player game. The second component is a software tool that, given two labeled transition systems and simulation definition, is able to check whether this simulation is satisfied between these labeled transition systems.