Reactive Bisimilarity Game Play

Two magicians move through a graph, trying to get each other stuck. They pass through edges where some spells are only possible in certain contexts.

Reactive Bisimilarity is a notion of equivalence for systems with timeout actions. Such systems can be used to model the event that a process may not be able to carry out certain tasks in certain environments, causing a timeout to occur. To determine whether two systems behave equivalently one can play logical games on their model representation as labeled transition system.