GAVS+ Tag Cloud
GAVS+ Tool

Game-based Solver

After the properties of the controller to synthesize have been specified in the model-driven tool, they are converted into a "game" scenario. This game is played between the two players controller and the environment.

The moves that are available to the controller correspond to the capabilities of the hardware modules in the plant (e.g., move the conveyor belt, process the work piece). Controller's task is to fulfill the specification from the formal model, that is, to find a sequence of moves starting from the initial configuration that leads to the goal configuration (a so-called strategy).

The moves that are available to the environment correspond to all the sensor inputs that are available in the plant. Whenever it takes turns, environment may choose one of the allowed sensor inputs (e.g., work piece color is red or black or silver). As such, environment represents the uncertainty in the plant.

The goal of the game-based solver that receives a formal representation of the game scenario is to find a strategy for controller in the presence of the uncertainty introduced by the environment. Or, to put it in another way, the goal is to find a strategy for every combination of environment moves. If such a strategy is found, we can guarantee that controller will win every game and hence we have successfully found a controller for the plant.