Quantifying Masking Fault-Tolerance via Fair Stochastic Games

We introduce a formal notion of masking fault-tolerance between probabilistic transition systems using stochastic games. These games are inspired in bisimulation games, but they also take into account the possible faulty behavior of systems. When no faults are present, these games boil down to probabilistic bisimulation games. Since these games could be infinite, we propose a symbolic way of representing them so that they can be solved in polynomial time. In particular, we use this notion of masking to quantify the level of masking fault-tolerance exhibited by almost-sure failing systems, i.e., those systems that eventually fail with probability 1. The level of masking fault-tolerance of almost-sure failing systems can be calculated by solving a collection of functional equations. We produce this metric in a setting in which one of the player behaves in a strong fair way (mimicking the idea of fair environments).