11institutetext: Departamento de Computación, FCEFQyN, Universidad Nacional de
Río Cuarto, Argentina 22institutetext: FAMAF, Universidad Nacional de Córdoba
Argentina, 33institutetext: Consejo Nacional de Investigaciones Científicas y
Técnicas (CONICET), Argentina 44institutetext: Saarland University, Saarland
Informatics Campus, Germany

# A Stochastic Game Approach to Masking Fault-Tolerance: Bisimulation and
Quantification

Pablo F. Castro 1133 Pedro R. D’Argenio 223344
Luciano Putruele 1133 Ramiro Demasi 2233

###### Abstract

We introduce a formal notion of masking fault-tolerance between probabilistic
transition systems based on a variant of probabilistic bisimulation (named
masking simulation). We also provide the corresponding probabilistic game
characterization. Even though these games could be infinite, we propose a
symbolic way of representing them, such that it can be decided in polynomial
time if there is a masking simulation between two probabilistic transition
systems. 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 the
minimizing player behaves in a strong fair way (mimicking the idea of fair
environments), and limit our study to memoryless strategies due to the
infinite nature of the game. We implemented these ideas in a prototype tool,
and performed an experimental evaluation.

##  1 Introduction

Fault-tolerance is one important characteristic of modern software. This is
particularly true for critical software like banking software, automotive
applications, communication protocols, avionics software, etc. However, in
practice, it is hard to quantify the level of fault-tolerance provided by
computing systems. In most cases fault-tolerant systems are built using ad-hoc
techniques which are based on experience and, many times, lack a mathematical
foundation. Furthermore, faults usually have a probabilistic nature.
Therefore, concepts coming from probability theory become necessary when
developing fault-tolerant software. In this paper we provide a framework aimed
at analysing the fault-tolerance exhibited by concurrent probabilistic
systems. This encompasses the probability of occurrence of faults as well as
the use of randomized algorithms for improving the fault-tolerance of systems.

In practice, there are different types of fault-tolerance, _masking fault-
tolerance_ (when both the safety and liveness properties are preserved under
the occurrence of faults), _non-masking fault-tolerance_ (when only liveness
properties are preserved) and _failsafe fault-tolerance_ (when only safety
properties are preserved). Among them, masking fault-tolerance is often
acknowledged as the most desirable kind of fault-tolerance, because all the
properties of the nominal (i.e., non-faulty) system are preserved under faulty
behavior. However, in many settings, requiring full masking fault-tolerance is
unrealistic. In particular, for those systems that are not designed to
terminate and the degradation of hardware, or software, components will
eventually lead to a failure (i.e., a behavior that deviates from the expected
system’s behavior). One of the main applications of the framework described in
the forthcoming sections is the quantification of the amount of masking fault-
tolerance provided by systems before they enter into a failure. This measure
provides a tool for selecting a fault tolerance mechanism, or for balancing
multiple mechanisms (e.g., to which extent it is worth the cost of efficient
hardware redundancy against time demanding software artifacts).

During the last decade, significant progress has been made towards defining
suitable metrics or distances for diverse types of quantitative models
including real-time systems [18], probabilistic models [2, 3, 14, 15, 30], and
metrics for linear and branching systems [8, 13, 17, 26, 31]. Some authors
have already pointed out that these metrics can be useful to reason about the
robustness and correctness of a system, notions related to fault-tolerance. In
[6], we presented a notion of masking fault-tolerance between systems built on
a simulation relation and a corresponding game representation with
quantitative objectives. In this paper we review these ideas in a
probabilistic setting, and define a probabilistic version of this
characterization of masking fault-tolerance.

More specifically, we start characterizing probabilistic masking fault-
tolerance via a variant of probabilistic bisimulation. This _masking
simulation_ relates two probabilistic transition systems. The first one acts
as a specification of the intended behavior (i.e., nominal model) and the
second one as the fault-tolerant implementation (i.e., the extended model with
faulty behavior). The existence of a masking simulation implies that the
implementation masks the faults. This simulation relation can be captured as a
stochastic game played by a _Verifier_ and a _Refuter_. If the _Verifier_
wins, there is a probabilistic masking simulation. If instead the _Refuter_
wins, the implementation is not masking fault-tolerant. These games rely on
the notion of couplings between probabilistic distributions and, as a
consequence, the numbers of vertices of the game graphs is infinite. To tackle
this problem, we introduce a symbolic representation of these games where the
couplings are symbolically captured by means of equation systems. The size of
this symbolic graph is polynomial on the size of the input systems. Moreover,
the simulation games can be solved via their symbolic representation.

In practice masking fault-tolerance comes in a quantitative fashion, and thus
we enrich the games with quantitative objectives. This makes it possible to
quantify the amount of masking tolerance provided by the implementations. We
focus on games that almost-surely fail when the Refuter plays fairly (i.e.,
those systems that eventually fail with probability $1$). Due to the infinite
nature of the games, we restrict this result to randomized memoryless
strategies and show that the game is determined under these conditions. We
show that the problem of deciding if the game is almost surely failing under
fairness is polynomial. Moreover, the value of the game can be computed by
solving a collection of functional equations via a _Value Iteration_ algorithm
[9, 11, 12, 21]. We take such a value as the measure of fault-tolerance.

Summarizing our contribution,  (1) we define a notion of probabilistic masking
simulation,  (2) provide a game characterization for it, and  (3) show that it
can be decided in polynomial time (Sec. 3). Moreover, in Sec 4,  (4) we define
an extension of the game with rewards and provide a payoff function that
counts the number of “milestones” achieved by the implementation;  (5) we show
that the game is determined provided it is almost-surely failing under
fairness and memoryless strategies, and  (6) provide an algorithm to calculate
it. In addition,  (7) we provide a polynomial time algorithm to decide if a
game is almost-surely failing under fairness.  (8) We finally present an
experimental evaluation on some well-known case studies (Sec. 5).  Full
details and proofs can be found in the Appendix.

##  2 Preliminaries

We first introduce some basic definitions that will be necessary across the
paper.

A (discrete) _probability distribution_ $\mu$ over a denumerable set $S$ is a
function $\mu:S\rightarrow[0,1]$ such that $\mu(S)\triangleq\sum_{s\in
S}\mu(s)=1$. Let $\mathcal{D}(S)$ denote the set of all probability
distributions on $S$. $\Delta_{s}\in\mathcal{D}(S)$ denotes the Dirac
distribution for $s$, i.e., $\Delta_{s}(s)=1$ and $\Delta_{s}(s^{\prime})=0$
whenever $s^{\prime}\neq s$. The support set of $\mu$ is defined by
$\mathit{Supp}(\mu)=\\{s|~{}\mu(s)>0\\}$.

A _Probabilistic Transition System_ (PTS) is a structure $A=\langle
S,\Sigma,\rightarrow,s_{0}\rangle$ where  (i) $S$is a denumerable set of
_states_ containing the _initial state_ $s_{0}\in S$,  (ii) $\Sigma$is a set
of _actions_ , and  (iii) ${\rightarrow}\subseteq
S\times\Sigma\times\mathcal{D}(S)$is the _(probabilistic) transition
relation_.  We assume that there is always some transition leaving from every
state.

A distribution $w\in\mathcal{D}(S\times S^{\prime})$ is a coupling for
$(\mu,\mu^{\prime})$, with $\mu\in\mathcal{D}(S)$ and
$\mu^{\prime}\in\mathcal{D}(S^{\prime})$, if $w(S,\cdot)=\mu^{\prime}$ and
$w(\cdot,S^{\prime})=\mu$. $\mathbb{C}(\mu,\mu^{\prime})$ denotes the set of
all couplings for $(\mu,\mu^{\prime})$. It is worth noting that this defines a
polytope. $\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime}))$ denotes the set of all
vertices of the corresponding polytope. This set is finite if $S$ and
$S^{\prime}$ are finite. For $R\subseteq S\times S^{\prime}$, we say that a
coupling $w$ for $(\mu,\mu^{\prime})$ respects $R$ if
$\mathit{Supp}(w)\subseteq R$ (i.e., $w(s,s^{\prime})>0\Rightarrow
s~{}R~{}s^{\prime}$). We define
$R^{\\#}\subseteq\mathcal{D}(S)\times\mathcal{D}(S^{\prime})$ by
$\mu~{}R^{\\#}~{}\mu^{\prime}$ if and only if there is an $R$-respecting
coupling for $(\mu,\mu^{\prime})$.

A _stochastic game graph_ [10] is a tuple
$\mathcal{G}=(V,E,V_{1},V_{2},V_{\mathsf{P}},v_{0},\delta)$, where $V$ is a
set of vertices with $V_{1},V_{2},V_{\mathsf{P}}\subseteq V$ being a partition
of $V$, $v_{0}\in V$ is the initial vertice, $E\subseteq V\times V$, and
$\delta:V_{\mathsf{P}}\rightarrow\mathcal{D}(V)$ is a probabilistic transition
function such that, for all $v\in V_{\mathsf{P}}$ and $v^{\prime}\in V$:
$(v,v^{\prime})\in E$ iff $v^{\prime}\in\mathit{Supp}(\delta(v))$. If
$V_{\mathsf{P}}=\emptyset$, then $\mathcal{G}$ is called a $2$-player game
graph. Moreover, if $V_{1}=\emptyset$ or $V_{2}=\emptyset$, then $\mathcal{G}$
is a _Markov Decision Process_ (or MDP). Finally, in case that
$V_{1}=\emptyset$ and $V_{2}=\emptyset$, $\mathcal{G}$ is a _Markov chain_ (or
MC). For all states $v\in V$ we define $\mathit{Post}(v)=\\{v^{\prime}\in
V\mid(v,v^{\prime})\in E\\}$, the set of successors of $v$. Similarly,
$\mathit{Pre}(v^{\prime})=\\{v\in V\mid(v,v^{\prime})\in E\\}$ as the set of
predecessors of $v^{\prime}$. We assume that $\mathit{Post}(s)\neq\emptyset$
for every $v\in V_{1}\cup V_{2}$.

Given a game as defined above, a _play_ is an infinite sequence
$\omega=\omega_{0},\omega_{1},\dots$ such that $(\omega_{k},\omega_{k+1})\in
E$ for every $k\in\mathbb{N}$. The set of all plays is denoted by $\Omega$,
and the set of plays starting at vertex $v$ is written $\Omega_{v}$. A
_strategy_ (or policy) for Player $i\in\\{1,2\\}$ is a function
$\pi_{i}:V^{*}\cdot V_{i}\rightarrow\mathcal{D}(V)$ that assigns a
probabilistic distribution to each finite sequence of states such that
$\mathit{Supp}(\pi_{i}(w\cdot v))\subseteq\mathit{Post}(v)$ for all $w\in
V^{*}$ and $v\in V_{i}$. The set of all the strategies for Player $i$ is named
$\Pi_{i}$. A strategy $\pi_{i}$ is said to be _pure_ if, for every $w\in
V^{*}$ and $v\in V_{i}$, $\pi_{i}(w\cdot v)$ is a Dirac distribution, and it
is called _memoryless_ if $\pi_{i}(w\cdot v)=\pi_{i}(v)$, for every $w\in
V^{*}$ and $v\in V_{i}$. Given two strategies $\pi_{1}\in\Pi_{1}$,
$\pi_{2}\in\Pi_{2}$ and a starting state $v$, the _result_ of the game is a
Markov chain, denoted by $\mathcal{G}^{\pi_{1},\pi_{2}}_{v}$. As any Markov
chain, $\mathcal{G}^{\pi_{1},\pi_{2}}_{v}$ defines a probability measure
$\mathit{Prob}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}$. An event $\mathcal{A}$ is a
measurable set in the Borel $\sigma$-algebra generated by the cones of
$\Omega$. Thus, $\mathit{Prob}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}(\mathcal{A})$
is the probability that strategies $\pi_{1}$ and $\pi_{2}$ generate a play
belonging to $\mathcal{A}$ from state $v$. It would normally be convenient to
use LTL notation to define events. For instance, $\Diamond
V^{\prime}=\\{\omega=\omega_{0},\omega_{1},\dots\in\Omega\mid\exists
i:\omega_{i}\in V^{\prime}\\}$ defines the event in which some state in
$V^{\prime}$ is reached. The outcome of the game, denoted by
$\mathit{out}_{v}(\pi_{1},\pi_{2})$ is the set of possible paths of
$\mathcal{G}^{\pi_{1},\pi_{2}}_{v}$ starting at vertex $v$ (i.e., the possible
plays when strategies $\pi_{1}$ and $\pi_{2}$ are used). When the initial
state $v$ is fixed, we write $\mathit{out}(\pi_{1},\pi_{2})$ instead of
$\mathit{out}_{v}(\pi_{1},\pi_{2})$.

A _Boolean objective_ for $\mathcal{G}$ is a set $\Phi\subseteq\Omega$, we say
that a play $\omega$ is _winning_ for Player $1$ at vertex $v$ if
$\omega\in\Phi$, otherwise we say that it is winning for Player $2$ (i.e., we
consider _zero-sum_ games). A strategy $\pi_{1}$ is a _sure winning strategy_
for Player $1$ from vertex $v$ if, for every strategy $\pi_{2}$ for Player
$2$, $\mathit{out}_{v}(\pi_{1},\pi_{2})\subseteq\Phi$. $\pi_{1}$ is said to be
_almost-sure winning_ if for every strategy $\pi_{2}$ for Player $2$, we have
$\mathit{Prob}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}(\Phi)=1$. Sure and almost-
sure winning strategies for Player $2$ are defined in a similarly.
Reachability games are games with Boolean objectives of the style: $\Diamond
V^{\prime}$, for some set $V^{\prime}\subseteq V$. A standard result is that,
if a reachability game has a sure winning strategy, then it has a pure
memoryless sure winning strategy [10].

A _quantitative objective_ is a measurable function
$f:\Omega\rightarrow\mathbb{R}$. Given a measurable function we define
$\mathbb{E}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}[f]$ as the expectation of
function $f$ under probability
$\mathit{Prob}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}$. The goal of Player $1$ is
to maximize the value $f$ of the play, whereas the goal of Player $2$ is to
minimize it. Sometimes quantitative objective functions can be defined via
_rewards_. These are assigned by a _reward function_
$r:V\rightarrow\mathbb{R}$. A _stochastic game with rewards_ is a structure
$(V,E,V_{1},V_{2},V_{\mathsf{P}},\delta,r)$ composed of a stochastic game and
a reward function. The value of the game for Player $1$ under strategy
$\pi_{1}$ at vertex $v$, denoted $\mathop{\textup{val}}_{1}(\pi_{1})(v)$, is
defined as the infimum over all the values resulting from Player $2$
strategies when the game starts at $v$, i.e.,
$\mathop{\textup{val}}_{1}(\pi_{1})(v)=\inf_{\pi_{2}\in\Pi_{2}}\mathbb{E}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}[f]$.
The _value of the game_ for Player $1$ from vertex $v$ is defined as the
supremum of the values of all Player $1$ strategies, i.e.,
$\sup_{\pi_{1}\in\Pi_{1}}\mathop{\textup{val}}_{1}(\pi_{1})(v)$. Analogously,
the value of the game for a Player $2$ strategy $\pi_{2}$ and the value of the
game for Player $2$ are defined as
$\mathop{\textup{val}}_{2}(\pi_{2})(v)=\sup_{\pi_{1}\in\Pi_{1}}\mathbb{E}^{\pi_{1},\pi_{2}}_{\mathcal{G},v}[f]$
and $\inf_{\pi_{2}\in\Pi_{2}}\mathop{\textup{val}}_{2}(\pi_{2})(v)$,
respectively. We say that a game is determined if both values are equal, that
is,
$\sup_{\pi_{1}\in\Pi_{1}}\mathop{\textup{val}}_{1}(\pi_{1})(v)=\inf_{\pi_{2}\in\Pi_{2}}\mathop{\textup{val}}_{2}(\pi_{2})(v)$,
for every vertex $v$.

##  3 Probabilistic Masking Simulation

In this section we introduce probabilistic masking simulation which is a
probabilistic extension of the masking simulation relation introduced in [6].
We also give a symbolic version of the stochastic game characterization of the
relation, and provide an algorithm to solve it.

###  3.1 The relation.

Roughly speaking, a probabilistic masking simulation is a relation between
PTSs that extends probabilistic bisimulation [19] in order to account for
fault masking. Intuitively, one of the PTSs acts as the nominal model (i.e.,
the specification), while the other one models the implementation of the
system under faults. The nominal model describes the ideal behavior of the
system (i.e., when no faults are considered), while the implementation
describes a fault-tolerant version of the system, where the occurrence of
faults are taken into account and a fault tolerance mechanism is expected to
act upon them. Probabilistic masking simulation allows one to analyze whether
the implementation is able to mask the faults while preserving the behavior of
the nominal model. More specifically, for non-faulty transitions, the relation
behaves as probabilistic bisimulation, which is captured by means of couplings
and relations respecting these couplings (as done for instance in [19]). The
novel part is given by the occurrence of faults: if the implementation
performs a fault, the nominal model matches it by doing nothing.

For a set of actions $\Sigma$, and a (finite) set of _fault labels_
$\mathcal{F}$, with $\mathcal{F}\cap\Sigma=\emptyset$, we define
$\Sigma_{\mathcal{F}}=\Sigma\cup\mathcal{F}$. Intuitively, the elements of
$\mathcal{F}$ indicate the occurrence of a fault in a faulty implementation.
Furthermore, when useful we consider the set $\Sigma^{i}=\\{e^{i}\mid
e\in\Sigma\\}$, containing the elements of $\Sigma$ indexed with superscript
$i$.

###### Definition 1

Let $A=(S,\Sigma,{\rightarrow},s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},{\rightarrow^{\prime}},s_{0}^{\prime})$
be two PTSs representing the nominal and the implementation model,
respectively. $A^{\prime}$ is _strong probabilistic masking fault-tolerant_
with respect to $A$ if there exists a relation $\mathbin{\mathbf{M}}\subseteq
S\times S^{\prime}$ such that:  (a) $s_{0}\mathbin{\mathbf{M}}s^{\prime}_{0}$,
and  (b) for all $s\in S,s^{\prime}\in S^{\prime}$ with
$s\mathbin{\mathbf{M}}s^{\prime}$ and all $e\in\Sigma$ and $F\in\mathcal{F}$
the following holds:

  1. (1)

if $s\xrightarrow{e}\mu$, then $s^{\prime}\xrightarrow{e}\mu^{\prime}$ and
$\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$ for some $\mu^{\prime}$;

  2. (2)

if $s^{\prime}\xrightarrow{e}\mu^{\prime}$, then $s\xrightarrow{e}\mu$ and
$\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$ for some $\mu$;

  3. (3)

if $s^{\prime}\xrightarrow{F}\mu^{\prime}$, then
$\Delta_{s}\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$.

If such relation exists we say that $A^{\prime}$ is a _strong probabilistic
masking fault-tolerant implementation_ of $A$, denoted
$A\preceq_{m}A^{\prime}$.

###### Example 1

Consider a memory cell storing one bit of information that periodically
refreshes its value. The memory supports writing and reading operations,
whereas a refresh performs a read operation and overwrites the value with
itself. Obviously, in this system, the result of a reading depends on the
value stored in the cell. Thus, a property associated with the system is that
the value read from the cell coincides with that of the last performed
writing. This is captured by the nominal model given at the left of Figure 1
in PRISM notation [24]. Actions $\texttt{r}i$ and $\texttt{w}i$ (for $i=0,1$)
represent the actions of reading or writing value $i$. The bit stored in the
memory is saved in variable b. A tick action indicates the passing of one time
unit and in doing so, with probability p, it enables the refresh action
(rfsh). Variable m indicates whether the system is in write/read mode, or
producing a refresh.

module NOMINAL
---
| b : [0..1] init 0;
| m : [0..1] init 0; |  | // 0 = normal,
|  |  | // 1 = refreshing
| [w0] | (m=0) |  | -> | (b’= 0);
| [w1] | (m=0) |  | -> | (b’= 1);
| [r0] | (m=0) & (b=0) |  | -> | true;
| [r1] | (m=0) & (b=1) |  | -> | true;
| [tick] | (m=0) |  | -> | p : (m’= 1) +
|  |  |  |  | (1-p) : true;
| [rfsh] | (m=1) |  | -> | (m’= 0);
endmodule

module FAULTY
---
| v : [0..3] init 0;
| s : [0..2] init 0; |  | // 0 = normal, 1 = faulty,
|  |  | // 2 = refreshing
|  f : [0..1] init 0; |  | // fault limiting artifact
| [w0] | (s!=2) |  | -> | (v’= 0) & (s’= 0);
| [w1] | (s!=2) |  | -> | (v’= 3) & (s’= 0);
| [r0] | (s!=2) & (v<=1) |  | -> | true;
| [r1] | (s!=2) & (v>=2) |  | -> | true;
| [tick] | (s!=2) |  | -> | p : (s’= 2) + q : (s’= 1)
|  |  |  |  | \+ (1-p-q) : true;
| [rfsh] | (s=2) |  | -> | (s’=0)
|  |  |  |  | & (v’= (v<=1) ? 0 : 3);
| [fault] |  (s=1) & (f<1) |  | -> | (v’= (v<3) ? (v+1) : 2)
|  |  |  |  |  & (s’= 0) & (f’= f+1);
| [fault] |  (s=1) & (f<1) |  | -> | (v’= (v>0) ? (v-1) : 1)
|  |  |  |  |  & (s’= 0) & (f’= f+1);
endmodule

Figure 1: Nominal and fault-tolerant models for the memory cell.

A potential fault in this scenario occurs when a cell unexpectedly changes its
value (e.g., as a consequence of some electromagnetic interference). In
practice, the occurrence of such an error has a certain probability. A typical
technique to deal with this situation is _redundancy_ ; for instance, using
three memory bits instead of one. Then, writing operations are performed
simultaneously on the three bits while reading returns the value read by
majority (i.e., by _voting_). The right hand-side model of Figure 1 represents
this implementation with the occurrence of the fault implicitly modeled
(ignore, by the time being the red part). Variable v counts the votes for the
value 1\. Thus writing 1 (w1) sets v in 3, and writing 0 (w0) sets it in 0.
The read actions would return 1 (r1) if $\texttt{v}\geq 2$ and 0 (r0)
otherwise. In addition to enabling the refresh action, a tick may also enable
the occurrence of a fault with probability q, with the restriction that
$\texttt{p}+\texttt{q}\leq 1$. Variable s indicates that the system is in
normal mode ($\texttt{s}=0$), in a state where a fault may occur
($\texttt{s}=1$), or producing a refresh ($\texttt{s}=2$). Notice that reading
and writing are allowed as long as the system is not producing a refresh. The
red coloured text of the figure is an artifact to limit the number of faults
to 1. Under this condition, it is easy to check that the relation
$\mathbin{\mathbf{M}}=\\{{\langle(b,m),(v,s,f)\rangle}\mid{{2b\leq v\leq
2b{+}1}\wedge(m=1\Leftrightarrow s=2)}\\}$ is a probabilistic masking
simulation (where $b$, $m$, $v$, $s$, and $f$ represent the values of
variables b, m, v, s, and f, respectively.)

It should be evident that if the red coloured text is not present then FAULTY
is not a probabilistic masking fault-tolerant implementation of NOMINAL.

###  3.2 A characterization in terms of a stochastic game.

In the following, we define a stochastic masking simulation game for the
nominal model $A=(S,\Sigma,{\rightarrow},s_{0})$ and the implementation model
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},{\rightarrow^{\prime}},s^{\prime}_{0})$.
The game is similar to a bisimulation game [29], and it is played by two
players, named by convenience the Refuter ($\mathsf{R}$) and the Verifier
($\mathsf{V}$). The Verifier wants to prove that $s\in S$ and $s^{\prime}\in
S^{\prime}$ are probabilistic masking similar, and the Refuter intends to
disprove that. The game starts from the pair of states $(s,s^{\prime})$ and
the following steps are repeated:

  1. 1)

$\mathsf{R}$ chooses either a transition $s\xrightarrow{a}\mu$ from the
nominal model or a transition $s^{\prime}\xrightarrow{a}\mu^{\prime}$ from the
implementation;

  2. 2.a)

If $a\notin\mathcal{F}$, $\mathsf{V}$ chooses a transition matching action $a$
from the opposite model, i.e., a transition
$s^{\prime}\xrightarrow{a}\mu^{\prime}$ if $\mathsf{R}$’s choice was from the
nominal, or a transition $s\xrightarrow{a}\mu$ otherwise. In addition,
$\mathsf{V}$ chooses a coupling $w$ for $(\mu,\mu^{\prime})$;

  3. 2.b)

If $a\in\mathcal{F}$, $\mathsf{V}$ can only selects the Dirac distribution
$\Delta_{s}$ and the only possible coupling $w$ for
$(\Delta_{s},\mu^{\prime})$;

  4. 3)

The successor pair of states $(t,t^{\prime})$ is chosen probabilistically
according to $w$.

If the play continues forever, then the Verifier wins; otherwise, the Refuter
wins. Step 2.b is the only one that differs from the usual bisimulation game.
It is necessary for the asymmetry produced by transitions that represent the
occurrence of faults: if the Refuter chooses to play a fault in the
implementation, then it needs to be masked, and therefore the Verifier cannot
produce any move in the nominal model. Thus, the probabilistic step of the
fault can only be matched by a Dirac distribution on the same state of the
nominal model.

In the following we define the stochastic making game graph that allows us to
formalize this game.

###### Definition 2

Let $A=(S,\Sigma,{\rightarrow},s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},{\rightarrow^{\prime}},s^{\prime}_{0})$
be two PTSs. The 2-players _stochastic masking game graph_
$\mathcal{G}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$,
is defined as follows:

$\displaystyle V^{\mathcal{G}}=\ $ $\displaystyle
V^{\mathcal{G}}_{\mathsf{R}}\cup V^{\mathcal{G}}_{\mathsf{V}}\cup
V^{\mathcal{G}}_{\mathsf{P}},\text{where: }$ $\displaystyle
V^{\mathcal{G}}_{\mathsf{R}}=\ $ $\displaystyle\\{(s,\mathchar
45\relax,s^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R})\mid s\in S\wedge s^{\prime}\in
S^{\prime}\\}\cup\\{v_{\text{err}}\\}$ $\displaystyle
V^{\mathcal{G}}_{\mathsf{V}}=\ $
$\displaystyle\\{(s,\sigma^{1},s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V})\mid s\in S\wedge s^{\prime}\in
S^{\prime}\wedge\sigma\in\Sigma\wedge(s,\sigma,\mu)\in{\rightarrow}\\}\cup{}$
$\displaystyle\\{(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathchar 45\relax,\mathsf{V})\mid s\in S\wedge
s^{\prime}\in
S^{\prime}\wedge\sigma\in\Sigma_{\mathcal{F}}\wedge(s^{\prime},\sigma,\mu^{\prime})\in{\rightarrow^{\prime}}\\}$
$\displaystyle V^{\mathcal{G}}_{\mathsf{P}}=\ $ $\displaystyle\\{(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\mid s\in S\wedge
s^{\prime}\in
S^{\prime}\wedge\mu\in\mathcal{D}(S)\wedge\mu^{\prime}\in\mathcal{D}(S^{\prime})\wedge
w\in\mathbb{C}(\mu,\mu^{\prime})\\}$ $\displaystyle v_{0}^{\mathcal{G}}=\ $
$\displaystyle(s_{0},\mathchar 45\relax,s^{\prime}_{0},\mathchar
45\relax,\mathchar 45\relax,\mathchar 45\relax,\mathsf{R})\text{ \ (the
Refuter starts playing)}$
$\displaystyle\delta^{\mathcal{G}}:V^{\mathcal{G}}_{\mathsf{P}}\rightarrow\mathcal{D}(V^{\mathcal{G}}_{\mathsf{R}}),\text{
defined by }\delta^{\mathcal{G}}((s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}))((t,\mathchar
45\relax,t^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R}))=w(t,t^{\prime})\text{,}$

and $E^{\mathcal{G}}$ is the minimal set satisfying the following rules:

$\displaystyle s\xrightarrow{\sigma}\mu$
$\displaystyle\Rightarrow{\langle{(s,\mathchar 45\relax,s^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R}),(s,\sigma^{1},s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V})}\rangle}\in E^{\mathcal{G}}$ (11) $\displaystyle
s^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}\mu^{\prime}$
$\displaystyle\Rightarrow{\langle{(s,\mathchar 45\relax,s^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R}),(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathchar 45\relax,\mathsf{V})}\rangle}\in
E^{\mathcal{G}}$ (12)
$\displaystyle{s^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}\mu^{\prime}}\wedge{w\in\mathbb{C}(\mu,\mu^{\prime})}$
$\displaystyle\Rightarrow{\langle{(s,\sigma^{1},s^{\prime},\mu,\mathchar
45\relax,\mathchar 45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})}\rangle}\in
E^{\mathcal{G}}$ (2.a1)
$\displaystyle{\sigma\notin\mathcal{F}}\wedge{s\xrightarrow{\sigma}\mu}\wedge{w\in\mathbb{C}(\mu,\mu^{\prime})}$
$\displaystyle\Rightarrow{\langle{(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathchar 45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})}\rangle}\in
E^{\mathcal{G}}$ (2.a2)
$\displaystyle{F\in\mathcal{F}}\wedge{w\in\mathbb{C}(\Delta_{s},\mu^{\prime})}$
$\displaystyle\Rightarrow{\langle{(s,F^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathchar 45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\Delta_{s},\mu^{\prime},w,\mathsf{P})}\rangle}\in
E^{\mathcal{G}}$ (2.b) $\displaystyle(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in
V^{\mathcal{G}}_{\mathsf{P}}\wedge$
$\displaystyle(t,t^{\prime})\in\mathit{Supp}(w)$
$\displaystyle\Rightarrow{\langle{(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}),(t,\mathchar
45\relax,t^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R})}\rangle}\in E^{\mathcal{G}}$ (3)
$\displaystyle{v\in(V^{\mathcal{G}}_{\mathsf{V}}{\cup}\\{v_{\text{err}}\\})}\wedge({\nexists
v^{\prime}}$ $\displaystyle{}\neq
v_{\text{err}}:{{\langle{v,v^{\prime}}\rangle}\in
E^{\mathcal{G}}})\Rightarrow{\langle{v,v_{\text{err}}}\rangle}\in
E^{\mathcal{G}}$ (err)

The definition follows the idea of the game previously described. A round of
the game starts in the Refuter’s state $v_{0}^{\mathcal{G}}$. Notice that, at
this point, only the current states of the nominal and implementation models
are relevant (all other information is not yet defined in this round and hence
marked with “$\mathchar 45\relax$”). Step 1 of the game is encoded in rules
(11) and (12), where the Refuter chooses a transition, thus defining the
action and distribution that need to be matched, and moving to a Verifier’s
state. Thus, a Verifier’s state in $V^{\mathcal{G}}_{\mathsf{V}}$ is a tuple
that has also defined which action and distribution need to be matched and
which model the Refuter has moved. Step 2.a of the game is given by rules
(2.a1) and (2.a2) in which the Verifier chooses a matching move from the
opposite model (hence defining the other distribution) and an appropriate
coupling, and moving to a probabilistic state. Step 2.b of the game is encoded
in rule (2.b). Here the Verifier has no choice since it is obliged to choose
the Dirac distribution $\Delta_{s}$ and the only available coupling in
$\mathbb{C}(\Delta_{s},\mu^{\prime})$. A probabilistic state in
$V^{\mathcal{G}}_{\mathsf{P}}$ has everything defined to probabilistically
resolve the next step through function $\delta^{\mathcal{G}}$ (rule (3)).
Finally, if a player has no move, then it can only move to the error state
$v_{\text{err}}$ (rule (err)). This can only happen in a Verifier’s state or
in $v_{\text{err}}$.

The notion of probabilistic masking simulation can be captured by the
corresponding stochastic masking game with the appropriate Boolean objective.

###### Theorem 3.1

Let $A=(S,\Sigma,{\rightarrow},s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},{\rightarrow^{\prime}},s_{0}^{\prime})$
be two PTSs. We have $A\preceq_{m}A^{\prime}$ iff the Verifier has a sure
winning strategy for the stochastic masking game graph
$\mathcal{G}_{A,A^{\prime}}$ with the Boolean objective $\neg\Diamond
v_{\text{err}}$.

Notice that the graph for a stochastic masking game could be infinite. Indeed,
each probabilistic node of the graph includes a coupling between the two
contending distributions, and there can be uncountably many of them. It
nonetheless induces an algorithm as follows. We define regions $W^{i}$ of the
graph vertices. Intuitively, each $W^{i}$ represents a collection of vertices
from which the Refuter has a strategy (in the infinite game) with probability
greater than $0$ of reaching the error state in at most $i$ steps (these sets
can be thought of as a probabilistic version of _attractors_ [20]).

###### Definition 3

Let
$\mathcal{G}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$
be a stochastic masking game graph for PTSs $A$ and $A^{\prime}$. We define
sets $W^{i}$ (for $i\geq 0$) as follows:

$\displaystyle W^{0}={}$ $\displaystyle\\{v_{\text{err}}\\},$ $\displaystyle
W^{i+1}={}$ $\displaystyle\textstyle\\{v^{\prime}\mid v^{\prime}\in
V^{\mathcal{G}}_{\mathsf{R}}\wedge\mathit{Post}(v^{\prime})\cap
W^{i}\neq\emptyset\\}\cup{}$
$\displaystyle\textstyle\\{v^{\prime}\mid{v^{\prime}\in
V^{\mathcal{G}}_{\mathsf{V}}}\wedge{\mathbb{V}(\mathit{Post}(v^{\prime}))\subseteq\bigcup_{j\leq
i}W^{j}}\wedge{\mathbb{V}(\mathit{Post}(v^{\prime}))\cap
W^{i}\neq\emptyset}\\}\cup{}$ $\displaystyle\textstyle\\{v^{\prime}\mid
v^{\prime}\in
V^{\mathcal{G}}_{\mathsf{P}}\wedge\sum_{v^{\prime\prime}\in\mathit{Post}(v^{\prime})\cap
W^{i}}\delta^{\mathcal{G}}(v^{\prime})(v^{\prime\prime})>0\\}$

where $\mathbb{V}(V^{\prime})=\\{(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in V^{\prime}\cap
V^{\mathcal{G}}_{\mathsf{P}}\mid
w\in\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime}))\\}$. Finally, let
$W=\bigcup_{i\geq 0}W^{i}$.

The sets $W^{i}$ can be used to solve the game $\mathcal{G}_{A,A^{\prime}}$.
Notice, in particular, that we do not take into account all possible couplings
but only those that are vertices of the polytope
$\mathbb{C}({v}[{3}],{v}[{4}])$. (${(x_{0},\dots,x_{n})}[{i}]$ is the
$(i+1)$-th projection, i.e., $x_{i}$.) This is sufficient to determine the
winner of the game since every coupling in $\mathbb{C}({v}[{3}],{v}[{4}])$ can
be expressed as a convex combination of its vertices. Thus, if there is a
positive probability of reaching the error state with some coupling, there is
also a positive probability of reaching it through a vertex coupling. By
taking only the vertex couplings, only a finite number of graph vertices are
collected in each $W_{i}$ and hence $W$ can be effectively computed with a fix
point algorithm.

The following result is a straightforward adaptation of the results for
reachability games over finite graphs [10].

###### Theorem 3.2

Let
$\mathcal{G}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$
be a stochastic masking game graph for PTSs $A$ and $A^{\prime}$. Then, the
Verifier has a sure winning strategy from vertex $v$ iff $v\notin W$.

It is worth noting that, for a probabilistic vertex $(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in
V^{\mathcal{G}}_{\mathsf{P}}$, the two-way transportation polytope
$\mathbb{C}(\mu,\mu^{\prime})$ has at least
$\frac{\max\\{m,n\\}!}{(\max\\{m,n\\}-\min\\{m,n\\}+1)!}$ vertices (and at
most $m^{n-1}n^{m-1}$ vertices) [22], where $m=\mathit{Supp}(\mu)$ and
$n=\mathit{Supp}(\mu^{\prime})$. Therefore, it could be computationally
impractical to calculate such sets.

###  3.3 A Symbolic Game Graph.

In this section, we introduce a finite representation of stochastic masking
games through a symbolic representation which enables a more efficient
algorithm. We define the symbolic graph for a stochastic masking game in two
parts. The first part captures the non-stochastic behaviour of the game by
removing the stochastic choice ($\delta^{\mathcal{G}}$) of the game graph, as
well as the couplings on the vertices. The second part appends an equation
system to each probabilistic vertex whose solution space is the polytope
defined by the set of all couplings for the contending distributions.

###### Definition 4

Let $A=(S,\Sigma,{\rightarrow},s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},{\rightarrow^{\prime}},s^{\prime}_{0})$
be two PTSs. The _symbolic game graph_ for the stochastic masking game
$\mathcal{G}_{A,A^{\prime}}$ is defined by the structure
$\mathcal{SG}_{A,A^{\prime}}=(V^{\mathcal{SG}},E^{\mathcal{SG}},V^{\mathcal{SG}}_{\mathsf{R}},V^{\mathcal{SG}}_{\mathsf{V}},V^{\mathcal{SG}}_{\mathsf{P}},v_{0}^{\mathcal{SG}})$,
where:

$\displaystyle V^{\mathcal{SG}}=\ $ $\displaystyle
V^{\mathcal{SG}}_{\mathsf{R}}\cup V^{\mathcal{SG}}_{\mathsf{V}}\cup
V^{\mathcal{SG}}_{\mathsf{P}},\text{ where: }$ $\displaystyle
V^{\mathcal{SG}}_{\mathsf{R}}=\ $ $\displaystyle\\{(s,\mathchar
45\relax,s^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathsf{R})\mid s\in
S\wedge s^{\prime}\in S^{\prime}\\}\cup\\{v_{\text{err}}\\}$ $\displaystyle
V^{\mathcal{SG}}_{\mathsf{V}}=\ $
$\displaystyle\\{(s,\sigma,s^{\prime},\mu,\mathchar 45\relax,\mathsf{V})\mid
s\in S\wedge s^{\prime}\in
S^{\prime}\wedge\sigma\in\Sigma^{1}\wedge(s,\sigma,\mu)\in{\rightarrow}\\}\cup{}$
$\displaystyle\\{(s,\sigma,s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathsf{V})\mid s\in S\wedge s^{\prime}\in
S^{\prime}\wedge\sigma\in\Sigma_{\mathcal{F}}^{2}\wedge(s^{\prime},\sigma,\mu^{\prime})\in{\rightarrow}\\}$
$\displaystyle V^{\mathcal{SG}}_{\mathsf{P}}=\ $ $\displaystyle\\{(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})\mid s\in S\wedge
s^{\prime}\in
S^{\prime}\wedge\mu\in\mathcal{D}(S)\wedge\mu^{\prime}\in\mathcal{D}(S^{\prime})\\}$
$\displaystyle v_{0}^{\mathcal{SG}}=\ $ $\displaystyle(s_{0},\mathchar
45\relax,s^{\prime}_{0},\mathchar 45\relax,\mathchar 45\relax,\mathsf{R}),$

and $E^{\mathcal{SG}}$ is the minimal set satisfying the following rules:

$\displaystyle s\xrightarrow{\sigma}\mu$
$\displaystyle\Rightarrow{\langle{(s,\mathchar 45\relax,s^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathsf{R}),(s,\sigma^{1},s^{\prime},\mu,\mathchar
45\relax,\mathsf{V})}\rangle}\in E^{\mathcal{SG}}$ $\displaystyle
s^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}\mu^{\prime}$
$\displaystyle\Rightarrow{\langle{(s,\mathchar 45\relax,s^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathsf{R}),(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathsf{V})}\rangle}\in E^{\mathcal{SG}}$
$\displaystyle{s^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}\mu^{\prime}}$
$\displaystyle\Rightarrow{\langle{(s,\sigma^{1},s^{\prime},\mu,\mathchar
45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})}\rangle}\in E^{\mathcal{SG}}$
$\displaystyle{\sigma\notin\mathcal{F}}\wedge{s\xrightarrow{\sigma}\mu}$
$\displaystyle\Rightarrow{\langle{(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})}\rangle}\in E^{\mathcal{SG}}$
$\displaystyle{F\in\mathcal{F}}$
$\displaystyle\Rightarrow{\langle{(s,F^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\Delta_{s},\mu^{\prime},\mathsf{P})}\rangle}\in
E^{\mathcal{SG}}$ $\displaystyle(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})\in
V^{\mathcal{SG}}_{\mathsf{P}}\wedge$
$\displaystyle((t,t^{\prime})\in\mathit{Supp}(\mu)\times\mathit{Supp}(\mu^{\prime}))$
$\displaystyle\Rightarrow{\langle{(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P}),(t,\mathchar
45\relax,t^{\prime},\mathchar 45\relax,\mathchar
45\relax,\mathsf{R})}\rangle}\in E^{\mathcal{SG}}$
$\displaystyle{v\in(V^{\mathcal{SG}}_{\mathsf{V}}{\cup}\\{v_{\text{err}}\\})}$
$\displaystyle{}\wedge{(\nexists{v^{\prime}\neq
v_{\text{err}}}:{{\langle{v,v^{\prime}}\rangle}\in
E^{\mathcal{SG}}})}\Rightarrow{\langle{v,v_{\text{err}}}\rangle}\in
E^{\mathcal{SG}}$

In addition, for each $v=(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})\in
V^{\mathcal{SG}}_{\mathsf{P}}$, define the set of variables
$X(v)=\\{x_{s_{i},s_{j}}\mid s_{i}\in\text{Supp}(\mu)\wedge
s_{j}\in\text{Supp}(\mu^{\prime})\\}$, and the system of equations

$\displaystyle\mathit{Eq}(v)={}$
$\displaystyle\textstyle\big{\\{}\sum_{s_{j}\in\mathit{Supp}(\mu^{\prime})}x_{s_{k},s_{j}}=\mu(s_{k})\mid
s_{k}\in\mathit{Supp}(\mu)\big{\\}}\cup{}$
$\displaystyle\textstyle\big{\\{}\sum_{s_{k}\in\mathit{Supp}(\mu)}x_{s_{k},s_{j}}=\mu^{\prime}(s_{j})\mid
s_{j}\in\mathit{Supp}(\mu^{\prime})\big{\\}}\cup{}$
$\displaystyle\textstyle\big{\\{}x_{s_{k},s_{j}}\geq 0\mid
s_{k}\in\mathit{Supp}(\mu)\wedge s_{j}\in\mathit{Supp}(\mu^{\prime})\big{\\}}$

Notice that $\\{\bar{x}_{s_{k},s_{j}}\\}_{s_{k},s_{j}}$ is a solution of
$\mathit{Eq}(v)$ if and only if there is a coupling
$w\in\mathbb{C}(\mu,\mu^{\prime})$ such that
$w(s_{k},s_{j})=\bar{x}_{s_{k},s_{j}}$ for all $s_{k}\in\mathit{Supp}(\mu)$
and $s_{j}\in\mathit{Supp}(\mu^{\prime})$.

In addition, given a set of game vertices $V^{\prime}\subseteq
V^{\mathcal{SG}}_{\mathsf{R}}$, we define $\mathit{Eq}(v,V^{\prime})$ by
extending $\mathit{Eq}(v)$ with an equation limiting the couplings in such a
way that vertices in $V^{\prime}$ are _not_ reached. Formally,
$\mathit{Eq}(v,V^{\prime})=\mathit{Eq}(v)\cup\big{\\{}\sum_{(s,\mathchar
45\relax,s^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathsf{R})\in
V^{\prime}}x_{s,s^{\prime}}=0\big{\\}}$. By properly defining a family of sets
$V^{\prime}$, we will show that probabilistic masking simulation can be
checked in polynomial time through the symbolic game graph.

In the following we propose to use the symbolic game graph to solve the
infinite game. By doing so, we obtain a polynomial time procedure. Similarly
to Definition 3, we provide an inductive construction of the Refuter-winning
nodes using equation systems in place of sets of polytope vertices, as
follows.

###### Definition 5

Let
$\mathcal{SG}_{A,A^{\prime}}=(V^{\mathcal{SG}},E^{\mathcal{SG}},V^{\mathcal{SG}}_{\mathsf{R}},V^{\mathcal{SG}}_{\mathsf{V}},V^{\mathcal{SG}}_{\mathsf{P}},v_{0}^{\mathcal{SG}})$
be a symbolic game graph for PTSs $A$ and $A^{\prime}$. Sets $U^{i}$ (for
$i\geq 0$) are defined as follows:

$\displaystyle U^{0}={}$ $\displaystyle\\{v_{\text{err}}\\},$ $\displaystyle
U^{i+1}={}$ $\displaystyle\textstyle\\{v^{\prime}\mid v^{\prime}\in
V^{\mathcal{SG}}_{\mathsf{R}}\wedge\mathit{Post}(v^{\prime})\cap
U^{i}\neq\emptyset\\}\cup{}$ $\displaystyle\textstyle\\{v^{\prime}\mid
v^{\prime}\in
V^{\mathcal{SG}}_{\mathsf{V}}\wedge\mathit{Post}(v^{\prime})\subseteq\bigcup_{j\leq
i}U^{j}\wedge\mathit{Post}(v^{\prime})\cap U^{i}\neq\emptyset\\}\cup{}$
$\displaystyle\textstyle\\{v^{\prime}\mid v^{\prime}\in
V^{\mathcal{SG}}_{\mathsf{P}}\wedge\mathit{Post}(v^{\prime})\cap
U^{i}\neq\emptyset\wedge\mathit{Eq}(v^{\prime},\mathit{Post}(v^{\prime})\cap
U^{i})\text{ has no solution}\\}$

Furthermore, we define $U=\bigcup_{i\geq 0}U^{i}$.

The construction of each $U^{i+1}$ follows a similar idea as the construction
of $W^{i+1}$, only varying significantly in the case of the probabilistic
vertices. The first and second line correspond to the Refuter and Verifier
players, respectively. The last one corresponds to the probabilistic player.
Notice that, if $\mathit{Eq}(v^{\prime},\mathit{Post}(v^{\prime})\cap U^{i})$
has no solution, it means that every possible coupling will inevitably lead
with some probability to a “losing” state of a smaller level, since, in
particular, equation $\sum_{(s,\mathchar 45\relax,s^{\prime},\mathchar
45\relax,\mathchar
45\relax,\mathsf{R})\in(\mathit{Post}(v^{\prime}){\cap}U^{i})}x_{s,s^{\prime}}=0$
cannot be satisfied.

There is a strong connection between sets $W^{i}$ and $U^{i}$: a vertex is in
$W^{i}$ if and only if its abstract version is in $U^{i}$. This is formally
stated in the next theorem.

###### Theorem 3.3

Let $\mathcal{G}_{A,A^{\prime}}$ be a stochastic masking game graph for PTSs
$A$ and $A^{\prime}$ and let $\mathcal{SG}_{A,A^{\prime}}$ be the
corresponding symbolic game graph. For every $v\in V^{\mathcal{G}}$, $u\in
V^{\mathcal{SG}}$ such that ${v}[{i}]={u}[{i}]$ (for $0\leq i\leq 4$) and
${v}[{6}]={u}[{5}]$, and for all $k\geq 0$, $v\in U^{k}$ if and only if $u\in
W^{k}$.

The following theorem is a direct consequence of Theorems 3.2 and 3.3.

###### Theorem 3.4

Let $\mathcal{G}_{A,A^{\prime}}$ be a stochastic game graph for PTSs $A$ and
$A^{\prime}$, and let $\mathcal{SG}_{A,A^{\prime}}$ be the corresponding
symbolic game graph. Then, the Verifier has a sure winning strategy in
$\mathcal{G}_{A,A^{\prime}}$ if and only if $v^{\mathcal{SG}}_{0}\notin U$.

As a consequence of this last theorem and Theorem 3.1, it suffices to
calculate the set $U$ over $\mathcal{SG}_{A,A^{\prime}}$ to decide whether
there is a probabilistic masking simulation between $A$ and $A^{\prime}$. This
can be done in polynomial time, since $\mathit{Eq}(v,C)$ can be solved in
polynomial time and the number of iterations to construct $U$ is bounded by
$|V^{\mathcal{SG}}|$. Since $V^{\mathcal{SG}}$ linearly depends on the
transitions of the involved PTSs, we have the following theorem.

###### Theorem 3.5

Let $A$ and $A^{\prime}$ be PTSs. $A\preceq_{m}A^{\prime}$ can be decided in
time $O(\textit{Poly}(m\cdot m^{\prime}))$, where $m$ and $m^{\prime}$ are the
size of the transitions of $A$ and $A^{\prime}$, respectively.

##  4 Quantifying Fault Tolerance in Almost-Sure Failing Systems

Probabilistic masking simulation determines whether a fault-tolerant
implementation is able to completely mask faults. However, in practice, this
kind of masking fault-tolerance is uncommon. Usually, fault-tolerant systems
are able to mask a number of faults before suffering a failure. Our main goal
in this section is to extend the game theory presented in the previous section
to be able to measure the amount of masking tolerance exhibited by a system
before it fails. To do this, we extend the probabilistic masking games with a
quantitative objective function. This is done in such a way that the expected
value of this function indicates the number of “milestones” that the fault-
tolerant implementation is expected to cross before failing. A milestone is
any interesting event that may occur during the execution of the system. For
instance, a milestone may be the number of faults occurring during the
execution of the system, and therefore this measure will reflect the number of
faults that are tolerated by the system before crashing. Another milestone may
be successful acknowledgments in a transmission protocol, in this case we
measure the expected number of chunks that the protocol is able to transfer
under the occurrence of faults before failing.

To do this type of measuring, we need stochastic games with quantitative
objective functions. Intuitively, these objective functions count the number
of “milestones” observed during a play. Therefore, we first extend stochastic
masking games as follows.

###### Definition 6

Let $A=(S,\Sigma,\rightarrow,s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},\rightarrow^{\prime},s_{0}^{\prime})$
be two PTSs. A _stochastic masking game graph with milestones_ $\mathcal{M}$
is a tuple
$\mathcal{MG}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}},\mathcal{M})$
where:  (i)
$(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$is
a stochastic masking game graph,  (ii)
$\mathcal{M}\subseteq\Sigma_{\mathcal{F}}^{2}$is the set of _milestones_ , and
(iii) $\mathit{r}^{\mathcal{G}}(v)=\chi_{\mathcal{M}}({v}[{1}])$is a _reward
function_.

In this definition, $\chi_{B}$ is the characteristic function over set $B$
defined as usual: $\chi_{B}(a)=1$ whenever $(a{\in}B)$ and $\chi_{B}(a)=0$
otherwise. If $B=\\{b\\}$ is a singleton set, we simply write $\chi_{b}$.

Given a stochastic masking game graph with milestones and reward function
$r^{\mathcal{G}}$, for any play $\rho=\rho_{0},\rho_{1},\dots$, we define the
_masking payoff function_ by
$f_{m}(\rho)=\lim_{n\rightarrow\infty}(\sum^{n}_{i=0}\mathit{r}^{\mathcal{G}}(\rho_{i}))$.

Intuitively, the payoff function $f_{m}$ characterizes the number of
milestones that a fault-tolerant implementation is able to achieve until the
error state is reached. This type of payoff functions are usually called
_total rewards_ in the literature. One may think of this as a game played by
the fault-tolerance built-in mechanism and a (malicious) player that chooses
the way in which faults occur. In this game, the Verifier is the maximizer
(she intends to obtain as much milestones as possible) and the Refuter is the
minimizer (she intends to prevent the Verifier from achieving milestones).

For the game of expected total reward to be determined, we need that the
stochastic game is almost-sure stopping, i.e., that the game reaches a sink
vertex with probability 1 [16]. We manage to extend the determinacy property
to games that are almost-sure stopping under the condition that the minimizing
player is fair [7].

In our setting, this amounts to considering _almost-sure failing masking
games_ , that is, games in which the error state $v_{\text{err}}$ is reached
with probability 1. Moreover, we require that the Refuter plays fair. This is
necessary to avoid the Refuter stalls the game in an unproductive loop.
Indeed, consider the scenario described in Example 1 and set the stochastic
masking game between the nominal and faulty model of Figure 1 (omitting the
red part). One would expect that the game leads to a failure with probability
1. However, the Refuter has strategies for which the probability of reaching
$v_{\text{err}}$ is less than $1$. For instance, the Refuter may always play
the reading action, and hence the Verifier has to mimic this action forever,
this yields a probability of $0$ of reaching the error state. Observe that, in
this scenario, the Refuter is behaving in a benevolent manner, playing with
the aim to avoid the error state. Clearly, this is against the spirit of the
behaviour of faults which one expects they happen if waiting long enough.
Therefore the assumption that the Refuter is fair in the sense that, if some
action or fault is infinitely often enabled for the Refuter, it will
eventually play such action or fault.

The setting for the stochastic game with the masking payoff function as
objective that we present in the rest of the section stands on [7], only that
here special care is needed due to the infinite nature of the stochastic game
graphs. For this reason we limit the results of the rest of the section to
(randomized) memoryless strategies and postpone the general result for further
work. Thus, we let $\Pi_{\mathsf{V}}^{\mathsf{M}}$ and
$\Pi_{\mathsf{R}}^{\mathsf{M}}$ denote the sets of all (randomized) memoryless
strategies for the Verifier and the Refuter, respectively, and similarly, we
let $\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}$ and
$\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}$ denote the sets of all pure (or
deterministic) memoryless strategies.

A Refuter’s fair play is defined as a play in which the Refuter commits to
follow a strong fair pattern, i.e., that includes infinitely often any
transition that is enabled infinitely often. A fair strategy for the Refuter,
is a strategy that always measures 1 on the set of all the Refuter’s fair
plays, regardless of the strategy of the Verifier. The definition provided
below follows the style in [5, 4, 7].

###### Definition 7

Given a masking game
$\mathcal{G}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$,
the _set of all Refuter’s fair plays_ is defined by
$\mathit{RFP}=\\{\omega\in\Omega\mid v\in\inf(\omega)\cap
V^{\mathcal{G}}_{\mathsf{R}}\Rightarrow\mathit{Post}(v)\subseteq\inf(\omega)\\}$.
A Refuter strategy $\pi_{\mathsf{R}}$ is said to be _almost-sure fair_ iff,
for every Verifier’s strategy $\pi_{\mathsf{V}}$,
$\mathit{Prob}^{\pi_{\mathsf{R}},\pi_{\mathsf{V}}}_{\mathcal{G}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\mathit{RFP})=1$.

Under this concept, the stochastic masking game is almost-sure failing under
fairness if for every Verifier’s strategy and every Refuter’s fair strategy,
the game leads to an error with probability 1. This is formally defined as
follows.

###### Definition 8

Let $A$ and $A^{\prime}$ be two PTSs. We say that the stochastich masking game
$\mathcal{G}_{A,A^{\prime}}$ is _almost-sure failing under fairness (and
memoryless strategies)_ iff, for every memoryless strategy
$\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}$ and any fair memoryless
strategy $\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}$,
$\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{G}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\Diamond
v_{\text{err}})=1$.

Interestingly, under strong fairness assumptions the determinacy of games is
preserved [7]. Furthermore, in finite stochastic games with fairness
restrictions the value of the game can be computed by calculating the greatest
fixed point of the following Bellman functional. We can adapt this result to
our games by using the vertices of the polytopes when computing the values of
the probabilistic states.

###### Theorem 4.1

Let $\mathcal{MG}_{A,A^{\prime}}$ be a stochastic game with milestones for
some PTSs $A$ and $A^{\prime}$ that is almost-sure failing for fair Refuter’s
strategies. Then, we have:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]=\sup_{\pi_{\mathsf{V}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}}\inf_{\pi_{\mathsf{R}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]<\infty.$

Moreover, the value of the game for memoryless strategies for the Verifier and
fair memoryless Refuter’s strategies is the greatest fixpoint of the following
functional $L$:

$L(f)(v)=\begin{cases}\displaystyle\min\\{\mathsf{u},\max_{w\in\mathbb{V}(\mathbb{C}({v}[{3}],{v}[{4}]))}\\{\chi_{\mathcal{M}}({v}[{1}])+\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])f(v^{\prime})\\}\\}&\text{
if }v\in V^{\mathcal{SG}}_{\mathsf{P}}\\\
\displaystyle\min\\{\mathsf{u},\max\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}}_{\mathsf{V}},\\\
\displaystyle\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}}_{\mathsf{R}},\\\ \displaystyle 0&\text{ if
}v=v_{\text{err}}.\displaystyle\end{cases}$

where $\mathsf{u}$ is a number such that
$\mathsf{u}\geq\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}[f_{m}]$.

Also, we can check whether a game is almost-sure failing under fairness by
computing predecessor sets in the symbolic game graph. To do so, we define the
symbolic version of the predecessor sets. Given a game
$\mathcal{G}_{A,A^{\prime}}$ and its symbolic version
$\mathcal{SG}_{A,A^{\prime}}$, let $\exists\mathit{Pre}^{S}_{f}(C)$ and
$\forall\mathit{Pre}^{S}_{f}(C)$, for a given set $C$ of symbolic vertices, be
defined as follows:

$\displaystyle\exists\mathit{Pre}^{S}_{f}(C)={}$ $\displaystyle\\{v\in
V^{\mathcal{SG}}_{\mathsf{P}}\mid\exists v^{\prime}\in C\cap
V^{\mathcal{SG}}_{\mathsf{R}}:{v^{\prime}}[{0}]\in\mathit{Supp}({v}[{3}])\land{v^{\prime}}[{2}]\in\mathit{Supp}({v}[{4}])\\}$
$\displaystyle\cup\\{v\in V^{\mathcal{SG}}_{\mathsf{V}}\cup
V^{\mathcal{SG}}_{\mathsf{R}}\mid\exists v^{\prime}\in C:(v,v^{\prime})\in
E^{\mathcal{SG}}_{A,A^{\prime}}\\}$
$\displaystyle\forall\mathit{Pre}^{S}_{f}(C)={}$ $\displaystyle\\{v\in
V^{\mathcal{SG}}_{\mathsf{P}}\mid\mathit{Eq}(v,C)\textit{ has no solution
}\\}$ $\displaystyle\cup\\{v\in V^{\mathcal{SG}}_{\mathsf{V}}\mid\forall
v^{\prime}\in C:(v,v^{\prime})\in E^{\mathcal{SG}}\Rightarrow v^{\prime}\in
C\\}$ $\displaystyle\cup\\{v\in V^{\mathcal{SG}}_{\mathsf{R}}\mid\exists
v^{\prime}\in C:(v,v^{\prime})\in E^{\mathcal{SG}}\\}$

In particular, the first set in the definition of
$\exists\mathit{Pre}^{S}_{f}(C)$ collects all probabilistic vertices $v$ for
which there is a coupling that leads to a Refuter vertex $v^{\prime}$ in $C$.
For this is sufficient to check that the states ${v^{\prime}}[{0}]$ and
${v^{\prime}}[{2}]$ that define $v^{\prime}$ are on the respective support
sets of the probabilities ${v}[{3}]$ and ${v}[{4}]$ that define $v$ (since it
is always possible to define a coupling that assigns positive probability to a
pair of states in the respective support sets). The first set in the
definition of $\forall\mathit{Pre}^{S}_{f}(C)$ collects all probabilistic
vertices $v$ for which there is no coupling “avoiding” $C$, that is, no
coupling that leads with probability 0 to the set of all pair of states
defining a vertex in $C$. A coupling avoiding $C$ will solve
$\mathit{Eq}(v,C)$. By using $\exists\mathit{Pre}^{S}_{f}$ and
$\forall\mathit{Pre}^{S}_{f}$ recursively, we can decide whether a game is
almost-sure failing under fairness as follows.

###### Theorem 4.2

Given a masking game $\mathcal{G}_{A,A^{\prime}}$ and its symbolic version
$\mathcal{SG}_{A,A^{\prime}}$, we have that $\mathcal{G}_{A,A^{\prime}}$ is
almost-sure failing under fairness iff $v_{0}^{\mathcal{G}}\in
V^{\mathcal{SG}}\setminus{\exists\mathit{Pre}^{S}_{f}}^{*}(V^{\mathcal{SG}}\setminus{\forall\mathit{Pre}^{S}_{f}}^{*}(v_{\text{err}})),$
where $v_{0}^{\mathcal{G}}$ is the initial state of
$\mathcal{SG}_{A,A^{\prime}}$ and $V^{\mathcal{SG}}$ its sets of vertices.

As $\mathit{Eq}(v,C)$ can be computed in polynomial time, so do the
predecessor sets $\exists\mathit{Pre}^{S}_{f}(C)$ and
$\forall\mathit{Pre}^{S}_{f}(C)$. As a consequence, the problem of deciding
whether a stochastic masking game is almost-sure failing under fairness is
also polynomial.

##  5 Experimental Evaluation

We implemented the approach described in this paper in a prototype tool,
available at [1]. Tables 3, 3 and 3 report the results obtained for three case
studies: a Redundant Cell Memory (our running example); N-Modular Redundancy
(NMR), a standard example of fault-tolerance [28]; and a NMR processor/memory
architecture with N voters [23]. In the tables, $M_{t}$ and $M_{r}$ are used
to indicate the measurement results for the tick and refresh actions,
considered as milestones, respectively.

Some words are useful to interpret the results. For the memory cell example,
either increasing the redundancy, or augmenting the frequency of refreshing,
have positive effects in the measures. In practice, these values can be taken
into account when designing a fault-tolerant component that provides an
optimal balance between fault-tolerance and hardware costs. For example,
assuming a fault probability of $0.05$, one might prefer $3$ bits and more
frequent refreshing, over $5$ bits with a less often refreshing, despite the
software overhead. NMR consists of N modules that independently perform a
task, and whose results are processed by a perfect voter to produce a single
output. These modules may exhibit an unexpected behavior with a given
probability, in which case they output an incorrect value. The results for
this case study are similar to the memory cell example when there is $0$
probability of refreshing. The last case study consists of N processors that
output a value to a memory module through N voters. Both the voters and
processors may output an incorrect value with certain probability. The
experiment outputs the same results if the fault probability of voters and
processors are exchanged. This suggests that, provided that the probability
that a pair processor-voter fails remains the same, the system is more
tolerant when faults occur equally distributed on voters and processors.

We have run our experiments on a MacBook Air with processor 1.3 GHz Intel Core
i5 and a memory of 4 Gb. The tool and case studies are available in the tool
repository [1].

Bits | Fault Prob. | Refresh Prob. | $M_{t}$ | $M_{r}$
---|---|---|---|---
3 | $0.5$ | $0.5$ | $6$ | $3$
$0.1$ | $4.44$ | $0.44$
$0.05$ | $4.2$ | $0.21$
$0.1$ | $0.5$ | $70$ | $35$
$0.1$ | $30$ | $3$
$0.05$ | $25$ | $1.25$
$0.05$ | $0.5$ | $240.02$ | $120.01$
$0.1$ | $80$ | $8$
$0.05$ | $60$ | $3$
5 | $0.5$ | $0.5$ | $14$ | $7$
$0.1$ | $7.28$ | $0.72$
$0.05$ | $6.62$ | $0.33$
$0.1$ | $0.5$ | $430$ | $215.02$
$0.1$ | $70$ | $7$
$0.05$ | $47.5$ | $2.38$
$0.05$ | $0.5$ | $2660.1$ | $1330.06$
$0.1$ | $260.01$ | $26.01$
$0.05$ | $140$ | $7$
7 | $0.5$ | $0.5$ | $30$ | $15$
$0.1$ | $10.74$ | $1.07$
$0.05$ | $9.28$ | $0.46$
$0.1$ | $0.5$ | $2590.1$ | $1295.05$
$0.1$ | $150$ | $15$
$0.05$ | $81.25$ | $4.06$
$0.05$ | $0.5$ | $29281$ | $14640.5$
$0.1$ | $800.03$ | $80.03$
$0.05$ | $300$ | $15$

Table 1: Experimental results on a Redundant Memory Cell.

Modules | Fault Prob. | $M_{t}$
---|---|---
$3$ | $0.5$ | $4$
$0.1$ | $20$
$0.05$ | $40$
$5$ | $0.5$ | $6$
$0.1$ | $30$
$0.05$ | $60$
$7$ | $0.5$ | $8$
$0.1$ | $40$
$0.05$ | $80$

Table 2: Experimental results on a N-Modular Redundant System.

N | P.Fault Prob. | V.Fault Prob. | $M_{t}$
---|---|---|---
$3$ | $0.09$ | $0.01$ | $21.8$
$0.07$ | $0.03$ | $24.2$
$0.05$ | $0.05$ | $25$
$5$ | $0.09$ | $0.01$ | $33.18$
$0.07$ | $0.03$ | $38.94$
$0.05$ | $0.05$ | $41.25$
$7$ | $0.09$ | $0.01$ | $44.39$
$0.07$ | $0.03$ | $53.78$
$0.05$ | $0.05$ | $58.12$
$9$ | $0.09$ | $0.01$ | $55.53$
$0.07$ | $0.03$ | $68.58$
$0.05$ | $0.05$ | $75.39$

Table 3: Experimental results on a NMR processor/memory architecture with N
voters.

##  6 Related Work

The games introduced in [2, 3, 14, 15] are based on probabilistic
bisimulation, so they are symmetric. Furthermore, in [14, 15] the nodes of the
game graph are modeled using subsets of states of the PTSs, in our formulation
we do not use subsets of states. The games defined in [2, 3] use Kanterovich’s
and Hausdorff’s liftings to deal with probabilistic distributions and non-
determinism, respectively. In addition, the authors use the vertices of the
transportation polytopes to model the probabilistic vertices. In contrast, we
introduced a symbolic representation of games to avoid the state explosion
caused by the vertices of the polytopes. Also note that the metrics introduced
in [2, 3] measure the (probabilistic) bisimulation distance between two PTSs,
which for almost-sure failing systems is always $1$.

Another related framework is defined in [25]. Therein, the authors introduce a
notion of weak simulation quasimetric tailored for reasoning about the
evolution of _gossip protocols_. This makes it possible to compare network
protocols that have similar behaviour up to a certain tolerance; being $0$ and
$1$ the minimum and maximum distance, respectively. Note that using this
quasimetric to compare a network protocol with an almost-sure failing
implementation will always return $1$, thus that approach cannot be used to
quantify the masking fault-tolerance of almost-sure failing systems.

After the case studies of Section 5, _Mean-Time To Failure_ (MTTF) [27] may
come to mind. Though this metric (lifted to games) may be the result of a
particular case study, we present a much more general framework. Indeed, on
the one hand, we do not necessarily have to count time units, and other events
may be set as milestones. On the other hand, the computation of MTTF would
normally require the identification of failures states in an ad hoc manner,
while we do this at a higher level of abstraction: the failure situation
appears in the game as a result of comparing the implementation model against
the nominal model.

##  7 Conclusions and Future Work

We presented a relation of masking fault-tolerance between probabilistic
transition systems, which is accompanied by a corresponding probabilistic game
characterization. Even though the game could be infinite, we proposed an
alternative finite symbolic representation by means of which the game can be
solved in polynomial time. We extended the game with quantitative objectives
based on counting “milestones” thus providing a way to quantify the amount of
masking fault tolerance provided by a given implementation. As this game
inherits the characteristic of total reward objectives, some stopping
criterion is necessary and thus the game is required to be almost-sure failing
under a fair Refuter. By restricting to (randomize) memoryless strategies, we
could show that the resulting game is determined and can be computed by
solving a collection of functional equations. We also provided a polynomial
technique to decide whether a game is almost-sure failing under fairness.

There are many directions for future work. As an immediate one, we have
pending to extend the result on quantitative objectives to non-memoryless
strategies. Given the result in [7], we believe this is possible but special
care is needed to deal with the infinite nature of the game. In a different
direction, in this paper we introduced a strong version of probabilistic
masking simulation. However, for analyzing non-trivial systems, a weak version
of this kind of relation is needed since it could abstract away from internal
transitions which are mostly associated with the fault-tolerant machinery of
the implementation. Besides, we have so far only worked with masking fault-
tolerance. Similar ideas to those presented in this paper could be
extrapolated to other levels of fault-tolerance like fail-safe and non-
masking. Finally, we have presented a prototype tool for measuring some well-
known small case studies. Our goal is to develop an automated tool to support
the use of these measurements in practice.

## References

  * [1] Tolerange.  https://github.com/cl-unrc-lab/Tolerange.
  * [2] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  On-the-fly computation of bisimilarity distances.  Logical Methods in Computer Science, 13(2), 2017.
  * [3] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel.  Computing probabilistic bisimilarity distances for probabilistic automata.  In Wan Fokkink and Rob van Glabbeek, editors, 30th International Conference on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the Netherlands, volume 140 of LIPIcs, pages 9:1–9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [4] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking (Representation and Mind Series).  The MIT Press, 2008.
  * [5] Christel Baier and Marta Z. Kwiatkowska.  Model checking for a probabilistic branching time logic with fairness.  Distributed Comput., 11(3):125–155, 1998.  doi:10.1007/s004460050046.
  * [6] Pablo F. Castro, Pedro R. D’Argenio, Ramiro Demasi, and Luciano Putruele.  Measuring masking fault-tolerance.  In TACAS 2019, Prague, Czech Republic, 2019.
  * [7] Pablo F. Castro, Pedro R. D’Argenio, Luciano Putruele, and Ramiro Demasi.  Playing against fair adversaries in stochastic games with total rewards.  CoRR, abs/2112.09811, 2021.  Submitted.  URL: https://arxiv.org/abs/2112.09811, arXiv:2112.09811.
  * [8] Pavol Cerný, Thomas A. Henzinger, and Arjun Radhakrishna.  Simulation distances.  Theor. Comput. Sci., 413(1):21–35, 2012.
  * [9] Krishnendu Chatterjee and Thomas A. Henzinger.  Value iteration.  In Orna Grumberg and Helmut Veith, editors, 25 Years of Model Checking - History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, pages 107–138. Springer, 2008.
  * [10] Krishnendu Chatterjee and Thomas A. Henzinger.  A survey of stochastic $\omega$-regular games.  J. Comput. Syst. Sci., 78(2):394–413, 2012.
  * [11] Anne Condon.  On algorithms for simple stochastic games.  In Jin-Yi Cai, editor, Advances In Computational Complexity Theory, Proceedings of a DIMACS Workshop, New Jersey, USA, December 3-7, 1990, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51–71. DIMACS/AMS, 1990.
  * [12] Anne Condon.  The complexity of stochastic games.  Inf. Comput., 96(2):203–224, 1992.
  * [13] Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga.  Linear and branching system metrics.  IEEE Trans. Software Eng., 35(2):258–273, 2009.
  * [14] Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled markov processes.  Theor. Comput. Sci., 318(3):323–354, 2004.
  * [15] Josée Desharnais, François Laviolette, and Amélie Turgeon.  A logical duality for underspecified probabilistic systems.  Inf. Comput., 209(5):850–871, 2011.
  * [16] Jerzy Filar and Koos Vrieze.  Competitive Markov Decision Processes.  Springer-Verlag, Berlin, Heidelberg, 1996.
  * [17] Thomas A. Henzinger.  Quantitative reactive modeling and verification.  Computer Science - R&D, 28(4):331–344, 2013.
  * [18] Thomas A. Henzinger, Rupak Majumdar, and Vinayak S. Prabhu.  Quantifying similarities between timed systems.  In Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, pages 226–241, 2005.
  * [19] Bengt Jonsson and Kim G. Larsen.  Specification and refinement of probabilistic processes.  In 6th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 1991.
  * [20] Marcin Jurdziński.  Algorithms for solving parity games.  In Krzysztof R. Apt and Erich Grädel, editors, Lectures in Game Theory for Computer Scientist, chapter 3, pages 74–95. Cambridge University Press, New York, NY, USA, 2011.
  * [21] Edon Kelmendi, Julia Krämer, Jan Kretínský, and Maximilian Weininger.  Value iteration for simple stochastic games: Stopping criterion and learning algorithm.  In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 623–642. Springer, 2018.
  * [22] V. Klee and C. Witzgall.  Facets and vertices of transportation polytopes.  In B. Dantzig and A.F. Veinott Jr., editors, Mathematics of the Decision Science, Part I. American Mathematical Society, 1968.
  * [23] Israel Koren and C. M. Krishna.  Fault-Tolerant Systems.  Elsevier Science, 2007.
  * [24] Marta Z. Kwiatkowska, Gethin Norman, and David Parker.  PRISM 4.0: Verification of probabilistic real-time systems.  In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585–591. Springer, 2011.  doi:10.1007/978-3-642-22110-1_47.
  * [25] Ruggero Lanotte, Massimo Merro, and Simone Tini.  Weak simulation quasimetric in a gossip scenario.  In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings, volume 10321 of Lecture Notes in Computer Science, pages 139–155. Springer, 2017.
  * [26] Kim G. Larsen, Uli Fahrenberg, and Claus R. Thrane.  Metrics for weighted transition systems: Axiomatization and complexity.  Theor. Comput. Sci., 412(28):3358–3369, 2011.
  * [27] J. Lienig and H. Bruemmer.  Reliability Analysis.  Springer International Publishing, 2017.
  * [28] Martin L. Shooman.  Reliability of Computer Systems and Networks: Fault Tolerance,Analysis,and Design.  John Wiley & Sons, Inc, 2002.
  * [29] Corlin Stirling.  The joys of bisimulation.  In Proceedings of MFCS’98, volume 1450 of LNCS. Springer, 1998\.
  * [30] Qiyi Tang and Franck van Breugel.  Deciding probabilistic bisimilarity distance one for labelled markov chains.  In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 681–699. Springer, 2018.
  * [31] Claus R. Thrane, Uli Fahrenberg, and Kim G. Larsen.  Quantitative analysis of weighted transition systems.  J. Log. Algebr. Program., 79(7):689–703, 2010.

##  Appendix 0.A Proofs of Properties

Proof of Theorem 3.1. Let $A=(S,\Sigma,\rightarrow,s_{0})$ and
$A^{\prime}=(S^{\prime},\Sigma_{\mathcal{F}},\rightarrow^{\prime},s_{0}^{\prime})$
be two PTSs. We have $A\preceq_{m}A^{\prime}$ iff the Verifier has a sure
winning strategy for the stochastic masking game graph
$\mathcal{G}_{A,A^{\prime}}$ with the Boolean objective
$\Phi=\\{\omega_{0},\omega_{1},\dots\in\Omega\mid\forall{i\geq
0}:\omega_{i}\neq v_{\text{err}}\\}$.

###### Proof

“Only If”: Assume $A\preceq_{m}A^{\prime}$, thus there is a probabilistic
masking simulation $\mathbin{\mathbf{M}}\subseteq S\times S^{\prime}$. Let us
define a sure winning strategy $\pi_{\mathsf{V}}$ for the Verifier as follows.
Given a state $(s,\sigma^{1},s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V})$ (resp. $(s,\sigma^{2},s^{\prime},\mathchar
45\relax,\mu^{\prime},\mathchar 45\relax,\mathsf{V})$), if
$s\mathbin{\mathbf{M}}s^{\prime}$, $\pi_{\mathsf{V}}$ selects a transition
$((s,\sigma^{1},s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V}),(s,\sigma^{1},s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}))$
(resp. $((s,\sigma^{2},s^{\prime},\mathchar 45\relax,\mu^{\prime},\mathchar
45\relax,\mathsf{V}),(s,\sigma^{2},s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}))$)
such that $w$ is a $\mathbin{\mathbf{M}}$-respecting coupling for
($\mu,\mu^{\prime}$) (which is guaranteed to exist by Def. 1). Otherwise,
$\pi_{\mathsf{V}}$ selects an arbitrary vertex. Let us show that this strategy
is sure winning for the Verifier in the initial state. We have to prove that,
for any Refuter’s strategy $\pi_{\mathsf{R}}$, we have
$\mathit{out}(\pi_{\mathsf{V}},\pi_{\mathsf{R}})\subseteq\Omega\setminus\Phi$,
where $\mathit{out}(\pi_{\mathsf{V}},\pi_{\mathsf{R}})$ denotes the set of
paths generated when strategies $\pi_{\mathsf{R}}$ and $\pi_{\mathsf{V}}$ are
used. Let $\pi_{\mathsf{R}}$ be any strategy for the Refuter, and
$\omega=\omega_{0},\omega_{1},\dots$ the corresponding play in
$\text{out}(\pi_{\mathsf{V}},\pi_{\mathsf{R}})$. We prove by induction that
$\forall i\geq 0:\omega_{i}\neq
v_{\text{err}}\wedge({\omega_{i}}[{6}]\neq\mathsf{R}\Rightarrow{\omega_{i}}[{0}]\mathbin{\mathbf{M}}{\omega_{i}}[{2}])$.
For $i=0$, the proof is straightforward. Assume that the property holds for
$\omega_{i}$, if $\omega_{i}$ is a Verifier’s vertex and
${\omega}[{1}]=\sigma^{1}$ (resp. $\sigma^{2}$) with
$\sigma\notin\mathcal{F}$, then by definition of $\pi_{\mathsf{V}}$ and Def. 1
$\omega_{i+1}=(s,\sigma^{1},s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})$ (resp.
$\omega_{i+1}=(s,\sigma^{2},s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})$). Thus,
we have by inductive hypothesis that $s\mathbin{\mathbf{M}}s^{\prime}$ and
also that $\omega_{i+1}\neq v_{\text{err}}$. If
${\omega_{i}}[{1}]\in\mathcal{F}$, then the proof is similar, but taking into
account that $\mu=\Delta_{s}$. If $\omega_{i}$ is a Refuter’s vertex, then
$\omega_{i+1}$ is a Verifier’s vertex, and it cannot be $v_{\text{err}}$
because by construction only Verifier’s nodes are adjacent to the
$v_{\text{err}}$. If $\omega_{i}$ is a probabilistic vertex, then note that
$\mathit{Supp}({\omega_{i}}[{5}])\neq\emptyset$ and therefore
$v_{\text{err}}\neq\omega_{i+1}$. Thereby,
${\omega_{i+1}}[{0}]\mathbin{\mathbf{M}}{\omega_{i+1}}[{2}]$. That is,
$\forall i\geq 0:\omega_{i}\neq v_{\text{err}}$. Hence,
$\omega\in\Omega\setminus\Phi$.

“If”: Suppose that the Verifier has a sure winning strategy $\pi_{\mathsf{V}}$
from the initial state. Then, we define a probabilistic masking simulation
relation as follows: $\mathbin{\mathbf{M}}=\\{(s,s^{\prime})\mid(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in\pi_{\mathsf{V}}(V^{\mathcal{G}}_{\mathsf{V}})$
for some sure winning strategy $\pi_{\mathsf{V}}\\}$. We know by our
assumption that this set is not empty and it is direct to see that
$(s_{0},s^{\prime}_{0})\in\mathbin{\mathbf{M}}$. First, let us prove that for
any $(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in\pi_{\mathsf{V}}(V^{\mathcal{G}}_{\mathsf{V}})$
we have $\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$. Assume $(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\in\pi_{\mathsf{V}}(V^{\mathcal{G}}_{\mathsf{V}})$
and it is not the case that $\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$, or
equivalently $\exists
t,t^{\prime}:w(t,t^{\prime})>0\wedge\neg(t\mathbin{\mathbf{M}}t^{\prime})$.
Thus, we have a successor $(t,\mathchar 45\relax,t^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathchar 45\relax,\mathsf{R})$ of $(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})$ which can be chosen with
probability greater than $0$ and $(t,t^{\prime})\notin\mathbin{\mathbf{M}}$.
Furthermore, there exists a $t\xrightarrow{\sigma}t_{0}$ (or
$t^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}t^{\prime}_{0}$) such
that $(t_{0},\sigma^{1},t^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V})\in\mathit{Post}((t,\mathchar
45\relax,t^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R}))$ (resp. $(t,\sigma^{2},t^{\prime}_{0},\mathchar
45\relax,\mu^{\prime},\mathchar
45\relax,\mathsf{V})\in\mathit{Post}((t,\mathchar
45\relax,t^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R}))$). This state cannot be $v_{\text{err}}$ and there must
be a winning strategy for the Verifier from it; otherwise, the Refuter would
have a winning strategy from $(t,\mathchar 45\relax,t^{\prime},\mathchar
45\relax,\mathchar 45\relax,\mathchar 45\relax,\mathsf{R})$, and $(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})\notin\mathit{Im}(\pi)$ for
some winning strategy $\pi_{\mathsf{V}}$ for the Verifier. But then
$(t,t^{\prime})\notin\mathbin{\mathbf{M}}$, contradicting the assumption
above. Thus, $\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$.

Let us now prove that $\mathbin{\mathbf{M}}$ is a probabilistic masking
simulation. Assume that $s\mathbin{\mathbf{M}}s^{\prime}$ and
$s\xrightarrow{a}\mu$, for any successor $(s,a,s^{\prime},\mu,\mathchar
45\relax,\mathchar 45\relax,\mathsf{V})$ of $(s,\mathchar
45\relax,s^{\prime},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R})$ we have a sure winning strategy $\pi_{\mathsf{V}}$ for
$\mathsf{V}$, such that: $\pi((s,a,s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V}))=(s,a,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})$. That
is, there is a $s^{\prime}\xrightarrow{a}\mu^{\prime}$ and also by the
property proven above, we have $\mu\mathbin{\mathbf{M^{\\#}}}\mu^{\prime}$.
Similarly for the cases: $s^{\prime}\xrightarrow{a}\mu^{\prime}$ and
$s^{\prime}\xrightarrow{F}\mu^{\prime}$ for $F\in\mathcal{F}$. Finally, since
$\mathsf{V}$ has a winning strategy from $(s_{0},\mathchar
45\relax,s^{\prime}_{0},\mathchar 45\relax,\mathchar 45\relax,\mathchar
45\relax,\mathsf{R})$ we have that $s_{0}\mathbin{\mathbf{M}}s^{\prime}_{0}$.
Thus, all the requirements of Def. 1 holds, and so $\mathbin{\mathbf{M}}$ is a
probabilistic masking relation.

Proof of Theorem 3.2. Let
$\mathcal{G}_{A,A^{\prime}}=(V^{\mathcal{G}},E^{\mathcal{G}},V^{\mathcal{G}}_{\mathsf{R}},V^{\mathcal{G}}_{\mathsf{V}},V^{\mathcal{G}}_{\mathsf{P}},v_{0}^{\mathcal{G}},\delta^{\mathcal{G}})$
be a stochastic masking game graph for some PTSs $A$ and $A^{\prime}$, we have
that the Verifier has a sure winning strategy from vertex $v$ iff $v\notin W$.

###### Proof

First, we can define a $2$-player reachability game obtained from
$\mathcal{G}_{A,A^{\prime}}$ by considering the probabilistic nodes as
Refuter’s nodes, and ignoring the probabilistic distribution, let
$\mathcal{H}^{\mathcal{G}}_{A,A^{\prime}}$ be that game. It is clear that a
Verifier’s strategy is sure winning in $\mathcal{G}_{A,A^{\prime}}$ iff this
strategy is winning in $\mathcal{H}^{\mathcal{G}}_{A,A^{\prime}}$. Then,
proving the theorem reduces to show that the sets $W^{i}$ determines the
winning strategies of the Verifier in
$\mathcal{H}^{\mathcal{G}}_{A,A^{\prime}}$ (recall that only the vertices of
the polytopes are taken into account for defining the $W$’s). If the Verifier
has a winning strategy from vertex $v$ let us prove that $v\notin W^{k}$ for
every $k$ by induction. For $k=1$ it is direct. Now, assume that the property
holds for $W^{k}$, let $v$ be an arbitrary vertex such that the Verifier has a
winning strategy named $\pi_{\mathsf{V}}$ from $v$. If $v$ is a Verifier’s
node and $v\in W^{k+1}$, then $\mathbb{V}(\mathit{Post}(v)))\subseteq W^{k}$.
Thus, by inductive hypothesis
$\pi_{\mathsf{V}}(v)\notin\mathbb{V}(\mathit{Post}(v))$, that is,
$\pi_{\mathsf{V}}(v)$ is a probabilistic vertex whose coupling is not a
vertex. Furthermore, it is a Refuter’s node in
$\mathcal{H}^{\mathcal{G}}_{A,A^{\prime}}$. For this node we have
$v^{\prime}\in\mathit{Post}(\pi_{\mathsf{V}}(v))$ iff
${\pi_{\mathsf{V}}(v)}[{5}]({v^{\prime}}[{0}],{v^{\prime}}[{2}])>0$. Note that
${\pi_{\mathsf{V}}(v)}[{5}]$ is a point of the polytope defined by
$\mathbb{C}({\pi_{\mathsf{V}}(v)}[{3}],{\pi_{\mathsf{V}}(v)}[{4}])$, since
polytopes do not contain lines, either ${\pi_{\mathsf{V}}(v)}[{5}]$ is a
vertex or there is a polytope’s vertex $w^{\prime}$ such that
$w^{\prime}({\pi_{\mathsf{V}}(v)}[{3}],{\pi_{\mathsf{V}}(v)}[{4}])>0$ iff
${\pi_{\mathsf{V}}(v)}[{5}]({\pi_{\mathsf{V}}(v)}[{3}],{\pi_{\mathsf{V}}(v)}[{4}])>0$.
Thereby, there is a $v^{\prime\prime}\in\mathbb{V}(\mathit{Post}(v))$ such
that $\mathit{Post}(v^{\prime\prime})=\mathit{Post}(\pi_{\mathsf{V}}(v))$,
that is, $v^{\prime\prime}\in W^{k}$ implies that $\pi_{\mathsf{V}}(v)\in
W^{k}$ which is a contradiction and so $v\notin W^{k+1}$.

Let us define a strategy $\pi_{\mathsf{V}}$ which is winning strategy in
$\mathcal{H}^{\mathcal{G}}_{A,A^{\prime}}$ for any Verifier’s node $v\notin
W$. If $v\notin W$, then $\pi_{\mathsf{V}}(v)=v^{\prime}$ for some
$v^{\prime}\in\mathit{Post}(v)\cap(V^{\mathcal{G}}\setminus W)$ (which is
guaranteed to exist by assumption), moreover, if $v\in W$, then
$\pi_{\mathsf{V}}(v)=v^{\prime}$ for an arbitrary node $v^{\prime}$. Let us
prove that for any play generated by $\pi_{\mathsf{V}}$: $v_{0},v_{1},\dots$
we have $v_{i}\notin W$, the proof is by induction on $i$. For $i=0$ it is
direct, assuming that $v_{i}\notin W$ let us prove that $v_{i+1}\notin W$. If
$v_{i}$ is a Refuter’s node by Def. 3 $\mathit{Post}(v_{i})\cap W=\emptyset$,
and therefore, $v_{i+1}\notin W$. If $v_{i}$ is Verifier’s node, by definition
of $\pi_{\mathsf{V}}$: $v_{i+1}=\pi_{\mathsf{V}}(v_{i})\notin W$ and therefore
the result follows.

Proof of Theorem 3.3. Given a stochastic masking game graph
$\mathcal{G}_{A,A^{\prime}}$ for some PTSs $A$ and $A^{\prime}$ and the
corresponding symbolic game $\mathcal{SG}_{A,A^{\prime}}$. For any states
$v\in V^{\mathcal{G}}$, $u\in V^{\mathcal{SG}}$ such that ${v}[{i}]={u}[{i}]$
(for $0\leq i\leq 4$) and for any $k>0$ we have that: $v\in U^{k}$ iff $u\in
W^{k}$.

###### Proof

The proof is by induction on $k$. For k=1, we have that
$W^{1}=\\{v_{\text{err}}\\}=U^{1}$. For the inductive case, consider arbitrary
nodes $v\in V^{\mathcal{SG}}$ and $u\in V^{G}$, such that ${v}[{i}]={u}[{i}]$
for $0\leq i\leq 4$. Note that these nodes also coincide in their last
components, that is, either both are Refuter’s nodes, Verifier’s nodes, or
probabilistic nodes. Assume these are Refuter’s nodes, if $v\in U^{k}$ then
$\mathit{Post}(v)\cap U^{k-1}\neq\emptyset$. Thus, there is some
$v^{\prime}\in\mathit{Post}(v)\cap U^{k-1}$ which is a probabilistic node. By
Def. 5, we have many $u^{\prime}\in\mathit{Post}(u)$ such that
${v^{\prime}}[{i}]={u^{\prime}}[{i}]$ (for $0\leq i\leq 4$), and by induction
we have that $u^{\prime}\in W^{k-1}$ and therefore $u\in W^{k}$. Similarly, if
$u\in W^{k}$ we have that $\mathit{Post}(u)\cap W^{k-1}\neq\emptyset$, and we
proceed as before. If $v$ and $u$ are Verifier’s nodes the proof is similar.
Now, assume that $v$ and $u$ are probabilistic nodes. If $v\in U^{k}$, then
$\mathit{Post}(v)\cap U^{k-1}\neq\emptyset$. As proved above, we also have
that $\mathit{Post}(u)\cap W^{k-1}\neq\emptyset$. Moreover, if
$\mathit{Eq}(v,\mathit{Post}(v)\cap U^{k-1})$ has no solutions, then we have
at least a coupling (say $w$) for distributions ${v}[{3}]$ and ${v}[{4}]$ that
satisfies the equations and also $w({v^{\prime}}[{0}],{v^{\prime}}[{2}])>0$
for some $v^{\prime}\in\mathit{Post}(v)\cap U^{k-1}$. By Def. 2, we have a
vertex $u^{\prime}\in\mathit{Post}(u)$ such that ${u^{\prime}}[{5}]=w$, and
thus $\sum_{u^{\prime}\in\mathit{Post}(u)\cap
W^{j-1}}\delta^{\mathcal{G}}(u)(u^{\prime})>0$, which means that that
$u^{\prime}\in W^{k}$. Similarly, if $\sum_{u^{\prime}\in\mathit{Post}(u)\cap
W^{j-1}}\delta^{\mathcal{G}}(u)(u^{\prime})>0$ then
$\mathit{Eq}(v,\mathit{Post}(v)\cap U^{k-1})$ has no solutions, and then $u\in
W^{k}$ implies $v\in U^{k}$.

Proof of Theorem 4.1. Let $\mathcal{MG}_{A,A^{\prime}}$ be a stochastic game
with milestones for some PTSs $A$ and $A^{\prime}$ that is almost-sure failing
for fair Refuter’s strategies. Then:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]=\sup_{\pi_{\mathsf{V}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}}\inf_{\pi_{\mathsf{R}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]<\infty$

Furthermore, the value of the game for memoryless strategies for the Verifier
and fair Memoryless Refuter’s strategies is the greatest fixpoint of the
following functional $L$:

$L(f)(v)=\begin{cases}\displaystyle\min\\{\mathsf{u},\max_{w\in\mathbb{V}(\mathbb{C}({v}[{3}],{v}[{4}]))}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])f(v^{\prime})\\}\\}&\text{
if }v\in V^{\mathcal{SG}}_{\mathsf{P}}\\\
\displaystyle\min\\{\mathsf{u},\max\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}}_{\mathsf{V}},\\\
\displaystyle\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}}_{\mathsf{R}},\\\ \displaystyle 0&\text{ if
}v=v_{\text{err}}.\displaystyle\end{cases}$

where $\mathsf{u}$ is a number such that
$\mathsf{u}\geq\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]$,
for every $v$.

###### Proof

First we prove that we can safely restrict to deterministic strategies when
computing the value of the game for memoryless strategies. To do so, we prove
that for every memoryless strategies $\pi_{\mathsf{V}}$ and
$\pi_{\mathsf{R}}$, there is a memoryless and deterministic strategy
$\pi_{\mathsf{V}}^{\prime}$ such that:
$\mathbb{E}^{\pi_{\mathsf{V}}^{\prime},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]\geq\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]$.
To do so, note that any memoryless strategy satisfies the following equation
for every $v\in V^{\mathcal{G}}_{\mathsf{V}}$:

$\displaystyle\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$
$\displaystyle\leq\mathit{r}(v)+\sum_{v^{\prime}\in\mathit{Post}(v)}\delta^{\pi_{\mathsf{R}},\pi_{\mathsf{V}}}(v,v^{\prime})\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$
(1)
$\displaystyle\leq\mathit{r}(v)+\max_{v^{\prime}\in\mathit{Post}(v)}\\{\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\\}$
(2)

The first inequality follows from the definition of expected value, the second
inequality follows since
$\sum_{v^{\prime}\in\mathit{Post}(v)}\delta^{\pi_{\mathsf{R}},\pi_{\mathsf{V}}}(v,v^{\prime})\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$
is a convex combination. That is, defining
$\pi_{\mathsf{V}}^{\prime}(v)=\operatorname*{argmax}_{v^{\prime}\in\mathit{Post}(v)}\\{\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\\}$,
for every $v$, we obtain
$\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v}^{\pi_{\mathsf{V}}^{\prime},\pi_{\mathsf{R}}}[f_{m}]$.
Similarly we can prove that for every memoryless strategies $\pi_{\mathsf{R}}$
and $\pi_{\mathsf{V}}$, there is a memoryless, deterministic and fair strategy
$\pi_{\mathsf{R}}^{\prime}$ such that
$\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}^{\prime}}[f_{m}]\leq\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$.
These properties imply that:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]=\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$

and similarly:

$\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]=\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{MG}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}].$

Now, we prove the theorem. We define a restricted (finite) game just taking
into account the vertices of the polytope defined by the couplings. Consider
the subgame $\mathcal{H}_{A,A^{\prime}}$ obtained from
$\mathcal{MG}_{A,A^{\prime}}$ by restricting the successors of Verifier’s
vertices to the following sets:

  * •

$\\{((s,\sigma^{2},s^{\prime},\mathchar 45\relax,\mu^{\prime},\mathchar
45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}))\mid(\exists\;\sigma\in\Sigma:s\xrightarrow{\sigma}\mu)\wedge
w\in\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime}))\\}\subseteq E^{\mathcal{G}}$ for
any $\sigma\notin\mathcal{F}$,

  * •

$\\{((s,\sigma^{1},s^{\prime},\mu,\mathchar 45\relax,\mathchar
45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P}))\mid(\exists\;\sigma\in\Sigma:s^{\prime}\mathrel{{\xrightarrow[]{\sigma}}{}^{\prime}}\mu^{\prime})\wedge
w\in\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime}))\\}\subseteq E^{\mathcal{G}}$,

  * •

$\\{((s,F^{2},s^{\prime},\mathchar 45\relax,\mu^{\prime},\mathchar
45\relax,\mathsf{V}),(s,\mathchar
45\relax,s^{\prime},\Delta_{s},\mu^{\prime},w,\mathsf{P}))\wedge
w\in\mathbb{V}(\mathbb{C}(\Delta_{s},\mu^{\prime}))\\}\subseteq
E^{\mathcal{G}}$ for any $F\in\mathcal{F}$,

That is, we restrict the couplings to the vertices of the polytope
$\mathbb{C}(\mu,\mu^{\prime})$. Note that since the set of vertices is finite,
the game $\mathcal{H}_{A,A^{\prime}}$ is finite. We show now that:

$\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{G}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}],$
(3)

and:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{G}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}],$
(4)

Note that, by the property proven above, these are equivalent to:

$\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{G}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}],$
(5)

and:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{G}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}],$
(6)

5 holds since
$\mathit{Post}^{\mathcal{H}_{A,A^{\prime}}}(v)\subseteq\mathit{Post}^{\mathcal{MG}_{A,A^{\prime}}}(v)$
for $v\in V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{V}}$ and
$\mathit{Post}^{\mathcal{H}_{A,A^{\prime}}}(v)=\mathit{Post}^{\mathcal{MG}_{A,A^{\prime}}}(v)$
for $v\in V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{R}}$. For proving 6, fix a
fair strategy $\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}$,
the optimal strategy for the Verifier in game $\mathcal{G}_{A,A^{\prime}}$ is
attained only in probabilistic vertices that are vertices of
$\mathbb{C}(\mu,\mu^{\prime})$, thus the probabilistic vertices of
$\mathcal{H}_{A,A^{\prime}}$, thus
$\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{G}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]\leq\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}],$
for any fair and memoryless $\pi_{\mathsf{R}}$, 6 follows.

Furthermore, the value of game $\mathcal{H}_{A,A^{\prime}}$ is given by the
greatest fixed point of the equations [7]:

$L(f)(v)=\begin{cases}\displaystyle\min\\{\mathsf{u},\chi_{\mathcal{M}}({v}[{1}])+\sum_{v^{\prime}\in\mathit{Post}(v)}\delta(v)(v^{\prime})f(v^{\prime})\\}&\text{
if }v\in V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{P}}\\\
\displaystyle\min\\{\mathsf{u},\max\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{V}},\\\
\displaystyle\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{R}},\\\ \displaystyle 0&\text{ if
}v=v_{\text{err}}.\displaystyle\end{cases}$ (7)

for some
$\mathsf{u}\geq\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}[f_{m}]$.
That is, we have:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v}[f_{m}]=\sup_{\pi_{\mathsf{V}\in\Pi_{\mathsf{V}}^{\mathsf{M}\mathsf{D}}}}\inf_{\pi_{\mathsf{R}\in\Pi_{\mathsf{R}}^{\mathsf{M}\mathsf{D}}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v}[f_{m}]<\infty$
(8)

Thus, because of 5, 6 and 8 we have:

$\inf_{\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}\sup_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]=\sup_{\pi_{\mathsf{V}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}}\inf_{\pi_{\mathsf{R}\in\Pi_{\mathsf{R}}^{\mathsf{M}}}}\mathbb{E}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{MG}_{A,A^{\prime}},v}[f_{m}]<\infty.$

This proves a part of the theorem. Now, consider the following functional over
the symbolic game:

$L^{\prime}(f)(v)=\begin{cases}\displaystyle\min\\{\mathsf{u},\max_{w\in\mathbb{V}(\mathbb{C}({v}[{3}],{v}[{4}]))}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])f(v^{\prime})\\}\\}&\text{
if }v\in V^{\mathcal{SG}_{A,A^{\prime}}}_{\mathsf{P}}\\\
\displaystyle\min\\{\mathsf{u},\max\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}_{A,A^{\prime}}}_{\mathsf{V}},\\\
\displaystyle\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+f(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}&\text{ if }v\in
V^{\mathcal{SG}_{A,A^{\prime}}}_{\mathsf{R}},\\\ \displaystyle 0&\text{ if
}v=v_{\text{err}}.\displaystyle\end{cases}$

we will prove that this can be used to solve $L$. First, note that
$L^{\prime}$ is monotone, it is defined over a complete lattice
$[0,\mathsf{u}]$ and it is Scott-complete. Thus, it has a greatest fixpoint.
Let $\nu L^{\prime}$ the greatest fixpoint, of $L^{\prime},$ we prove that
$\nu L(v)=\nu L^{\prime}((v[0],v[1],v[2],v[3],v[4]))$, for every $v\in
V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{V}}\cup
V^{\mathcal{H}_{A,A^{\prime}}}_{\mathsf{R}}$. For doing so, consider for each
symbolic vertex the following mapping:

  * •

$\llbracket(s,\sigma,s^{\prime},\mu,\mu^{\prime},X)\rrbracket=(s,\sigma,s^{\prime},\mu,\mu^{\prime},\mathchar
45\relax,X)$, for $X\in\\{\mathsf{R},\mathsf{V}\\}$,

  * •

$\llbracket(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},\mathsf{P})\rrbracket=(s,\mathchar
45\relax,s^{\prime},\mu,\mu^{\prime},w,\mathsf{P})$,
where
$w=\operatorname*{argmax}_{w\in\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime}))}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\nu
L^{\prime}(v^{\prime})\\}$

Similarly, we can define a mapping from concrete vertices to symbolic ones as:

  * •

$\llparenthesis(s,\sigma,s^{\prime},\mu,\mu^{\prime},Y,X)\rrparenthesis=(s,\sigma,s^{\prime},\mu,\mu^{\prime},X)$,
for $X\in\\{\mathsf{R},\mathsf{V}$ and $Y\in\\{\mathchar
45\relax\\}\cup\mathbb{V}(\mathbb{C}(\mu,\mu^{\prime},))$.

Now, we prove that $\alpha(v)=\nu L^{\prime}(\llparenthesis v\rrparenthesis)$
is a fixpoint of $L$. We proceed by cases:

If $v$ is a Refuter’s vertex, then:

$\displaystyle L(\alpha)(v)$
$\displaystyle=\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+\alpha(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}$ (9)
$\displaystyle=\min\\{\mathsf{u},\min\\{\chi_{\mathcal{M}}({v}[{1}])+\nu
L^{\prime}(\llparenthesis v^{\prime}\rrparenthesis)\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}$ (10) $\displaystyle=\nu
L^{\prime}(\llparenthesis v\rrparenthesis)$ (11) $\displaystyle=\alpha(v)$
(12)

The first line is by definition of $L$, the second line is obtained applying
the definition of $\alpha$, the third line is due to suryectivity of
$\llparenthesis\rrparenthesis$ and definition of $L^{\prime}$ and the fact
that $\nu L^{\prime}(\llparenthesis v\rrparenthesis)$ is a fixed point of
$L^{\prime}$. If $v$ is a Probabilistic vertex, the proof similar:

$\displaystyle L(\alpha)(v)$
$\displaystyle=\min\\{\mathsf{u},\max_{w\in\mathbb{C}({v}[{3}],{v}[{4}])}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\alpha(v^{\prime})\\}\\}$
(13)
$\displaystyle=\min\\{\mathsf{u},\max_{w\in\mathbb{C}({v}[{3}],{v}[{4}])}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\nu
L^{\prime}(\llparenthesis v^{\prime}\rrparenthesis)\\}\\}$ (14)
$\displaystyle=\nu L^{\prime}(\llparenthesis v\rrparenthesis)$ (15)
$\displaystyle=\alpha(v)$ (16)

If $v$ is a Verifier’s vertex, then:

$\displaystyle L(\alpha)(v)$
$\displaystyle=\min\\{\mathsf{u},\max\\{\chi_{\mathcal{M}}({v}[{1}])+\alpha(v^{\prime})\mid
v^{\prime}\in\mathit{Post}(v)\\}\\}$ (17)
$\displaystyle=\min\\{\mathsf{u},\max_{w\in\mathbb{V}(\mathbb{C}({v}[{3}],{v}[{4}]))}\\{\sum_{v^{\prime}\in\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\nu
L^{\prime}(\llparenthesis v^{\prime}\rrparenthesis)\\}\\}$ (18)
$\displaystyle=\nu L^{\prime}(\llparenthesis v\rrparenthesis)$ (19)
$\displaystyle=\alpha(v)$ (20)

Hence, $\alpha$ is a fixpoint of $L$. Furthermore, we prove that it is
greatest one. Assume for the sake of contradiction that there is some
$\alpha^{\prime}$ such that is a fixpoint of $L$ and
$\alpha^{\prime}(v)\geq\alpha(v)$ for every $v$, and
$\alpha^{\prime}(v^{\prime})>\alpha(v^{\prime})$ for some $v^{\prime}$. We can
define $\beta(v)=\alpha^{\prime}(\llbracket v\rrbracket)$, as above we can
prove that it is a fixpoint of $L^{\prime}$ and, furthermore, for every
symbolic vertex we have $\beta(v)=\alpha^{\prime}(\llbracket
v\rrbracket)\geq\alpha(\llbracket v\rrbracket)=\nu
L^{\prime}(\llparenthesis\llbracket v\rrbracket\rrparenthesis)=\nu
L^{\prime}(v)$, and similarly we can prove that there is a $v^{\prime}$ such
that $\beta(v^{\prime})>\nu L^{\prime}(v)$, which is a contradiction since
$\nu L^{\prime}$ is the greatest fixpoint of $L^{\prime}$.

Proof of Theorem 4.2 Given a masking game $\mathcal{G}_{A,A^{\prime}}$ and its
symbolic version $\mathcal{SG}_{A,A^{\prime}}$, we have that
$\mathcal{G}_{A,A^{\prime}}$ is stopping under fairness iff
$v_{0}^{\mathcal{G}}\in
V^{\mathcal{SG}}\setminus{\exists\mathit{Pre}^{S}_{f}}^{*}(V^{\mathcal{SG}}\setminus{\forall\mathit{Pre}^{S}_{f}}^{*}(v_{\text{err}})),$
where $v_{0}^{\mathcal{G}}$ is the initial state of
$\mathcal{SG}_{A,A^{\prime}}$ and $V^{\mathcal{SG}}$ its sets of vertices.

###### Proof

Consider the game $\mathcal{H}_{A,A^{\prime}}$ as defined in the proof of
Theorem 4.1. First, we prove that the game $\mathcal{G}_{A,A^{\prime}}$ is
almost-sure failing for fair Refuter’s strategies iff
$\mathcal{H}_{A,A^{\prime}}$ is too almost-sure failing for fair Refuter’s
strategies. This is equivalent to prove that
$\inf_{\pi_{\mathsf{V}}}\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{G}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\Diamond
v_{\text{err}})=1$ iff
$\inf_{\pi_{\mathsf{V}}}\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\Diamond
v_{\text{err}})=1$ for every strategy memoryless and fair $\pi_{\mathsf{R}}$.
Now, note we have:

$\displaystyle\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v}(\Diamond
v_{\text{err}})$
$\displaystyle=\min\\{\sum_{v^{\prime}\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}(\Diamond
v_{\text{err}})\mid w\in\mathbb{C}({v}[{3}],{v}[{4}])\\}$
$\displaystyle=\min\\{\sum_{v^{\prime}\mathit{Post}(v)}w({v^{\prime}}[{0}],{v^{\prime}}[{2}])\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v^{\prime}}(\Diamond
v_{\text{err}})\mid w\in\mathbb{V}(\mathbb{C}({v}[{3}],{v}[{4}]))\\}$

Thus, we have a deterministic and memoryless $\pi_{\mathsf{V}}^{\prime}$ such
that:

$\mathit{Prob}^{\pi_{\mathsf{V}}^{\prime},\pi_{\mathsf{R}}}_{\mathcal{G}_{A,A^{\prime}},v}(\Diamond
v_{\text{err}})=\inf_{\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}^{\mathsf{M}}}\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{G}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\Diamond
v_{\text{err}}),$

this strategy only selects probabilistic vertices in
$V^{\mathcal{H}}_{\mathsf{P}}$, and therefore, $\pi_{\mathsf{V}}^{\prime}$ is
a strategy in $\mathcal{H}_{A,A^{\prime}}$. Noting that the Markov chains
$\mathcal{G}^{\pi_{\mathsf{V}}^{\prime},\pi_{\mathsf{R}}}$,$\mathcal{H}^{\pi_{\mathsf{V}}^{\prime},\pi_{\mathsf{R}}}$
are the same for every strategy $\pi_{\mathsf{R}}$, we have:
$\inf_{\pi_{\mathsf{V}}}\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{G}_{A,A^{\prime}},v^{\mathcal{H}}_{0}}(\Diamond
v_{\text{err}})=\inf_{\pi_{\mathsf{V}}}\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H}_{A,A^{\prime}},v_{0}^{\mathcal{G}}}(\Diamond
v_{\text{err}})$.

Now, we prove that we can check wether the game $\mathcal{H}$ is almost-sure
failing under fairness using the symbolic game. We define the following sets
over this game:

$\displaystyle\exists\mathit{Pre}_{f}(C)={}$ $\displaystyle\\{v\in
V^{\mathcal{H}}\mid\exists v^{\prime}\in C:(v,v^{\prime})\in
E^{\mathcal{H}}_{A,A^{\prime}}\\}$
$\displaystyle\forall\mathit{Pre}_{f}(C)={}$ $\displaystyle\\{v\in
V^{\mathcal{H}}_{\mathsf{P}}\mid\delta(v,C)>0\\}$ $\displaystyle\cup\\{v\in
V^{\mathcal{H}}_{\mathsf{V}}\mid\forall
v^{\prime}{\in}V^{\mathcal{H}}:(v,v^{\prime})\in
E^{\mathcal{H}}_{A,A^{\prime}}\Rightarrow v^{\prime}{\in}C\\}$
$\displaystyle\cup\\{v\in V^{\mathcal{H}}_{\mathsf{R}}\mid\exists
v^{\prime}{\in}V^{\mathcal{H}}:(v,v^{\prime})\in
E^{\mathcal{H}}_{A,A^{\prime}}\\}$

As proven in [7] (Theorem 3) we have that:
$\mathit{Prob}^{\pi_{\mathsf{V}},\pi_{\mathsf{R}}}_{\mathcal{H},v}(\Diamond
v_{\text{err}})=1$ for every $\pi_{\mathsf{V}}\in\Pi_{\mathsf{V}}$ and fair
$\pi_{\mathsf{R}}\in\Pi_{\mathsf{R}}$ iff $v\in
V\setminus\exists\mathit{Pre}_{f}^{*}(V\setminus\forall\mathit{Pre}_{f}^{*}(v_{\text{err}}))$.

Now, we prove that for all $v\in V^{\mathcal{H}}$ and $v^{\prime}\in
V^{\mathcal{SG}}$ such that ${v}[{i}]={v^{\prime}}[{i}]$ for $0\leq i\leq 4$,
we have: $v\in\forall\mathit{Pre}_{f}^{n}(v_{\text{err}})$ iff
$v^{\prime}\in{\forall\mathit{Pre}^{S}_{f}}^{n}(v_{\text{err}})$, for every
$n$. The proof is by induction on $n$. The base case is direct. The inductive
cases for Refuter’s nodes and Probabilistic nodes are also direct (as the
predecessors in both games are the same for those vertices module dummy
notation). For Verifier’s nodes we proceed as follows. If
$v\in\forall\mathit{Pre}_{f}^{n}(v_{\text{err}})$, then for all
$t\in\mathit{Post}(v)$ we have
$\delta(t)(\forall\mathit{Pre}_{f}^{n-2}(v_{\text{err}}))>0$, that is,
$\mathit{Eq}(t^{\prime})({\exists\mathit{Pre}^{S}_{f}}^{n-2}(v_{\text{err}}))$
has no solutions (with $t^{\prime}$ satisfying ${t}[{i}]={t^{\prime}}[{i}]$
for $0\leq i\leq n$ ). Thus,
$t^{\prime}\in{\forall\mathit{Pre}^{S}_{f}}^{n-1}(v_{\text{err}})$, and since
$t^{\prime}$ is the unique successor of $v^{\prime}$ we have that
$v^{\prime}\in{\forall\mathit{Pre}^{S}_{f}}^{n}(v_{\text{err}})$, the other
direction is similar.

Now, given sets $C\subseteq V^{\mathcal{H}}$ and $C^{*}\subseteq
V^{\mathcal{G}}$ with $C^{*}=\\{v\mid\exists v^{\prime}\in C:\forall 0\leq
i\leq 4:{v}[{i}]={v^{\prime}}[{i}]\\}$. We prove that, for every $u\in
V^{\mathcal{H}}$ and $u^{\prime}\in V^{\mathcal{SG}}$ such that
${u}[{i}]={u^{\prime}}[{i}]$ for every $0\leq i\leq 4$, we have
$u\in\exists\mathit{Pre}_{f}^{n}(C)$ iff
$u^{\prime}\in\exists\mathit{Pre}_{f}^{n}(C^{*})$. The proof is by induction
on $n$, for $n=0$ it is direct. For $n>0$, assume
$w\in\exists\mathit{Pre}_{f}^{n}(C)$, for Refuter’s (or Verifier’s) vertices
the proof is direct, since in both games they have the same successors (up to
removal of dummy notation). If $u$ is a Probabilistic vertex and
$u\in\exists\mathit{Pre}_{f}^{n}(C)$, then there is $t\in C$ such that
$t\in\mathit{Post}(u)$, that is, ${u}[{5}]({t}[{3}])({t}[{4}])>0$. But then
${t}[{0}]\in\mathit{Supp}({u}[{3}])$ and ${t}[{2}]\in\mathit{Supp}({u}[{4}])$
which implies that $u^{\prime}\in{\exists\mathit{Pre}^{S}_{f}}^{n}(C)$. The
other direction is similar, but noting that if we have
${t}[{0}]\in\mathit{Supp}({u}[{3}])$ and ${t}[{2}]\in\mathit{Supp}({u}[{4}])$,
then we can construct a coupling relating distributions ${u}[{3}]$ and
${u}[{4}]$.

Thus, we have that $v_{0}^{\mathcal{G}}\in
V\setminus\exists\mathit{Pre}_{f}^{*}(V\setminus\forall\mathit{Pre}_{f}^{*}(v_{\text{err}}))$
iff $v_{0}^{\mathcal{G}}\in
V^{\mathcal{SG}}\setminus{\exists\mathit{Pre}^{S}_{f}}^{*}(V^{\mathcal{SG}}\setminus{\forall\mathit{Pre}^{S}_{f}}^{*}(v_{\text{err}}))$,
from there the theorem follows.