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).
翻译:我们引入一种基于随机博弈的概率转移系统间屏蔽容错性的形式化概念。这些博弈受双模拟博弈启发,但同时考虑了系统可能出现的故障行为。当不存在故障时,这些博弈退化为概率双模拟博弈。由于这类博弈可能存在无限状态,我们提出一种符号化表示方法,使得能够在多项式时间内求解。特别地,我们利用这种屏蔽概念来量化几乎必然失效系统(即最终以概率1失效的系统)所展现的屏蔽容错水平。通过求解一组泛函方程,可计算出这类系统的屏蔽容错性度量。我们在其中一个参与者以强公平方式行动(模拟公平环境的概念)的设定下得到该度量指标。