and the transitions pointing to $(q,m_{2})$ now point to $(q,m_{1})$. For
this, we show that for all $u\in\mathrm{dom}(R(\mathcal{A}_{q}))$ it holds
that $f_{\mathcal{B}}((q,m_{1}),u)=f_{\mathcal{B}^{\prime}}((q,m_{1}),u)$,
where
$f_{\mathcal{B}^{\prime}}((q,m_{1}),u)=S_{q}(u\otimes\mathcal{B}^{\prime}_{(q,m_{1})}(u))$.
Towards a contradiction, pick a shortest
$u\in\mathrm{dom}(R(\mathcal{A}_{q}))$ such that
$f_{\mathcal{B}}((q,m_{1}),u)>f_{\mathcal{B}^{\prime}}((q,m_{1}),u)$. Let
$\rho$ resp. $\rho^{\prime}$ be the run on the unique $u\otimes v$ resp.
$u\otimes v^{\prime}$ of $\mathcal{B}$ resp. $\mathcal{B}^{\prime}$ such that
$V(\rho)=f_{\mathcal{B}}((q,m_{1}),u)$ and
$V(\rho^{\prime})=f_{\mathcal{B}^{\prime}}((q,m_{1}),u)$. Since
$V(\rho)>V(\rho^{\prime})$, $\rho$ must visit $(q,m_{2})$, thus $\rho$ has a
factorization $\rho_{1}\rho_{2}$ such that the corresponding run of
$\mathcal{B}$ is of the form

$\mathcal{B}\colon\underbrace{(q,m_{1})\xrightarrow{u_{1}|v_{1}}}_{\rho_{1}}\underbrace{(q,m_{2})\xrightarrow{u_{2}|v_{2}}(p,m)}_{\rho_{2}},$

where $u=u_{1}u_{2}$, $v=v_{1}v_{2}$ and $(p,m)$ is a final state of
$\mathcal{B}$, and $\rho_{1}$ does not visit $(q,m_{2})$. By construction of
$\mathcal{B}^{\prime}$, the run $\rho^{\prime}$ is of the form
$\rho_{1}\rho_{2}^{\prime}$ as follows:

$\mathcal{B}^{\prime}\colon\underbrace{(q,m_{1})\xrightarrow{u_{1}|v_{1}}}_{\rho_{1}}\underbrace{(q,m_{1})\xrightarrow{u_{2}|v_{2}^{\prime}}(p^{\prime},m^{\prime})}_{\rho_{2}^{\prime}},$

where $v^{\prime}=v_{1}v_{2}^{\prime}$, and $(p^{\prime},m^{\prime})$ is a
final state of $\mathcal{B}^{\prime}$. The property ($\ast$) implies that
$f_{\mathcal{B}}((q,m_{1}),u_{2})=f_{\mathcal{B}}((q,m_{2}),u_{2})=V(\rho_{2})$.
Since $\mathcal{A}$ is $\leq$-stable, it follows that
$V(\rho_{2})>V(\rho_{2}^{\prime})$. Hence,
$f_{\mathcal{B}}((q,m_{1}),u_{2})>f_{\mathcal{B}^{\prime}}((q,m_{1}),u_{2})$,
which contradicts the assumption that $u$ is a shortest counter-example.

Finally, we show that $\mathcal{B^{\prime}}$ is also a best-value
$S$-realizer. Let $u\in\mathrm{dom}(S)$ and let $f_{\mathcal{B}}(u)$ resp.
$f_{\mathcal{B^{\prime}}}(u)$ be equal to $S(u\otimes\mathcal{B}(u))$ resp.
$S(u\otimes\mathcal{B^{\prime}}(u))$. We show that
$f_{\mathcal{B}}(u)=f_{\mathcal{B^{\prime}}}(u)$. Let $\rho$ be the run of
$\mathcal{A}$ on $(u,\mathcal{B}(u))$, and $\rho^{\prime}$ be the run of
$\mathcal{A}$ on $(u,\mathcal{B^{\prime}}(u))$. If $\rho$ does not visit
$(q,m_{2})$ then $\rho=\rho^{\prime}$ and the claim follows. If $\rho$ visits
$(q,m_{2})$, then $\rho$ and $\rho^{\prime}$ can be decomposed as:

$\mathcal{B}\colon\underbrace{(q_{0},m_{0})\xrightarrow{u_{1}|v_{1}}}_{\rho_{1}}\underbrace{(q,m_{2})\xrightarrow{u_{2}|v_{2}}(p,m)}_{\rho_{2}}\qquad\mathcal{B}^{\prime}\colon\underbrace{(q_{0},m_{0})\xrightarrow{u_{1}|v_{1}}}_{\rho_{1}}\underbrace{(q,m_{1})\xrightarrow{u_{2}|v_{2}^{\prime}}(p^{\prime},m^{\prime})}_{\rho_{2}^{\prime}}.$

By ($\ast$) we have
$f_{\mathcal{B}}((q,m_{1}),u_{2})=f_{\mathcal{B}}((q,m_{2}),u_{2})$ and by the
second property we have shown, we have
$f_{\mathcal{B}}((q,m_{1}),u_{2})=f_{\mathcal{B}^{\prime}}((q,m_{1}),u_{2})$.
In other words, we get $V(\rho_{2})=V(\rho^{\prime}_{2})$, from which we
conclude that $V(\rho_{1}\rho_{2})=V(\rho_{1}\rho^{\prime}_{2})$ (because
$\mathcal{A}$ is $V$-stable), i.e.
$f_{\mathcal{B}}(u)=f_{\mathcal{B^{\prime}}}(u)$. This concludes the proof, as
$\mathcal{B}$ is a best-value $S$-realizer. ∎

As a consequence of the latter lemma, the fact that $V$-specifications are
$\leq$-stable and have decidable inclusion problem [25] for
$V\in\\{\mathsf{Sum},\mathsf{Avg},\mathsf{Dsum}\\}$, we obtain decidability of
the best-value synthesis problem for those measures. While this technique is
general to obtain decidability results, it does not yield optimal
complexities, and in the following theorems, we use other techniques to obtain
better bounds.

####  C.3.2 Proof of Theorem 12 (continued)

See 12

It remains to prove Theorem 12 for $\mathsf{Avg}$\- and
$\mathsf{Dsum}$-specifications. This is done below in two separate theorems,
Theorem 22 and Theorem 23.

####  C.3.3 Proof of Theorem 12: Average

######  Theorem 22.

The best-value synthesis problem for an $\mathsf{Avg}$-specification is
decidable in Ptime.

###### Proof.

The problem reduces to the best-value synthesis problem for
$\mathsf{Sum}$-specifications.

Let $\mathcal{A}$ be a $\mathsf{Avg}$-automaton defining an
$\mathsf{Avg}$-specification $S$, and let $\mathcal{A}_{\mathsf{Sum}}$ be the
same automaton but interpreted as a $\mathsf{Sum}$-automaton defining the
$\mathsf{Sum}$-specification $S_{\mathsf{Sum}}$. We have that
$R(S)=R(S_{\mathsf{Sum}})$.

Let $\mathcal{T}$ be a such that $\mathrm{dom}(T)=\mathrm{dom}(S)$ and
$u\otimes\mathcal{T}(u)\in S$ for all $u\in\mathrm{dom}(S)$. It is easy to see
that $S(u\otimes\mathcal{T}(u))=\mathsf{bestVal}_{S}(u)$ if, and only if,
$S_{\mathsf{Sum}}(u,\mathcal{T}(u))=\mathsf{bestVal}_{S_{\mathsf{Sum}}}(u)$
for all $u\in\mathrm{dom}(S)$, because
$\mathsf{bestVal}_{S_{\mathsf{Sum}}}(u)=\mathsf{bestVal}_{S}(u)|uu|$. ∎

####  C.3.4 Proof of Theorem 12: Discounted-sum

######  Theorem 23.

The best-value synthesis problem for a $\mathsf{Dsum}$-specification is
decidable in NP$\cap$coNP.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{0},\Delta,F,\gamma)$ be a
$\mathsf{Dsum}$-automaton (with discount factor $\lambda$) defining a weighted
specification $S$, for which we want to solve the best-value synthesis
problem. We first give a property that characterizes best-value realizers of
$S$, and then use a game to check this property.

For a state $q\in Q$ we write $\mathsf{bestVal}_{q}$ for the function
$\mathsf{bestVal}_{S_{q}}$, where $S_{q}$ is the weighted specification
defined by $\mathcal{A}$ with initial state $q$. Let $\mathcal{T}$ be a
transducer. Then $\mathcal{T}$ is a best-value realizer of $S$ if, and only
if, the following property is satisfied:

  * $(*)$

Assume an input $u\in\Sigma_{\mathbbmtt{i}}^{*}$, $\mathcal{T}$ has produced
some output $v$, such that $\mathcal{A}$ reaches state $q$ on $u\otimes v$,
and the corresponding transition sequence of $\mathcal{A}$ has discounted-sum
$x$. Then for each $u^{\prime}\in\Sigma_{\mathbbmtt{i}}^{*}$ such that
$uu^{\prime}\in\mathrm{dom}(S)$:

$x+\lambda^{2|u|}\mathsf{bestVal}_{q}(u^{\prime})=\mathsf{bestVal}_{S}(uu^{\prime}).$

We argue that $(*)$ indeed characterizes the best-value realizers of $S$.
Clearly, always
$x+\lambda^{2|u|}\mathsf{bestVal}_{q}(u^{\prime})\leq\mathsf{bestVal}_{S}(uu^{\prime})$
because $x+\lambda^{2|u|}\mathsf{bestVal}_{q}(u^{\prime})$ is a possible value
for $uu^{\prime}$. So if $(*)$ is not satisfied, then there is a $u^{\prime}$
such that $uu^{\prime}\in\mathrm{dom}(S)$, and
$x+\lambda^{2|u|}\mathsf{bestVal}_{q}(u^{\prime})<\mathsf{bestVal}_{S}(uu^{\prime})$.
But then $\mathcal{T}$ cannot produce the best value for input $uu^{\prime}$.
If $(*)$ is satisfied, then for $u\in\mathrm{dom}(S)$, we obtain that
$\mathcal{T}$ produces weight $x=\mathsf{bestVal}(u)$ by choosing
$u^{\prime}=\varepsilon$. This finishes the argument that $(*)$ characterizes
the best-value realizers of $S$.

We now show how to reduce the problem of checking $(*)$ to critical prefix
$\mathsf{Dsum}$ non-strict threshold games in polynomial time, which yields
the claimed complexity by Theorem 16. The idea for the game is the same as for
the game used in the proof of Theorem 2 for the construction of domain-safe
automata: Adam and Eve simultaneously build runs of $\mathcal{A}$, both
starting in the initial state. The weights are chosen such that they give the
difference of the weights of the two runs (run of Eve $-$ run of Adam). Eve’s
goal is to ensure that the difference is $\geq 0$ for inputs that are in the
domain.

In the Boolean case (Theorem 2), the output transitions where chosen in two
moves, first by Eve, then by Adam. For $\mathsf{Dsum}$ this is problematic
because for building the weight difference of the two runs, we have to ensure
to use the right discount factors. Therefore, we modify the game a bit to take
this into account as follows:

  * $\bullet$

In a first part of the game, there is only one run. Adam chooses inputs, and
Eve chooses output transitions. The weights of these moves are 0. This
corresponds to the part where Adam’s run is the same as Eve’s run (and thus
the difference is $0$).

  * $\bullet$

Whenever Eve has chosen an output transition, Adam can either follow this
output transition and pick the next input, staying in the first part of the
game, or choose a different output, branching off another run and going to the
second part of the game (the idea is that Adam chooses this move the first
time Eve would reach a state violating property $(*)$).

  * $\bullet$

In the second part, the game traces two runs. Adam always chooses the input
and his next output at the same time. Then Eve chooses her output. The weights
are the differences between the transitions in the two runs. Since the move to
the second part of the game shifts the number of moves in the game by one
w.r.t. the transitions in the run, the weights have to be corrected, dividing
them by $\lambda$.

Since a best-value realizer of $S$ is also a Boolean realizer of $S$, we also
need to take care of the Boolean condition (the run of Eve is accepting if the
run of Adam is accepting). This could be done by first solving a safety
condition on the game that we build. However, since we have already solved the
Boolean case in Theorem 2, we can use those results.

We now turn to the formal definition of the game. Let $\mathcal{A}^{s}$ with
transitions $\Delta^{s}\subseteq\Delta$ be a domain-safe subautomaton of
$\mathcal{A}$ according to Theorem 2. Let $Q_{\mathbbmtt{i}}$,
$Q_{\mathbbmtt{o}}$ be the partition of the state set of $\mathcal{A}$ into
input and output states, and let
$\Delta_{\mathbbmtt{i}}=\Delta\cap(Q_{\mathbbmtt{i}}\times\Sigma_{\mathbbmtt{i}}\times
Q_{\mathbbmtt{o}})$ and
$\Delta_{\mathbbmtt{o}}=\Delta\cap(Q_{\mathbbmtt{o}}\times\Sigma_{\mathbbmtt{o}}\times
Q_{\mathbbmtt{i}})$ be the transitions starting from an input and output
states, respectively. The transitions that Eve can use are the ones in
$\Delta_{\mathbbmtt{o}}^{s}=\Delta_{\mathbbmtt{o}}\cap\Delta^{s}$.

  * $\bullet$

The vertices of Adam are
$\\{q_{0}\\}\cup\Delta_{\mathbbmtt{o}}^{s}\cup(Q_{\mathbbmtt{i}}\times
Q_{\mathbbmtt{i}})$.

  * $\bullet$

The vertices of Eve are $Q_{\mathbbmtt{o}}\cup(Q_{\mathbbmtt{o}}\times
Q_{\mathbbmtt{o}}\times\Sigma_{\mathbbmtt{o}})$.

  * $\bullet$

The critical vertices are $Q\times F$.

  * $\bullet$

The edges are

    * $\circ$

$q_{0}\rightarrow p$ with weight $0$ for all
$(q_{0},a,p)\in\Delta_{\mathbbmtt{i}}$ (Adam’s very first input)

    * $\circ$

For $p\in Q_{\mathbbmtt{o}}$:
$p\rightarrow(p,b,q)$ with weight $0$ for all
$(p,b,q)\in\Delta_{\mathbbmtt{o}}^{s}$ (Eve’s output in the first part of the
game)

    * $\circ$

For $(p,b,q)\in\Delta_{\mathbbmtt{o}}^{s}$:
$(p,b,q)\rightarrow p^{\prime}$ with weight $0$ for all
$(q,a,p^{\prime})\in\Delta_{\mathbbmtt{i}}$ (Adam follows Eve’s output and
chooses the next input in the first part of the game)

    * $\circ$

For $(p,b,q)\in\Delta_{\mathbbmtt{o}}^{s}$:
$(p,b,q)\rightarrow(q,q^{\prime})$ with weight
$\frac{\gamma(p,b^{\prime},q^{\prime})-\gamma(p,b,q)}{\lambda}$ for each
$(p,b^{\prime},q^{\prime})\in\Delta_{\mathbbmtt{o}}$ (Adam chooses a different
output than Eve, moving to the second part of the game; the length of the game
is now one more than the length of the runs, so the weights are corrected by
$\frac{1}{\lambda}$)

    * $\circ$

For $(q,q^{\prime})\in(Q_{\mathbbmtt{i}}\times Q_{\mathbbmtt{i}})$:
$(q,q^{\prime})\rightarrow(p,p^{\prime},b^{\prime})$ with weight
$\frac{\gamma(q^{\prime},a,p^{\prime})-\gamma(q,a,p)}{\lambda}$ for each
$a\in\Sigma_{\mathbbmtt{i}}$, $b^{\prime}\in\Sigma_{\mathbbmtt{o}}$, and
$(q,a,p),(q^{\prime},a,p^{\prime})\in\Delta_{\mathbbmtt{i}}$ (Adam chooses
next input and his next output in the second part of the game)

    * $\circ$

For $(p,p^{\prime},b^{\prime})\in Q_{\mathbbmtt{o}}\times
Q_{\mathbbmtt{o}}\times\Sigma_{\mathbbmtt{o}}$:
$(p,p^{\prime},b^{\prime})\rightarrow(q,q^{\prime})$ with weight
$\frac{\gamma(p^{\prime},b^{\prime},q^{\prime})-\gamma(p,b,q)}{\lambda}$ for
each $b\in\Sigma_{\mathbbmtt{o}}$ with $(p,b,q)\in\Delta_{\mathbbmtt{o}}^{s}$,
and $(p^{\prime},b^{\prime},q^{\prime})\in\Delta_{\mathbbmtt{o}}$ (Eve chooses
her next output in the second part of the game).

We claim that Eve has a winning strategy in this critical prefix
$\mathsf{Dsum}$ game with threshold $\geq 0$ iff there is a best-value
realizer of $S$.

We view the first part of the game as Adam playing the same outputs as Eve.
With this view, any play ending in a vertex of Adam corresponds to an input
word $u$, two output words $v,v^{\prime}$ of the same length as $u$, a run of
$\mathcal{A}^{s}$ on $u\otimes v$, and a run of $\mathcal{A}$ on $u\otimes
v^{\prime}$. The weight of such a play is the difference of the weights of
these two runs, which can easily be shown by induction on the length of the
play.

If there is a best-value realizer of $S$, then it only uses transition of
$\mathcal{A}^{s}$ (see Theorem 2). Eve can play her moves according to this
realizer, ensuring that her run produces the best value for each input in the
domain of $S$. Hence, the weight of plays ending in $Q\times F$ is $\geq 0$.

Now assume that Eve has a winning strategy $\sigma$ in the game, which can be
assumed to be positional by Theorem 18.

On the first part of the game, this strategy corresponds to a transducer
$\mathcal{T}_{\sigma}$. We show that $\mathcal{T}_{\sigma}$ satisfies property
$(*)$. Assume that $\mathcal{T}_{\sigma}$ violates $(*)$, and pick a shortest
word $u$ for which $(*)$ is not satisfied. Let $v$ be the output produced by
$\mathcal{T}_{\sigma}$, and $x$, $q$ as in $(*)$.

If $u=v=\varepsilon$, then $x=0$ and $q=q_{0}$, and thus the equation from
$(*)$ is satisfied. Hence, $u=a_{1}\cdots a_{n}$ and $v=b_{1}\cdots b_{n}$
with $n\geq 1$. Consider the corresponding play $\pi$ in the first part of the
game, which is of this form (where the $a_{i}$ are not part of the game but
are added for readability):

$\pi=q_{0}\xrightarrow{a_{1}}p_{1}\rightarrow(p_{1},b_{1},q_{1})\xrightarrow{a_{2}}p_{2}\rightarrow\cdots\rightarrow
q_{n-1}\xrightarrow{a_{n}}p_{n}\rightarrow(p_{n},b_{n},q_{n})$

with $q=q_{n}$. Let $u^{\prime}=a_{n+1}\cdots a_{n+m}$ be a witness that $(*)$
is violated, i.e., such that

$x+\lambda^{2|u|}\mathsf{bestVal}_{q}(u^{\prime})<\mathsf{bestVal}_{S}(uu^{\prime}).$

We can conclude that for all $b_{n+1}\cdots b_{n+m}$:

$\mathcal{A}(a_{1}b_{1}\cdots
a_{n+m}b_{n+m})<\mathsf{bestVal}_{S}(uu^{\prime}).\hfill(1)$

Since $u$ was chosen as shortest word, property $(*)$ is satisfied for
$w=a_{1}\cdots a_{n-1}$, $q_{n-1}$, and the weight
$y=\mathcal{A}(a_{1}b_{1}\cdots a_{n-1}b_{n-1})$, i.e.,

$y+\lambda^{2|w|}\mathsf{bestVal}_{q_{n-1}}(a_{n}u^{\prime})=\mathsf{bestVal}_{S}(wa_{n}u^{\prime})=\mathsf{bestVal}_{S}(uu^{\prime}).$

So there are $b_{n}^{\prime}b_{n+1}^{\prime}\cdots b_{n+m}^{\prime}$ such that

$\mathcal{A}(a_{1}b_{1}\cdots
a_{n-1}b_{n-1}a_{n}b_{n}^{\prime}a_{n+1}b_{n+1}^{\prime}\cdots
a_{n+m}b_{n+m}^{\prime})=\mathsf{bestVal}_{S}(uu^{\prime}).\hfill(2)$

This means that Adam can continue the play $\pi$ by first playing
$b_{n}^{\prime}$, taking the play into a configuration
$(q_{n},q_{n}^{\prime})$ in the second part of the game, and then playing
$a_{n+1}b_{n+1}^{\prime}\cdots a_{n+m}b_{n+m}^{\prime}$, reaching a critical
vertex. For all responses of Eve (corresponding to some outputs $b_{n+1}\cdots
b_{n+m}$), the value reached at the end of the play is $<0$ because of $(1)$
and $(2)$.

∎

###  C.4 Approximate synthesis

See 13

blub

We split the proof into several theorems. First, we prove the theorem for sum,
see Theorem 24. Then, we prove the theorem for average, see Theorem 25 for
decidability and Theorem 26 for hardness. Finally, we prove the theorem for
discounted-sum, see Theorem 27.

####  C.4.1 Proof of Theorem 13: Sum

######  Theorem 24.

The approximate synthesis problem for a $\mathsf{Sum}$-specification and a
strict or non-strict threshold is decidable. The problem is EXPtime-complete.

###### Proof.

The approximate synthesis problem for a $\mathsf{Sum}$-specification reduces
to the regret determinization problem for nondeterministic
$\mathsf{Sum}$-automata, see Lemma 10. The latter problem was shown to be
EXPtime-complete in [26], so we obtain EXPtime-membership. We obtain EXPtime-
hardness by Lemma 21. ∎

####  C.4.2 Proof of Theorem 13: Average

######  Theorem 25.

The approximate synthesis problem for an $\mathsf{Avg}$-specification and a
strict or non-strict threshold is decidable.

###### Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{i},\Delta,F,\gamma)$ be a complete
$\mathsf{Avg}$-automaton defining an $\mathsf{Avg}$-specification $S$. We
assume that $S$ has a non-empty domain, otherwise we can directly conclude
that the specification is realizable. Since $\mathcal{A}$ alternatively reads
input and output symbols, we assume that the set of states is partitioned into
a set of input states $Q_{\mathbbmtt{i}}$ from which only input symbols are
read, and set of output states $Q_{\mathbbmtt{o}}$. Note that $q_{i}\in
Q_{\mathbbmtt{i}}$.

Given a non-strict threshold $r$, the goal is to decide whether there exists a
transducer $\mathcal{T}$ such that $\mathrm{dom}(\mathcal{T})=\mathrm{dom}(S)$
and $S(u\otimes\mathcal{T}(u))\geq\mathsf{bestVal}_{S}(u)-r$ for all
$u\in\mathrm{dom}(S)$. The latter is equivalent to
$S(u\otimes\mathcal{T}(u))|u\mathcal{T}(u)|-\mathsf{bestVal}_{S}(u)|u\mathcal{T}(u)|+|u\mathcal{T}(u)|r\geq
0$. Let $\rho$ be the unique run of $\mathcal{A}$ on $u\otimes v$, let
$v^{\prime}$ be such that $S(u\otimes v^{\prime})=\mathsf{bestVal}_{S}(u)$,
and let $\rho^{\prime}$ be the unique run of $\mathcal{A}$ on $u\otimes
v^{\prime}$. We can express the above equation as
$\mathsf{Sum}(\rho)-\mathsf{Sum}(\rho^{\prime})+|\rho|r\geq 0$. With this
formulation in mind, we are ready to present a decision method.

We reduce the problem to deciding whether Eve has an observation-based winning
strategy in a critical prefix energy game with imperfect information with
initial credit zero, in which for all states of the game, Adam has a strategy
to enforce a visit to a critical state. Such games are decidable according to
Theorem 8. Intuitively in the game, Adam constructs a run $\rho$ of
$\mathcal{A}$ but Eve only sees the input word $u$ of $\rho$ and not the
output word nor its states, using imperfect information. Eve also constructs a
run $\rho^{\prime}$ of $\mathcal{A}$ on input $u$. The weights are defined so
as to maintain the invariant property that the energy level is
$\mathsf{Sum}(\rho^{\prime})-\mathsf{Sum}(\rho)+|\rho|r$. Moreover, the
construction makes sure that Adam has always a strategy to reach an accepting
state, i.e., that the run $\rho$, if non-accepting, can be continued into an
accepting run. To do so, Adam’s actions are restricted to those which maintain
this invariant.

Let us now describe the construction formally. Consider $Q^{trim}\subseteq Q$
the subset of states which are both reachable from the initial state and from
which an accepting state can be reached. Let
$Q^{trim}_{\mathbbmtt{i}}=Q^{trim}\cap Q_{\mathbbmtt{i}}$ and
$Q^{trim}_{\mathbbmtt{o}}=Q^{trim}\cap Q_{\mathbbmtt{o}}$. Note that $q_{i}\in
Q^{trim}_{\mathbbmtt{i}}$ since we assume that
$\mathrm{dom}(S)\neq\varnothing$, and $F\subseteq Q^{trim}_{\mathbbmtt{i}}$,
since accepted words end with an output symbol.

The game arena $G$ has the set of vertices $(Q_{\mathbbmtt{i}}\times
Q_{\mathbbmtt{i}}^{trim})\ \cup\ (Q_{\mathbbmtt{o}}\times
Q^{trim}_{\mathbbmtt{o}}\times\Sigma_{\mathbbmtt{i}})\ \cup\ \\{q_{\bot}\\}$,
and the set of available actions are
$\Sigma_{\mathbbmtt{o}}\cup\\{\mathit{choose}\\}$. The arena contains the
following edges

  * $\bullet$

$(p,q)$ to $(\delta(p,a),\delta(q,a),a)$ with action $\mathit{choose}$ and
weight $\gamma(\delta(p,a))-\gamma(\delta(q,a))+r$ for all $p,q\in Q$ and
$a\in\Sigma_{\mathbbmtt{i}}$ such that $\delta(q,a)\in
Q^{trim}_{\mathbbmtt{o}}$.  _This edge indicates that Adam chooses the input
symbol $a$._

  * $\bullet$

$(p,q,a)$ to $(\delta(p,b),\delta(q,b^{\prime}))$ with action $b$ and weight
$\gamma(\delta(p,b))-\gamma(\delta(q,b^{\prime}))+r$ for all $p,q\in Q$,
$a\in\Sigma_{\mathbbmtt{i}}$ and $b,b^{\prime}\in\Sigma_{\mathbbmtt{o}}$ such
that $\delta(q,b^{\prime})\in Q^{trim}_{\mathbbmtt{i}}$.  _This edge indicates
that Eve chooses the output symbol $b$ and Adam chooses $b^{\prime}$ instead._

  * $\bullet$

$(p,q)$ to $q_{\bot}$ with action $\mathit{choose}$ and weight zero for all
$p\in Q\setminus F$ and $q\in F$  _This edge indicates that Adam has completed
a valid input word, but Eve was not able to produce a valid output word._

  * $\bullet$

$q_{\bot}$ to $q_{\bot}$ with action $\mathit{choose}$ and weight $-1$  _This
is a sink state used to bring the energy level below zero._

  * $\bullet$

$(p,q)$ to $(p,q)$ with action $\mathit{choose}$ and weight $0$.  _This is to
make the arena deadlock-free._

Note that the arena is deadlock free thanks to the loop on states $(p,q)$ and
for states of the form $(p,q,a)$, there always exist $b,b^{\prime}$ such that
$\delta(p,b)$ is defined (because $\mathcal{A}$ is complete) and
$\delta(p,b^{\prime})\in Q_{\mathbbmtt{i}}^{trim}$ since $q\in
Q_{\mathbbmtt{o}}^{trim}$ and $F\subseteq Q_{\mathbbmtt{i}}^{trim}$.

The observation of a vertex of the form $(p,q)$ is $p$, of the form $(p,q,a)$
is $(p,a)$ and of $q_{\bot}$ is $q_{\bot}$. The set of critical vertices
contains all vertices of the form $(p,q)$ with $q\in F$ and $q_{\bot}$. The
initial vertex is $(q_{i},q_{i})$.

First, let us show that Adam, from any vertex of the game, has a strategy to
reach a critical vertex, an assumption required to apply Theorem 8. Let
consider a non-critical vertex of the form $(p,q)$ or of the form $(p,q,a)$
such that $q\not\in F$. Since $q\in Q^{trim}$, Adam can, in the game,
construct a run (correspond to the second components of the vertices) to an
accepting state of $\mathcal{A}$, leading in the game to a critical vertex.

Second, we show that Eve has an observation-based winning strategy in the
constructed energy game with imperfect information with initial credit zero,
if, and only if, there exists a transducer $\mathcal{T}$ such that
$\mathrm{dom}(\mathcal{T})=\mathrm{dom}(S)$ and for all $u\in\mathrm{dom}(S)$,
$S(u\otimes\mathcal{T}(u))\geq\mathsf{bestVal}_{S}(u)-r$.

Assume that Eve has an observation-based winning strategy with initial credit
zero. Let $\sigma$ be a finite-memory observation-based winning strategy, as
is guaranteed to exist by Theorem 8. The strategy can be translated into a
transducer $\mathcal{T}_{\sigma}$. Indeed, a finite-memory observation-based
strategy is of type $M\times
O\rightarrow(\mathit{choose}\cup\Sigma_{\mathbbmtt{o}})\times M$, where $M$ is
a finite set of memory states and $\mathcal{O}$ is the set of observations of
the game. Note that there, an observation $O$ is either a pair $(p,a)$, a
single state $p$ or $q_{\bot}$. Since $\sigma$ is winning and $q_{\bot}$ is
losing, $q_{\bot}$ is never reached. Initially, the transducer is in state
$(q_{i},m_{0})$ where $m_{0}$ is the initial memory state of $\sigma$. The
states of $\mathcal{T}_{\sigma}$ are pairs $(p,m)$. Let
$a\in\Sigma_{\mathbbmtt{i}}$ be some input symbol and assume that Eve gets
observation $(p^{\prime}=\delta(p,a),a)$. From this observation, we get the
pair $\sigma(m,(p^{\prime},a))=(b,m^{\prime})$ meaning that she plays $b$ and
the memory is updated to $m^{\prime}$. Then, she can only observes that she is
in $p^{\prime}\in Q_{\mathbbmtt{i}}$ and her only possible action is
$\mathit{choose}$. Let $m^{\prime\prime}$ such that
$\sigma(m^{\prime},p^{\prime})=(\mathit{choose},m^{\prime\prime})$. From state
$(p,m)$ and input $a$, $\mathcal{T}_{\sigma}$ outputs $b$ and moves to state
$(\delta(p^{\prime},b),m^{\prime})$. The accepting states of
$\mathcal{T}_{\sigma}$ are pairs $(p,m)$ such that $p\in F$.

We show that $\mathcal{T}_{\sigma}$ implements an $r$-approximate
$S$-realization. From the construction of the game graph it is clear that
$R(\mathcal{T}_{\sigma})\subseteq R(S)$, since any accepting run of
$\mathcal{T}_{\sigma}$ can be translated back to an accepting run of
$\mathcal{A}$. We prove that their domains are equivalent. Towards a
contradiction assume otherwise. Then there exists some input word
$u=u_{1}\dots u_{n}\in\mathrm{dom}(S)$ such that
$u\notin\mathrm{dom}(\mathcal{T}_{\sigma})$. We pick some $v=v_{1}\dots v_{n}$
such that $u\otimes v\in S$. Consider the play $\pi$ according to $\sigma$
where Adam chooses the edges that correspond to input $u$ and output $v$,
eventually the play reaches the vertex $(p,q)=(\delta(u_{1}v^{\prime}_{1}\dots
u_{n}v^{\prime}_{n}),\delta(u_{1}v_{1}\dots u_{n}v_{n}))$. Since $u\otimes
v\in S$ we have $q\in F$ and since $u\not\in\mathrm{dom}(T_{\sigma})$,
$p\notin F$, because by construction of $\mathcal{T}_{\sigma}$, the projection
of $\pi$ on its first component corresponds to a run of
$\mathcal{T}_{\sigma}$. Then, Adam can move to $q_{\bot}$ and bring the energy
level below zero. Since $q_{\bot}$ is a critical vertex, Eve loses. This
contradicts that $\sigma$ is winning.

It is left to show that for all $u\in\mathrm{dom}(S)$ holds that
$S(u\otimes\mathcal{T}_{\sigma}(u))\geq\mathsf{bestVal}_{S}(u)-r$. Towards a
contradiction assume
$S(u\otimes\mathcal{T}_{\sigma}(u))<\mathsf{bestVal}_{S}(u)-r$. Let $v$ be an
output word such that $u\otimes v\in S$ and $S(u\otimes
v)=\mathsf{bestVal}_{S}(u)$. Let $\rho$ and $\rho^{\prime}$ be the unique runs
of $\mathcal{A}$ on $u\otimes v$ and $u\otimes\mathcal{T}_{\sigma}(u)$,
respectively. Now, we consider the play $\pi$ in $G$, where Eve plays
according to $\sigma$ and Adam makes his choices such that they correspond to
the input word $u$ and the run $\rho$. Eve does not observe $\rho$. Eve
choices of actions spell the run $\rho^{\prime}$. By construction of the game
graph, the play ends up in a critical vertex, say after $i$ steps, because
$u\in\mathrm{dom}(S)$. Furthermore, the energy level of the play prefix is
$\mathsf{EL}(\pi(i))=\mathsf{Sum}(\rho^{\prime})-\mathsf{Sum}(\rho)+r|\rho|$.
Since
$S(u\otimes\mathcal{T}_{\sigma}(u))=\frac{\mathsf{Sum}(\rho^{\prime})}{|\rho|}$
and $S(u\otimes v)=\frac{\mathsf{Sum}(\rho)}{|\rho|}=\mathsf{bestVal}_{S}(u)$,
it follows from $S(u\otimes\mathcal{T}_{\sigma}(u))<\mathsf{bestVal}_{S}(u)-r$
that $\mathsf{Sum}(\rho^{\prime})+r|\rho|<\mathsf{Sum}(\rho)$. Thus,
$\mathsf{EL}(\pi(i))<0$, which contradicts that $\sigma$ is an observation-
based winning strategy with initial credit zero.

For the other direction, assume that $\mathcal{T}$ is an $S$-realizer which
non-strictly $r$-approximates $S$. The transducer $\mathcal{T}$ can be
directly translated into an observation-based finite-state strategy
$\sigma_{\mathcal{T}}$ for Eve as follows. Let $M$ be the states of
$\mathcal{T}$ with initial state $m_{0}$. The states of $\sigma_{\mathcal{T}}$
are $M\times\\{\mathbbmtt{i},\mathbbmtt{o}\\}$, with initial state
$(m_{0},\mathbbmtt{i})$. In state $(m,\mathbbmtt{i})$ and for an observation
$(p,a)$, $\sigma_{\mathcal{T}}$ picks action $b$ such that there exists a
transition $(m,a,b,m^{\prime})$ in $T$, and the strategy moves to state
$m^{\prime}$. From a state $(m,\mathbbmtt{o})$ and for an observation $p$, Eve
can only pick action $\mathit{choose}$ and the strategy moves to state
$(m,\mathbbmtt{i})$.

We show that $\sigma_{\mathcal{T}}$ is winning with initial credit zero.
Clearly, plays according to $\sigma_{\mathcal{T}}$ never reach the critical
vertex $q_{\bot}$. We prove that in the energy level in every other critical
vertex that is reached is not below zero. Consider some play $\pi$ according
to $\sigma_{\mathcal{T}}$ and assume $\mathsf{last}(\pi(i))\in C$ for some $i$
and assume $\pi(i)$ describes some input word $u$. Eve has made choices such
that she picks the run $\rho^{\prime}$ of $\mathcal{A}$ on the pair
$(u,\mathcal{T}(u))$. Let $\rho$ denote the alternative run that Adam has
picked which corresponds to some pair $(u,v)$. We have that
$\frac{\mathsf{Sum}(\rho)}{|\rho|}\leq\mathsf{bestVal}_{S}(u)$. Since
$\mathcal{T}$ is an $r$-approximate $S$-realizer, we know that
$\frac{\mathsf{Sum}(\rho^{\prime})}{|\rho^{\prime}|}+r\geq\mathsf{bestVal}_{S}(u)$.
Thus,
$\mathsf{EL}(\pi(i))=\mathsf{Sum}(\rho^{\prime})-\mathsf{Sum}(\rho)+r|\rho|\geq
0$, since $|\rho|=|\rho^{\prime}|$.

Given a strict threshold $r$, we show that the problem reduces to deciding if
Eve has an observation based winning strategy in a slightly different energy
game with imperfect information with initial credit zero. For all $u,v$ holds
that $S(u\otimes v)>\mathsf{bestVal}_{S}(u)-r$ implies that $S(u\otimes
v)|uv|\geq\mathsf{bestVal}_{S}(u)|uv|-r|uv|+1\Leftrightarrow S(u\otimes
v)|uv|-\mathsf{bestVal}_{S}(u)|uv|+r|uv|-1\geq 0$, because $\mathcal{A}$ has
weights in $\mathbbm{Z}$. Thus, it easy to see that it suffices to subtract
one from the weights of the edges outgoing of the initial state. ∎

####  C.4.3 Proof of Theorem 13: Average (lower bound)

######  Theorem 26.

The approximate synthesis problem for an $\mathsf{Avg}$-specification and a
strict or non-strict threshold is EXPtime-hard.

###### Proof.

We provide a reduction from countdown games. A countdown game is a weighted
game with weights over $\mathbbm{N}\setminus\\{0\\}$ with perfect information
in which the actions of a transition are equal to their weight. In this
setting an action is called duration and the sum value of a play prefix is
called counter value. The countdown objective is parameterized by a bound
$N\in\mathbbm{N}$ and is given by
$\mathsf{Count}_{G}(N)=\\{\pi\in\mathsf{Plays}(G)\mid\exists
i\in\mathbbm{N}:\mathsf{Sum}(\pi(i))=N\\}$. Deciding whether Eve has a winning
strategy for the objective $\mathsf{Count}_{G}(N)$, where $N$ and all
durations are given in binary, is EXPtime-complete [31].

Note that Adam has clearly won a play if it is currently in a vertex $s$ and
the counter value is $c<N$ such that for all $\tau=(s,d,s^{\prime})\in T$
holds that $c+d>N$. Let $n=\lfloor\mathrm{log}_{2}N\rfloor+2$, let
$D\subseteq\mathbbm{N}$ be the set of durations used in the counter game.

We first consider the strict case. We design an $\mathsf{Avg}$-automaton
$\mathcal{A}$ defining a weighted specification $S$ such that there exists a
$\mathcal{T}$ that implements a strictly $1$-approximate $S$-realization if,
and only if, Eve has a winning strategy in the countdown game. Recall,
strictly $1$-approximate means that
$S(u\otimes\mathcal{T}(u))>\mathsf{bestVal}_{S}(u)-1$ for all
$u\in\mathrm{dom}(S)$.

$q_{in}$$q_{n}$$q_{y}$$v_{in}$Game
part$q_{1,\square}$$q_{fin}$$q_{0,\square}$$q_{fin}$$\overline{x_{0}}$$\overline{x_{1}}$$\overline{x_{2}}$$\dots$$\overline{x_{n}}$${x_{0}}$${x_{1}}$${x_{2}}$$\dots$${x_{n}}$$\hat{q_{1}}$$\hat{q_{1}}$$\hat{q_{1}}$$\hat{q_{1}}$$\hat{q_{1}}$Counter
part$q_{1}$$q_{\blacktriangleright}$$q_{0}$$\hat{q_{0}}$$\hat{q_{1}}$$\mathbbmtt{i}|1$$n|1$$y|\\!-\\!1$$\square|\\!-\\!3$$\square|4$$\square|1$$\square|0$$\mathbbmtt{i}|1$$\mathbbmtt{i}|0$$\mathbbmtt{o}|0$$\mathbbmtt{i}|0$$0|1$$1|1$$2|1$$n|1$$\mathbbmtt{i}|0$$\mathbbmtt{o}|0$$\mathbbmtt{i}|1$$\mathbbmtt{o}|1$$\blacktriangleright|0$$\blacktriangleright|1$$\blacktriangleright|1$$\blacktriangleright|0$$\blacktriangleright|1$$\blacktriangleright|0$$\blacktriangleright|1$$\square|1$$\mathbbmtt{i}|1$$\textit{counting
error
}\\!|1$$\square|0$$\blacktriangleright|0$$\square|0$$\blacktriangleright|0$$\square|0$$\textit{input
error }\\!|1$ Figure 1: Overview of the automaton. The initial part is
designed to force a strictly $1$-approximate realization to be in the game
part (if it exists). The counter part is always entered with average one, and
all transitions in the counter part have weight one. Each bit of the counter
has its own gadget. The counter part is exited with weight one when either the
$n$th bit is flipped to one, or a counting error occurred, or after seeing the
input $\blacktriangleright$ where the counter bits do not correspond to the
bits of $N$, $N$ is the counter value to be reached in the counter game. This
figure shows the example where $N$ corresponds to the little-endian bit
sequence $011$. The counter part is exited with weight zero when either the
end input $\square$ is seen, or after seeing the input $\blacktriangleright$
where the counter bits correspond to the bits of $N$. These transitions are
shown in blue. The game part is always entered with average zero. All
transitions in the game part have weight zero. The game part is exited with
weight zero when either the end input $\square$ is seen, or the output
$\blacktriangleright$ is seen. The next input then has to be
$\blacktriangleright$. The output $\blacktriangleright$ is intended to be
taken when the counter value is $N$. The game part is exited with weight one
if the input has an error, meaning input does not simulate the game play
correctly. This transition is shown in blue.

The idea behind the automaton is as follows, see Fig. 1 for an overview. The
automaton has three parts, the initial part, the game part and the counter
part.

The initial part is used to force a strictly $1$-approximate $S$-realization
to be in the game part, if there exists one. This is done as follows. Consider
the input $\sigma\square\in\mathrm{dom}(S)$, $\sigma$ is any input symbol. The
possible output combinations are $n\square$ and $y\square$, with
$S(\sigma\square\otimes n\square)=0$ and $S(\sigma\square\otimes y\square)=1$.
Since the difference is one, the first output must be $y$ in a sequential
transducer in order to be a strictly $1$-approximate $S$-realizer.

The remainder of the automaton is split into two parts, one part – the game
part – is used to simulate the moves of Eve and Adam in the counter game, the
other part – the counter part – is used to represent the binary encoding of
the current sum of durations. It suffices to use an $n$-bit counter, because
if the $n$th bit is one, the counter represents a value of at least $2^{n}>N$.
If the counter has reached this value without seeing $N$, it is no longer
possible to reach the counter value $N$ required for Eve to win the game. In
the counter part each bit is represented by its own gadget.

We give a brief overview of the weights in these parts and their functions.
The game part is always reached with current value zero, the counter part with
value one. The value of a run while in the game part remains zero, and while
in the counter part remains one. In the end, given a transducer $\mathcal{T}$,
for a given input sequence $u\in\mathrm{dom}(S)$, we compare the run that was
induced by the produced output sequence $\mathcal{T}(u)$ to all other runs
that could be induced with the same input sequence $u$ and different output
sequences $v$ such that $u\otimes v\in S$. For $\mathcal{T}$ to be a strictly
$1$-approximate $S$-realizer, we require that the difference between
$S(u\otimes\mathcal{T}(u))$ and $S(u\otimes v)$ is less than one for all $v$
such that $u\otimes v\in S$. The goal is that runs can exit the counter part
(triggered by the special output $\blacktriangleright$ in the game part,
explained in detail further below) with a value slightly less than one when
the counter value represents $N$ (the input sequence can continue after the
exit). Also, if the counter represents a value less or equal to $N$ and the
input sequence ends, then the counter part is exited with a value slightly
less than one. In Fig. 1 these transitions correspond to the transitions
exiting the counter part which are shown in blue. Runs exit the counter part
with value exactly one if either the $n$th bit has flipped to one, which
indicates that the value $N$ has been surpassed, or if an error in updating
the counter has been observed. Moreover, if exiting the counter part was
triggered by the special output $\blacktriangleright$ in the game part, then
it should not be beneficial if the counter value is not exactly $N$. Thus, in
these cases the counter part is exited maintaining value one. The game part is
always exited with value zero, unless the exit was caused by an error in the
input sequence, then the value is above zero. The input errors are symbolized
by the blue transition exiting the game part in Fig. 1. These properties
ensure that the difference between compared runs in these two parts will
always be less than one if, and only if, Eve has a winning strategy in the
counter game that is copied by a transducer.

We are ready to go into more detail. First, we give the alphabet explicitly,
the other components are given implicitly by describing the structure of the
automaton.

The alphabet $\Sigma$ is the union of the following sets: the set
$\\{0,\dots,n\\}$, the number $i$ is used as output to lead the run into the
gadget for the $i$th bit of the counter; the set of vertices $V$, vertices are
used as input to choose the successor of a transition; the set of durations
$D$, durations are used as output to choose a duration; $\\{b_{i}\mid 0\leq
i\leq n\\}$ and $\\{c_{i}\mid 1\leq i\leq n\\}$ are used as input, each
$b_{i}$ is used to indicate that the $i$th bit is one, each $c_{i}$ is used to
indicate that the $i$th carry bit in an addition is one; $\\{y,n\\}$, for yes
and no, are used as output to indicate whether the next input should set a
carry bit or not; $\\{\diamond\\}$, $\diamond$ is used as input for carry bits
that remain zero; finally, $\\{\blacktriangleright,\square\\}$, these two
symbols are used as both input and output, $\blacktriangleright$ to force the
runs into special states and $\square$ to end input and output. Let
$\Sigma_{\mathbbmtt{i}}$ and $\Sigma_{\mathbbmtt{o}}$ denote the subset that
is used as input and output, respectively.

We use the symbol $\mathbbmtt{i}$ resp. $\mathbbmtt{o}$ to denote any input
resp. output symbol that is not $\blacktriangleright$ or $\square$.
Furthermore, when depicting (parts of) the automaton, we allow to label
transitions with two symbols, one input and one output symbol, e.g.,
$(p,b_{1}\mathbbmtt{o},q)$ is used a shorthand for $(p,b_{1},r)$ and
$(r,\mathbbmtt{o},q)$ that uses an intermediate state which is not shown to
make the depictions more readable.

The automaton has special states, $q_{0}$, $\hat{q_{0}}$, $q_{0,\square}$,
$q_{1}$, $\hat{q_{1}}$ $q_{1,\square}$, $q_{\mathit{f}in}$, and
$q_{\blacktriangleright}$, see Fig. 1. The state $q_{fin}$ is a deadlock and
the only final state of the automaton. From $q_{i}$, reading one input (except
$\square$) and one output symbol leads back to $q_{i}$ via $\hat{q_{i}}$ with
sum $i+i$ for $i=0,1$. From $q_{i}$, reading $\square$ leads to
$q_{i,\square}$ with weight $i$, and from $q_{i,\square}$, reading $\square$
leads to $q_{\mathit{f}in}$ with weight $i$ for $i=0,1$. The purpose of
$q_{\blacktriangleright}$ is explained further below in the paragraphs that
describe the game part.

We describe the counter part. Each transition with source and target in this
part has weight one. For each bit of the counter there is one gadget, see Fig.
2. The counter part is designed to update the counter based on the durations
seen in the game part of the automaton, the addition of bits and carry bits is
done in the order $b_{0}c_{1}b_{1}\dots b_{n}c_{n}$, see the description of
the game part. The outputs play no role in the bit gadgets, the targets of
transitions are determined by the input. We explain the gadget for the $i$th
bit. The design is such that a run that is in state $\overline{x}_{i}$ resp.
$x_{i}$ indicates that the $i$th bit of the counter is currently zero resp.
one. In $\overline{x}_{i}$, adding a bit or a carry bit (indicated by reading
$b_{i}$ resp. $c_{i}$) flips the counter, so $x_{i}$ is reached. In
$\overline{x}_{i}$, reading $c_{i+1}$ leads to $\hat{q_{1}}$ with weight one,
because adding something to the $i$th bit of the counter while it is zero
cannot set the $i+1$th carry bit to one. In Fig. 1 this transition (among
others) is symbolized by the transition with label _counting error_. Taking
this transition ensures that the value of the run can not go below one
anymore. In $x_{i}$, adding a bit or a carry bit (indicated by reading $b_{i}$
resp. $c_{i}$) flips the counter, however, $c_{i+1}$ has to be read
eventually, because this operation sets the $i+1$th carry bit to one. In Fig.
2 the unnamed states represent states where the counter waists to see
$c_{i+1}$, if as input some vertex $v\in V$ is seen, we know the addition of a
duration to the counter is finished, because input has chosen a successor
vertex. Thus, the necessary carry bit was not seen and an error was detected,
so seeing $v\in V$ leads to $\hat{q_{1}}$. If the first waiting state was
reached with $c_{i}$ the input $b_{i}$ might be seen before $c_{i+1}$, that is
why there is the second waiting state. Reading $c_{i+1}$ directly from $x_{i}$
leads to $q_{1}$ with weight one, because this would indicate that the $i+1$th
carry bit was set without adding something to the $i$th bit of the counter
which is an error.

Regarding the $n$th bit, from $x_{n}$ everything goes to $\hat{q_{1}}$ with
weight one, because this means the counter has surpassed the value $N$, see
Fig. 1.

As mentioned above, in the game part, output can trigger to stop the game by
the output symbol $\blacktriangleright$, then input has to answer with
$\blacktriangleright$ as input; seeing the input $\blacktriangleright$ in the
counter gadgets triggers to exit the counter gadget, see Fig. 1. The intention
is that exiting the counter gadget with $\blacktriangleright$ should only be
beneficial, i.e., lead to a run with value less than one, if the counter value
represents exactly $N$. This is achieved as follows, see also Fig. 1. Let
$y_{0}\dots y_{n-1}$ be the little-endian bit encoding of $N$. If $y_{i}$ is
zero resp. one, then from $\overline{x_{i}}$ resp. $x_{i}$ a transitions with
$\blacktriangleright$ leads to $\hat{q_{1}}$ with weight _zero_ for each $i$,
ensuring that the value of the run will be less than one. For all other states
(that expect input), reading $\blacktriangleright$ leads to $\hat{q_{1}}$ with
weight one.

In the bit gadgets, for all inputs that are not $\square$ and were not
described together with some output symbol lead back to the same state, e.g.,
reading $b_{2}\mathbbmtt{o}$ from $x_{i}$ (with $i\neq 1$) goes back to
$x_{i}$. From every state (that expects input), reading $\square$ leads to
$q_{1,\square}$ with weight _zero_. This ensures that the value of the run is
less than one, because it does not indicate a counter value that has surpassed
$N$, nor an error in updating the counter.

$\overline{x_{i}}$$x_{i}$$\overline{x_{n}}$$x_{n}$$\hat{q_{1}}$$\hat{q_{1}}$$\dots$$\dots$$c_{i+1}$$b_{i}\mathbbmtt{o}$,
$c_{i}\mathbbmtt{o}$$b_{i}\mathbbmtt{o}$,
$c_{i}\mathbbmtt{o}$$c_{i+1}$$c_{i+1}\mathbbmtt{o}$$v\in
V$$\mathbbmtt{i}$$b_{n}\mathbbmtt{o}$,
$c_{n}\mathbbmtt{o}$$b_{i}\mathbbmtt{o}$$c_{i+1}\mathbbmtt{o}$$v\in V$ Figure
2: Counter gadgets. One gadget for each bit.

We describe the game part. Each transition with source and target in this part
has weight zero. The idea behind the weights in this part is that each run
should have value zero, unless the input stops to faithfully simulate a play
in the counter game, in which case it should have a value greater than zero.

From a state $v\in V$ an output symbol must be read. It is possible to go to a
state $(v,d)$ with output $d$ if there exists a transition of the form
$(v,d,v^{\prime})\in T$. Furthermore, the output $\blacktriangleright$ is
possible leading to the state $q_{\blacktriangleright}$ with weight zero, see
Fig. 1. The intention is to use this output if the counter part of the
automaton represents the value $N$. In $q_{\blacktriangleright}$ the input
$\blacktriangleright$ leads to $q_{0}$ with weight zero, all other inputs
(except $\square$) lead to $q_{0}$ with weight _one_ , $\square$ leads to
$q_{0,\square}$ with weight _one_. These transitions are not shown in Fig. 1,
to not clutter the figure further, if inserted this would also be visualized
by a blue transition labeled with _input error_. As explained before, the
automaton is designed such that reading the input $\blacktriangleright$ in the
counter part leads to a value less than one if the counter value is indeed
$N$.

From a state $(v,d)$ the next symbols must ensure that the duration $d$ is
added to the counter, i.e., the sequence read from here in the game part must
– when read in the counter part – update the automaton representation of the
bit counter. We show how this is done for a concrete example, see Fig. 3. We
assume that a $4$-bit counter is used, that we are in a state $(s,13)$ and
that the possible successors of $s$ with duration $13$ in the counter game are
$s_{1}$ and $s_{2}$. The number $13$ is $1011$ in little-endian notation, so
the next inputs that describe the duration are $b_{0}$, $b_{2}$ and $b_{3}$.
When adding $1011$ to the $4$-bit counter, some carry bits might become one.
The outputs $y$(es) and $n$(o) are used to indicate which ones, the input
$c_{i}$ indicates that the $i$th carry bit becomes one, the input $\diamond$
is used for the carry bits that remain zero. Whether the chosen carry bits are
correct is checked in the counter part of the automaton. If it is incorrect,
the run in the counter part will have value one and the run in this adder
gadget will have value zero. Eventually, the next input symbol indicates which
successor is picked.

From a state $(v,d)$, the input $\square$ leads to $q_{0,\square}$ with weight
zero. From every other state (that expects input), the input $\square$ leads
to $q_{0,\square}$ with weight _one_ (not pictured in Fig. 1 to save space).
The target of a transition for any state (that expects input) and an input
symbol for which we did not describe a transition leads to $\hat{q_{0}}$ with
weight _one_. These transition are symbolized by the transition labeled with
_input error_ in Fig. 1. The first input possibility marks a valid point to
stop simulating the game. The latter two input possibilities mark invalid
points to stop simulating the game, so it is ensured that the value of run is
not zero.

$(s,13)$$s_{1}$$s_{2}$$b_{0}$$\mathbbmtt{o}$$b_{2}$$\mathbbmtt{o}$$b_{3}$$s_{1}$$s_{2}$$y$$y$$y$$y$$c_{1}$$c_{2}$$c_{3}$$c_{4}$$n$$n$$n$$n$$\diamond$$\diamond$$\diamond$$\diamond$$\mathbbmtt{o}$
Figure 3: Adder gadget. Example for the gadget corresponding to transitions
$(s,13,s_{1})$ and $(s,13,s_{2})$ with $n=4$. The duration $13$ is $1011$ in
little-endian notation.

We are ready to prove the correctness of our construction. We make three
observations. First, it is easy to see that we have constructed a
deterministic automaton with weights, thus, it defines a weighted
specification $S$. Second, the domain of $S$ is
$(\Sigma_{\mathbbmtt{i}}\setminus\\{\square\\})^{+}\square$, furthermore, the
domain of both parts of the automaton are the same. Third, we have $0\leq
S(u\otimes v)\leq 1$ for all $u\otimes v\in S$.

We already established that a strictly $1$-approximate $S$-realizer must lie
in the game part of the automaton if it exists.

Assume that Eve has a winning strategy in the countdown game. Consider a
transducer that behaves according to a winning strategy.

We distinguish between input sequences that faithfully simulate a play in the
game, and those that do not.

In the latter case, the run in the game part has a strictly positive value,
all values for alternative runs with same input sequence have a value of at
most one (this property is also true for all other input sequences). So, the
difference is less than one.

In the former case, the output indicates to stop counting after the counter
has reached the value $N$ by the output $\blacktriangleright$, the run in the
game part has value zero. We take a look at all other output sequences that
can be combined with the same input sequence. First, consider all alternative
output sequences such that the run also lies in the game part. All runs in the
game part have a value strictly less than one, so the difference is less than
one. Secondly, consider all alternative output sequences such that the run
lies in the counter part. The second output symbol fixes in which bit gadget
the run lies. Note that after a bit gadget has been entered, the outputs do
not influence the runs anymore, they depend only on the input. Thus, no matter
which gadget is entered, when the input $\blacktriangleright$ is seen, the run
is assigned a value less than one, because the bit value is the same as in
$N$. So, the difference is less than one.

What is left for this direction, is to consider the input sequences that
faithfully simulate the game, but stop before the counter has reached $N$. The
run in the game part induced by the output sequence provided by the transducer
has value zero. All alternative output sequences that induce runs in the
counter part have value less than one, because no counting error occurs and
the $n$th bit does not flip to one. As argued before, all alternative output
sequences that induce runs in the game part have a value less than one.

Assume that Eve has no winning strategy. We consider input sequences that
faithfully simulate the game. Consider the outputs of any transducer that is
an $S$-realizer. The resulting run in the game part has value exactly zero,
because the inputs faithfully simulate the game.

We consider an input sequence such that the value of the counter eventually
surpasses $N$ if the simulation of the game is faithful.

If the provided output sequence is faithful, then the $n$th bit of the counter
eventually flips to one. Considering the run for an alternative output
sequence that lies in the gadget of the $n$th bit of the counter yields a
value of exactly one. The difference is one, the transducer is not strictly
$1$-approximate.

The other possibility is that the output provided by the transducer contain
errors when updating the carry bits in order to maintain a counter value below
$N$. Since such an error is detected in the corresponding counter bit, again
there exists an alternative output sequence such that the corresponding run in
the counter part witnesses the error and is assigned value exactly one. The
difference between the run in the game part and the alternative is one, thus,
the transducer is not strictly $1$-approximate.

We turn to the case of a non-strict threshold. We can easily change the
described specification such that there exists a non-strict $1$-approximate
realizer if, and only if, Eve has a winning strategy in the counter game. For
this we change the weight of two transitions. First, the weight of the
transition that goes from $q_{y}$ to $q_{0,\square}$ is changed from $4$ to
$5$, to ensure that a non-strict $1$-approximate realizer has to still lie in
the game part. Secondly, the weight of outgoing transitions from $q_{n}$ for
some input that is not $\square$ is changed from $1$ to $2$. This ensures that
the runs in the counter part have a value of slightly above one unless
something beneficial for output happens, then the values will be decreased to
exactly one. In the game part the values will be as before, i.e., zero, unless
there is an input error, then the values will be slightly above zero. These
changes ensure that the difference between the runs will always be exactly one
if, and only if, Eve has a winning strategy in the counter game. ∎

####  C.4.4 Proof of Theorem 13: Discounted-sum

######  Theorem 27.

The approximate synthesis problem for a $\mathsf{Dsum}$-specification with a
discount factor $\lambda$ of the form $\frac{1}{n}$ with $n\in\mathbbm{N}$ and
a strict threshold is decidable in NEXPtime and a non-strict threshold in
EXPtime.

###### Proof.

We reduce the problems from the statement to threshold synthesis problems for
$\mathsf{Dsum}$-specifications.

In [8], it is shown that $\mathsf{Dsum}$-automata with a discount factor
$\lambda$ of the form $\frac{1}{\ell}$ with $\ell\in\mathbbm{N}$ are
determinizable with the same discount factor.

The idea is to (disregard the labels of output transitions which yields a
nondeterministic specification automaton and) construct the product automaton
of the specification automaton (without output labels) and a deterministic
version of it. The weights of a transition in the product is the weight of the
transition in the deterministic version subtracted from the weight of the
transition in the specification automaton (without output labels).

We show that there is a transducer that implements an approximate realization
of the specification (without output labels) for a threshold $r$ if, and only
if, there is a transducer that implements a realization of the specification
(without output labels) defined by the product automaton that ensures a value
of $-r$ for each pair.

Let
$\mathcal{A}=(Q_{\mathcal{A}},\Sigma_{\mathbbmtt{i}\mathbbmtt{o}},q_{i}^{\mathcal{A}},\Delta_{\mathcal{A}},F_{\mathcal{A}},\gamma_{\mathcal{A}})$
be a complete $\mathsf{Dsum}$-automaton with a discount factor $\lambda$ of
the form $\frac{1}{\ell}$ with $\ell\in\mathbbm{N}$ defining a
$\mathsf{Dsum}$-specification $S$. Let $\mathcal{B}$ be the nondeterministic
$\mathsf{Dsum}$-automaton that is obtained from $\mathcal{A}$ by replacing all
transition labels that are output symbols by the same arbitrary output symbol,
let $o_{\mathrm{fix}}$ denote this output symbol. Let
$\mathcal{D}=(Q_{\mathcal{D}},\Sigma_{\mathbbmtt{i}\mathbbmtt{o}},q_{i}^{\mathcal{D}},\Delta_{\mathcal{D}},F_{\mathcal{D}},\gamma_{\mathcal{D}})$
be a trim version of $\mathcal{B}$.

Formally, the $\mathsf{Dsum}$-automaton
$\mathcal{C}=(Q_{\mathcal{C}},\Sigma_{\mathbbmtt{i}\mathbbmtt{o}},q_{i}^{\mathcal{C}},\Delta_{\mathcal{C}},F_{\mathcal{C}},\gamma_{\mathcal{C}})$
is defined as follows. The state set is $Q^{\mathcal{A}}\times
Q^{\mathcal{D}}$, the initial state is
$(q_{i}^{\mathcal{A}},q_{i}^{\mathcal{D}})$, the final state set is
$F_{\mathcal{A}}\times F_{\mathcal{D}}$, and $\Delta_{\mathcal{C}}$ contains
the following transitions

  * $\bullet$

$(p,q)$ to $(p^{\prime},q^{\prime})$ if
$(p,\sigma,p^{\prime})\in\Delta_{\mathcal{A}}$ and
$(q,\sigma,q^{\prime})\in\Delta_{\mathcal{D}}$ for all $(p,q)\in
Q^{\mathcal{A}}_{\mathbbmtt{i}}\times Q^{\mathcal{D}}_{\mathbbmtt{i}}$, the
weight of the transition is
$\gamma_{\mathcal{A}}((p,\sigma,p^{\prime}))-\gamma_{\mathcal{D}}((q,\sigma,q^{\prime}))$,

  * $\bullet$

$(p,q)$ to $(p^{\prime},q^{\prime})$ if
$(p,\sigma,p^{\prime})\in\Delta_{\mathcal{A}}$ and
$(q,o_{\mathrm{fix}},q^{\prime})\in\Delta_{\mathcal{D}}$ for all $(p,q)\in
Q^{\mathcal{A}}_{\mathbbmtt{o}}\times Q^{\mathcal{D}}_{\mathbbmtt{o}}$, the
weight of the transition is
$\gamma_{\mathcal{A}}((p,\sigma,p^{\prime}))-\gamma_{\mathcal{D}}((q,o_{\mathrm{fix}},q^{\prime}))$.

Given a threshold $r\in\mathbbm{Q}$ and $\triangleleft\in\\{<,\leq\\}$, it is
easy to see that there is a transducer that implements a
$r_{\triangleleft}$-approximate $S$-realization if, and only if, there is a
transducer that implements a $S_{\mathcal{C}}$-realization that ensures a
value $\triangleright-r$ for each pair, where $S_{\mathcal{C}}$ is the
$\mathsf{Dsum}$-specification defined by $\mathcal{C}$, and $\triangleright=>$
if $\triangleleft=<$ and $\triangleright=\geq$ otherwise.

It is left to show the claimed complexity bounds. We assume that the weights
are given in binary and the discount factor $\lambda$ is given as a pair of
binary numbers. Following the construction presented in [8], $\mathcal{D}$ is
of size $m^{n}=2^{n\cdot\mathrm{log}\ m}$, where $n$ is the number of states
of $\mathcal{A}$ and $\mathrm{log}\ m$ is a number in the size of the
representation of its weights. Thus, the number of states of $\mathcal{D}$ is
exponential in the number of states of $\mathcal{A}$ and polynomial in the
weights of $\mathcal{A}$. The weights in $\mathcal{D}$ are polynomial (the
representation of the weights grows by one bit at most) in the weights of
$\mathcal{A}$. Hence, the size of the game arena is exponential in the number
of states and polynomial in the weights of $\mathcal{A}$, and its weights are
polynomial in the weights of $\mathcal{A}$.

For a strict threshold, Theorem 9 yields that solving critical prefix
threshold games is in NP for discounted-sum. Since the constructed arena is of
exponential size, the claimed complexity bound follows.

For a non-strict threshold, Theorem 9 yields that solving critical prefix
threshold games in $\textsc{NP}\cap\textsc{coNP}$ for discounted-sum. To
obtain our desired complexity bound, we make a more precise analysis.
Threshold synthesis problems for discounted-sum are reduced in polynomial time
to critical prefix discounted-sum threshold games which are reduced in
polynomial time to discounted-sum games, see the proof of Theorem 16. Using
the value iteration algorithm from [36] to solve discounted-sum games yields
the claimed complexity bound, because it runs in polynomial time in the size
of the arena, logarithmic in the absolute maximal weight of the arena, and
exponential in the representation of the discount factor, i.e., polynomial in
the discount factor. An analysis of the run time of the value iteration
algorithm is given in [29]. ∎

###  C.5 Infinite words and Church synthesis

####  C.5.1 Some observation on the finite-memory requirement for synthesis
problems

In the definition of synthesis problems of Section 2, we ask for the
realizability of the specification by a (finite-state) transducer. This
requirement can be relaxed to asking whether the specification is realizable
by some sequential function $f$, i.e. a function of type
$\Sigma_{\mathbbmtt{i}}^{*}\rightarrow\Sigma_{\mathbbmtt{o}}$ prescribing
which output symbol should be produced by Eve, depending on the sequence of
input symbols Adam has provided so far. In other words, we could relax the
requirement that $f$ is computable by a (finite-state) transducer. First, we
impose this requirement because we are interested in functions which can be
finitely represented and computed. Second, we claim that realizability in the
relaxed sense entails realizability by transducers. To see that, consider
first the threshold synthesis problems for all measures
$V\in\\{\mathsf{Sum},\mathsf{Avg},\mathsf{Dsum}\\}$. They are all solved by
reduction to corresponding critical prefix games, with back-and-forth
translations from finite-memory strategies to transducers. For those games, it
has been shown in Section 3 that finite-memory suffice for Eve to win. It
entails our claim for threshold synthesis problems.

The claim also holds for (strict and non-strict) approximate synthesis (and
therefore for best-value synthesis by taking non-strict threshold $0$).
Indeed, for $\mathsf{Sum}$-specification $S$, the approximate synthesis
algorithm for $S$ works by reduction to the regret determinization problem for
a nondeterministic $\mathsf{Sum}$-automaton (Theorem 24). The algorithmic
solution to the latter problem itself relies on solving a game whose finite-
memory strategies can be back-translated into (finite-state) regret
determinizers [26], which in turn are back-translated into transducers
realizing $S$ for the threshold synthesis problem as shown in Lemma 10. In
[26], it is shown that finite-memory strategies are sufficient to win,
entailing our claim for $\mathsf{Sum}$-specifications. For
$\mathsf{Avg}$-specifications (Theorem 25), the approximate synthesis
algorithms work by reduction to some critical prefix energy games of imperfect
information with fixed initial credit for which finite-memory are sufficient
to win by Theorem 8. Likewise for $\mathsf{Dsum}$-specifications and discount
factor $1/n$, the approximate synthesis problems (Theorem 27) reduce to
critical prefix threshold games for which finite-memory are known to suffice
(Theorem 18).

####  C.5.2 Proof of Theorem 14

See 14

These synthesis problems can be directly reduced to the corresponding
synthesis problems on finite words. E.g., synthesis problem for
$\mathsf{Thres}^{>t}(W)$ reduces to the strict threshold synthesis problem for
$W$ (on finite words). The main difference is that our quantitative synthesis
problems on finite words require realizability by a transducer. This is
however not a problem. Indeed, we could have relaxed this condition to asking
for realizability by a possibly infinite-state transducer or equivalently, a
function of type
$\Sigma_{\mathbbmtt{i}}^{*}\rightarrow\Sigma_{\mathbbmtt{o}}$. However, the
algorithms we provide to solve quantitative synthesis problems over finite
words guarantee that (finite-state) transducers are sufficient. So we do not
need infinite memory.

###### Proof.

We consider the case of threshold specifications. For best-value and
approximate synthesis, the proof is the same. The proof is also parametric in
$V$. Given a deterministic $V$-automaton defining a weighted specification $W$
and a threshold $t$, we reduce the synthesis problem for
$\mathsf{Thres}^{\triangleright t}(W)$ to the threshold synthesis problem (on
finite words) for $W$, which is decidable by Theorem 9. Let us show the
correctness of the reduction.

Assume that $\mathsf{Thres}^{\triangleright t}(W)$ is realizable by a (total)
function
$\lambda:\Sigma_{\mathbbmtt{i}}^{*}\rightarrow\Sigma_{\mathbbmtt{o}}$. We
construct a function
$f\colon\text{dom}(W)\rightarrow\Sigma_{\mathbbmtt{o}}^{*}$ and prove that it
realizes $W$ (over finite words for the threshold problem). To define $f$, let
$u=i_{1}\dots i_{k}\in\text{dom}(W)$. Then, let
$f(u)=\lambda(i_{1})\lambda(i_{1}i_{2})\dots\lambda(i_{1}\dots i_{k})$. By
definition of Church synthesis, since $\lambda$ realizes
$\mathsf{Thres}^{\triangleright t}(W)$, for any infinite continuation
$i_{k+1}\dots\in\Sigma_{\mathbbmtt{i}}^{\omega}$, we have for all $j\geq 0$,
if $i_{1}\dots i_{j}\in\text{dom}(W)$, then
$W(i_{1}\lambda(i_{1})i_{2}\lambda(i_{1}i_{2})\dots i_{j}\lambda(i_{1}\dots
i_{j}))\triangleright t$. It is true in particular for $j=k$ and therefore,
$u\otimes f(u)\in W$ and $W(u\otimes f(u))\triangleright t$.

Conversely, assume that $W$ is realizable (for threshold $t$) by a function
$f:\text{dom}(W)\rightarrow\Sigma_{\mathbbmtt{o}}^{*}$, which can be assumed
to be computable by a transducer thanks to the observation of Section C.5.1.
We construct a function
$\lambda:\Sigma_{\mathbbmtt{i}}^{*}\rightarrow\Sigma_{\mathbbmtt{o}}$ and
prove that $(i)$ it realizes $\mathsf{Thres}^{\triangleright t}(W)$ and $(ii)$
it is computable by a Mealy machine. The function $\lambda$ has to be defined
by all finite words over $\Sigma_{\mathbbmtt{i}}$. Let $u=i_{1}\dots i_{k}$ be
such a word and let $o_{0}\in\Sigma_{\mathbbmtt{o}}$ be some arbitrarily
chosen output symbol. We consider two cases:

  1. 1.

there exists $v\in\Sigma_{\mathbbmtt{i}}^{*}$ such that $uv\in\text{dom}(W)$.
Then, we let $\lambda(u)$ be the $k$th letter of $f(uv)$ (since $f$ is
computable by a transducer, this definition is independent from the choice of
$v$)

  2. 2.

there is no such $v$. Then, we let $\lambda(u)=o_{0}$.

$(i)$ Let us show that $\lambda$ realizes $\mathsf{Thres}^{\triangleright
t}(W)$. Let $i_{1}i_{2}\dots\in\Sigma_{\mathbbmtt{i}}^{\omega}$ be some input
$\omega$-word and for all $j$, let $o_{j}=\lambda(i_{1}\dots i_{j})$. Assume
that $i_{1}\dots i_{k}\in\text{dom}(W)$. Then, by the choice of
$o_{1},\dots,o_{k}$ (in particular by taking $v=\epsilon$ in the definition of
$\lambda$ above), we have $f(i_{1}\dots i_{k})=o_{1}\dots o_{k})$ and since
$f$ realizes $W$, we get $W(i_{1}o_{1}\dots i_{k}o_{k})$. It is true for all
$k$, therefore $i_{1}o_{1}i_{2}o_{2}\dots\in\mathsf{Thres}^{\triangleright
t}(W)$.

$(ii)$ Let $T$ be a transducer computing $f$. We construct a Mealy machine for
$\lambda$. Since $T$ is defined only over $\text{dom}(W)$, we have to extend
its domain to any finite word. To do so, we just complete $T$ whenever there
is a missing transition towards a sink state which outputs $o_{0}$ whenever it
reads an input letter.

The reduction (and proof of its correctness) is exactly the same for best-
value and approximate synthesis. The only difference is the theorems we rely
on to get decidability. For best-value and $\mathsf{Sum}$, decidability is
given by Theorem 12, for best-value and $\mathsf{Avg}$, by Theorem 22, for
best-value and $\mathsf{Dsum}$, by Theorem 23. For the approximate synthesis
and $\mathsf{Sum}$ it is given by Theorem 24, for $\mathsf{Avg}$ by Theorem
25, and for $\mathsf{Dsum}$ by Theorem 27. ∎


#  Stream VByte: Faster Byte-Oriented Integer Compression

Daniel Lemire<EMAIL_ADDRESS>Nathan Kurz<EMAIL_ADDRESS>Christoph Rupp
<EMAIL_ADDRESS>LICEF, Université du Québec, 5800 Saint-Denis, Montreal, QC,
H2S 3L5 Canada  Orinda, California USA Upscaledb, Munich, Germany

###### Abstract

Arrays of integers are often compressed in search engines. Though there are
many ways to compress integers, we are interested in the popular byte-oriented
integer compression techniques (e.g., VByte or Google’s varint-GB). Although
not known for their speed, they are appealing due to their simplicity and
engineering convenience. Amazon’s varint-G8IU is one of the fastest byte-
oriented compression technique published so far. It makes judicious use of the
powerful single-instruction-multiple-data (SIMD) instructions available in
commodity processors. To surpass varint-G8IU, we present Stream VByte, a novel
byte-oriented compression technique that separates the control stream from the
encoded data. Like varint-G8IU, Stream VByte is well suited for SIMD
instructions. We show that Stream VByte decoding can be up to twice as fast as
varint-G8IU decoding over real data sets. In this sense, Stream VByte
establishes new speed records for byte-oriented integer compression, at times
exceeding the speed of the memcpy function. On a
$3.4\text{\,}\mathrm{G}\mathrm{H}\mathrm{z}$ Haswell processor, it decodes
more than 4 billion differentially-coded integers per second from RAM to L1
cache.

###### keywords:

Data compression , Indexing , Vectorization , SIMD Instructions

††journal: Information Processing Letters

##  1 Introduction

We frequently represent sets of document or row identifiers by arrays of
integers. Compressing these arrays can keep the data closer to the processor
and reduce bandwidth usage, and fit more data in memory or on a disk. Though
data can always be compressed using generic algorithms such as Lempel-Ziv
coding (LZ77), specialized compression algorithms for integers can be orders
of magnitude faster. We consider codecs to compress 32-bit unsigned integers
(in $[0,2^{32})$). We are especially interested in compressing arrays where
most integers are small. In addition to such arrays that arise naturally,
sorted arrays of non-small integers can often be treated as arrays of small
integers by considering the successive differences (“deltas”). So instead of
compressing the integers $x_{1},x_{2},\ldots$ directly, we can compress the
gaps between them $x_{1},x_{2}-x_{1},x_{3}-x_{2},\ldots$ There are many
integer-compression algorithms applicable to arrays of small integers. One
option are byte-oriented techniques [1]. In these formats, the main data
corresponding to an integer is stored in consecutive whole bytes, and all bits
within a given byte correspond to only one such integer. Though byte-oriented
formats do not offer the best compression ratios or the best speeds, they are
in widespread use within databases, search engines and data protocols in part
because of their simplicity.

Historically, the most widely known byte-oriented compression algorithm is
VByte. It writes a non-negative integer starting from the least significant
bits, using seven bits in each byte, with the most significant bit set to zero
when the following byte continues the current integer. Thus integers in
$[0,2^{7})$ are coded using a single byte, integers in $[2^{7},2^{14})$ in two
bytes and so on. For example, the integer 32 is written using a single byte
(00100000) and the integer 128 is written using two bytes (10000000 and
00000001).

To decode VByte data, it suffices to iterate over the compressed bytes while
checking the value of the most significant bit. Whenever the number of bytes
required per integer is easily predictable—such as when most integers fit in
$[0,2^{7})$—the absence of branch prediction errors allows high decoding
speeds on modern-day superscalar processors capable of speculative execution.

Unfortunately, not all data is easily predictable. In some of these case, the
decoding speed of VByte compressed data becomes a bottleneck. For this reason,
Google developed varint-GB [2]. In varint-GB, numbers are compressed and
decompressed in blocks of four. Instead of having to check one bit per
compressed byte, only one control byte for every four integers needs to be
processed. For unpredictable patterns, this block-based design can reduce the
number of branch mispredictions by a factor of four.

Modern processors (e.g., ARM, POWER, Intel, AMD) have instructions that
perform the same operation on multiple scalar values (e.g., the addition of
two sets of four 32-bit integers). These instructions are said to be _single-
instruction-multiple-data_ (SIMD) while the algorithms designed to take
advantage of SIMD instructions are said to be _vectorized_.

Stepanov et al. [1] considered the problem of vectorizing byte-oriented
compression. They reported that there was little benefit to vectorizing VByte
decoding. As an alternative to VByte and varint-GB, Stepanov et al. proposed a
new patented byte-oriented format (varint-G8IU) designed with SIMD
instructions in mind. It proved more than three times faster than VByte on
realistic sets of document identifiers.

Plaisance et al. [3] revisted the VByte decoding problem: unlike Stepanov et
al., their Masked VByte decoder is twice as fast as a scalar VByte decoder.
Though it should not be expected to be as fast as a decoder working on a
format designed for SIMD instructions (e.g., varint-G8IU), it can help in
systems where the data format is fixed.

There remained an open question: could varint-G8IU be surpassed? Could byte-
oriented decoding be even faster? We answer this question by the positive. In
fact, our proposal (Stream VByte) can be twice as fast as varint-G8IU on
realistic data.

##  2 SIMD Instructions

Since the introduction of the Pentium 4 in 2001, x64 processors have had
vector instructions operating on 16-byte SIMD registers (called XMM
registers). These registers can store four 32-bit integers.

A Stream VByte decoder (§ 4) can be written with just two x64 SIMD assembly
instructions:

  * •

The movdqu instruction can load 16 bytes from memory into a SIMD register, or
write such a register to memory. On recent Intel processors (e.g., Haswell)
these operations have multicycle latency (5–6 cycles from L1 cache), but they
also have high throughput. In ideal cases, two XMM loads and an XMM write can
all be issued each CPU cycle.

  * •

The shuffle (pshufb) instruction can selectively copy the byte values of one
SIMD register $v$ to another according to a mask $m$. If
$v_{0},v_{1},\ldots,v_{15}$ are the values of the 16 individual bytes in $v$,
and $m_{0},m_{1},\ldots,m_{15}$ are the bytes within $m$
($m_{i}\in\\{-1,0,1,2,\ldots,15\\}$), then pshufb outputs
$(v_{m_{0}},v_{m_{1}},\ldots,v_{m_{15}})$ where $v_{-1}\equiv 0$. Once its
operands are in registers, the pshufb instruction is fast: it has a latency of
one cycle and a reciprocal throughput of one instruction per cycle.

Both of these SIMD instructions are available in all processors supporting the
SSSE3 instruction set, i.e., almost all x64 processors produced since 2010.

### Differential Coding

When we have compressed “deltas”, or successive differences
$\delta_{1},\delta_{2},\ldots=x_{1},x_{2}-x_{1},x_{3}-x_{2},\ldots$ instead of
the original integers, we need to compute a prefix sum to recover the original
integers
($\delta_{1},\delta_{1}+\delta_{2},\delta_{1}+\delta_{2}+\delta_{3},\ldots$).
The computation of the prefix sum can be accelerated by vector shifts and
additions. We can compute the prefix sum of a vector of size $2^{L}$ using $L$
shifts and $L$ additions [4]. For example, consider the vector of delta values
$(3,4,12,1)$. We add to this vector a version of itself shifted by one integer
($(0,3,4,12)$) to get $(3,7,16,13)$. Finally, we add to this last vector a
version of itself shifted by two integers ($0,0,3,7$) to get the prefix sum
$(3,7,19,20)$ of the original vector.

##  3 Byte-Oriented Integer Codecs

The VByte format uses the most significant bit of each byte as a control bit.
Thus an integer is compressed to an array of $L+1$ bytes
$b_{0},b_{1},\ldots,b_{L}$ such that $b_{0},b_{1},\ldots,b_{L-1}$ have their
most significant bits set to 1 whereas the most significant bit of $b_{L}$ is
zero. That is, if we view bytes as unsigned integers in $[0,2^{8})$, we have
that $b_{0},b_{1},\ldots,b_{L}\in[2^{7},2^{8})$ and $b_{L}\in[0,2^{7})$. We
can decode the compressed integer as $\sum_{i=0}^{L}(b_{i}\bmod 2^{7})\times
2^{7i}$. Integers in $[2^{7(L-1)},2^{7L})$ are coded using $L$ bytes for
$L=1,2,\ldots$ The software to decode the VByte format is easy to write in
standard C, but performance on inputs with mixed byte lengths $L$ can suffer
due to poor branch prediction.

For greater speed, Plaisance et al. [3] proposed the Masked VByte decoder that
uses SIMD instructions. It works directly on the standard VByte format. The
Masked VByte decoder gathers the most significant bits of an array of
consecutive bytes using the pmovmskb x64/SSE2 instruction. Using look-up
tables and a shuffle instruction (pshufb), Masked VByte permutes the bytes to
arrive at the decoded integers. We refer the interested reader to Plaisance et
al. [3] for a detailed description.

Table 1: Overview of the byte-oriented integer compression techniques name of decoder |  data format | SIMD
---|---|---
VByte |  7 data bits per byte, 1 bit as continuation flag | no
Masked VByte [3] |  identical to VByte | yes
varint-GB [2] |  fixed number of integers (4) compressed to a variable number of bytes (4–16), prefixed by a control byte | no
varint-G8IU [1] |  fixed number of compressed bytes (8) for a variable number of integers (2–8), prefixed by a control byte | yes
Stream VByte (novel) |  control bytes and data bytes in separate streams | yes

Whereas the VByte format interleaves actual integer data (using the least
significant 7 bits of each byte) with control data (using the most significant
bit of each byte), varint-GB stores the control data using a distinct control
byte corresponding to a block of four integers [2]. See Table 1 and Fig. 1. To
store an integer $x$, we use $\lceil\log_{2^{8}}(x+1)\rceil$ continuous bytes,
since $x\in[0,2^{\lceil\log_{2^{8}}(x+1)\rceil})$ always holds. Given four
integers, $x_{1},x_{2},x_{3},x_{4}$, the control byte stores the lengths
$\lceil\log_{2^{8}}(x_{i}+1)\rceil$ for each of the four integers $i=1,2,3,4$.
Indeed, because there are only four possible byte lengths ($\\{1,2,3,4\\}$),
each of the four individual byte lengths can be stored using just two bits.
Thus a block in varint-GB used to store integers $x_{1},x_{2},x_{3},x_{4}$
contains a control byte followed by
$\sum_{i=1}^{4}\lceil\log_{2^{8}}(x_{i}+1)\rceil$ bytes. When the number of
integers is not divisible by four, an incomplete block might be used. For this
reason, it might be necessary to record how many integers are compressed
(e.g., as a format header).

To decode varint-GB data, the control byte is first parsed, from which we
extract the four lengths. The integers $x_{1},x_{2},x_{3},x_{4}$ are then
extracted (without any branching) and we advance to the next control byte. To
achieve higher speed for highly compressible data, we find it useful to
include an optimized code path for when all integers are small
($x_{1},x_{2},x_{3},x_{4}\in[0,2^{8})$).

$\overbracket{01|00|00|11}^{\text{control
byte}}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x00}}^{\text{2
bytes}}}_{1024}$$\underbrace{\overbracket{\texttt{0x0c}}^{\text{1
byte}}}_{12}$$\underbrace{\overbracket{\texttt{0x0a}}^{\text{1
byte}}}_{10}$$\underbrace{\overbracket{\texttt{0x40}|\texttt{0x00}|\texttt{0x00}|\texttt{0x00}}^{\text{4
bytes}}}_{$1\,073\,741\,824$}$ (a) Integer values
$1024,12,10,$1\,073\,741\,824$$ compressed using 9 bytes

$\overbracket{00|00|00|01}^{\text{control
byte}}$$\underbrace{\overbracket{\texttt{0x01}}^{\text{1
byte}}}_{1}$$\underbrace{\overbracket{\texttt{0x02}}^{\text{1
byte}}}_{2}$$\underbrace{\overbracket{\texttt{0x03}}^{\text{1
byte}}}_{3}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x00}}^{\text{2
bytes}}}_{$1024$}$ (b) Integer values $1,2,3,1024$ using 6 bytes

Figure 1: Examples of blocks of four integers compressed with varint-GB.

Like varint-GB, varint-G8IU also uses a control byte [1], but it does not
describe a fixed number (four) of integers. Rather, varint-G8IU divides the
compressed output into blocks of eight data bytes for each control byte. Each
block can contain between two and eight compressed integers. See Fig. 2. The
control byte describes the next eight data bytes. Thus a compressed block in
varint-G8IU is always made of exactly nine compressed bytes. Each bit in the
control byte corresponds to one of the eight data bytes. A bit value of 0
indicates that the data byte completes a compressed integer, whereas a bit
value of 1 indicates that the data byte is part of a compressed byte or is
“wasted”. Indeed, as shown in Fig. 2b, if the control byte ends with trailing
ones, then they correspond to bytes that are wasted (they do not correspond to
a compressed integer). A case with waste like the example of Fig. 2b might
arise if the next integer to be coded is larger or equal to $2^{8}$ so that it
cannot fit in the remaining byte.

varint-G8IU can sometimes have worse compression than VByte due to the wasted
bytes. However, varint-G8IU can compress a stream of integers in
$[2^{7},2^{8})$ using only nine bits per integer on average, against $16$
bytes for VByte, so varint-G8IU can also, in principle, compress better.
varint-GB has a slight size disadvantage compared to varint-G8IU when
compressing streams of integers in $[0,2^{8})$ as it uses ten bits per integer
against only nine bits per integer for varint-G8IU. However, this is offset by
varint-GB’s better compression ratio for larger integers.

$\overbracket{10|0|0|1110}^{\text{control
byte}}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x00}}^{\text{2
bytes}}}_{1024}$$\underbrace{\overbracket{\texttt{0x0c}}^{\text{1
byte}}}_{12}$$\underbrace{\overbracket{\texttt{0x0a}}^{\text{1
byte}}}_{10}$$\underbrace{\overbracket{\texttt{0x40}|\texttt{0x00}|\texttt{0x00}|\texttt{0x00}}^{\text{4
bytes}}}_{$1\,073\,741\,824$}$ (a) Integer values
$1024,12,10,$1\,073\,741\,824$$ compressed using 9 bytes

$\overbracket{0|0|0|10|10|\underbrace{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}_{\text{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}waste}}}^{\text{control
byte}}$$\underbrace{\overbracket{\texttt{0x01}}^{\text{1
byte}}}_{1}$$\underbrace{\overbracket{\texttt{0x02}}^{\text{1
byte}}}_{2}$$\underbrace{\overbracket{\texttt{0x03}}^{\text{1
byte}}}_{3}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x01}}^{\text{2
bytes}}}_{$1024$}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x01}}^{\text{2
bytes}}}_{$1024$}$$\underbrace{\overbracket{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{0x00}}^{\text{1
byte}}}_{\text{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}waste}}$
(b) Integer values $1,2,3,1024,1024$ compressed using 9 bytes

Figure 2: Examples of blocks of 9 compressed bytes representing different
numbers of integers in the varint-G8IU format

##  4 The Stream VByte format

Stepanov et al. [1] attempted to accelerate varint-GB by using SIMD
instructions. The results were far inferior to varint-G8IU—despite the
apparent similarity between the formats, with each having one control byte
followed by some data.

To understand why it might be difficult to accelerate the decoding of data
compressed in the varint-GB format compared to the varint-G8IU format,
consider that we cannot decode faster than we can access the control bytes. In
varint-G8IU, the control bytes are conveniently always located nine compressed
bytes apart. Thus while a control byte is being processed, or even before, our
superscalar processor can load and start processing upcoming control bytes, as
their locations are predictable. Instructions depending on these control bytes
can be reordered by the processor for best performance. However, in the
varint-GB format, there is a strong data dependency: the location of the next
control byte depends on the current control byte. This increases the risk that
the processor remains underutilized, delayed by the latency between issuing
the load for the next control byte and waiting for it to be ready.

But the varint-G8IU format has its own downside: it decodes a variable number
of integers per control bytes (between two and eight inclusively). We expect
that it is faster to store full SIMD registers (e.g., four integers) to memory
with each iteration. Moreover, when using differential coding, it is more
convenient and efficient to reconstruct the original integers from their
deltas when they come in full SIMD registers.

$\overbracket{01|00|00|11}^{\text{control
byte}}$$\overbracket{00|00|00|01}^{\text{control byte}}$ Control bytes are
stored continuously in a separate address than from the data bytes that are
also stored continuously. This layout minimizes latency while accessing the
control bytes. $\underbrace{\overbracket{\texttt{0x04}|\texttt{0x00}}^{\text{2
bytes}}}_{1024}$$\underbrace{\overbracket{\texttt{0x0c}}^{\text{1
byte}}}_{12}$$\underbrace{\overbracket{\texttt{0x0a}}^{\text{1
byte}}}_{10}$$\underbrace{\overbracket{\texttt{0x40}|\cdots|\texttt{0x00}}^{\text{4
bytes}}}_{$1\,073\,741\,824$}$$\underbrace{\overbracket{\texttt{0x01}}^{\text{1
byte}}}_{1}$$\underbrace{\overbracket{\texttt{0x02}}^{\text{1
byte}}}_{2}$$\underbrace{\overbracket{\texttt{0x03}}^{\text{1
byte}}}_{3}$$\underbrace{\overbracket{\texttt{0x04}|\texttt{0x00}}^{\text{2
bytes}}}_{$1024$}$ Figure 3: Compressed Stream VByte bytes for
$1024,12,10,$1\,073\,741\,824$,1,2,3,1024$.

Thankfully, we can combine the benefits of the varint-GB and the varint-G8IU
formats: (1) having control bytes at predictable locations so that the
processor can access series of control bytes simultaneously, without data
dependency and (2) decoding integers in full SIMD registers. We use a format
that is identical to that of varint-GB with the small, but important,
difference that the control bytes are stored continuously in a separate stream
from the data bytes. See Fig. 3. Since we record how many integers $N$ are
compressed, we can use the first $\lceil 2N/8\rceil$ compressed bytes to store
the control bytes followed by the data bytes.

⬇ 1// "databytes" is a byte pointer to compressed data 2// "control" contains
control byte 3uint8_t C = lengthTable[control]; // C is between 4 and 16
4__m128i Data = _mm_loadu_si128((__m128i *) databytes); 5__m128i Shuf =
_mm_loadu_si128(shuffleTable[control]); 6Data = _mm_shuffle_epi8(Data, Shuf);
// final decoded data 7datasource += C;
---
Figure 4: Core of the Stream VByte decoding procedure in C with Intel
intrinsics

Decoding a block requires no more than a handful of lines of code (see Fig.
4). At all times, we maintain a pointer into the stream of control bytes and a
pointer into the stream of data bytes. They are initialized to the respective
beginning of their streams.

  * •

We start by retrieving the control byte. Given the control byte, we load from
a 256-integer look-up table the number $C$ of corresponding compressed bytes
($C\in[4,16]$). See Fig. 4, line 3. For example, if the control byte is made
of only zeros, then the sought-after length is four.

  * •

Simultaneously, we load the next 16 data bytes in a 16-byte SIMD register. See
Fig. 4, line 4. Depending on the control byte, we use only $C$ of these bytes.

  * •

From the control byte, we load a 16-byte shuffling mask for the pshufb
instruction (line 5). There are 256 such masks, one for each possible value of
the control byte.

  * •

We apply the pshufb instruction on the data SIMD register using the shuffling
mask (line 6). The result contains the uncompressed integers. If differential
coding is used, the result contains four deltas which can be decoded (§ 2).

  * •

Both pointers are advanced. The control-byte pointer is advanced by one byte
whereas the data-byte pointer is advanced by $C$ bytes (line 7).

Incomplete blocks (containing fewer than four integers) are decoded using a
scalar function similar to that used for varint-GB. Likewise, when we detect
that fewer than 16 data bytes remain, we use a scalar function. Further, we
found it useful to use an optimized code path when we have four zero control
bytes in sequence.

When the data is highly compressible, the Stream VByte format stores long runs
of control bytes set to zero. In some applications, it might be beneficial to
compress such runs to improve compression (e.g., using run-length encoding).

Though details are outside our scope, we have implemented fast functions to
append new integers to a compressed Stream VByte array without having to
recompress the data. We append extra data, and occasionally grow the control
bytes stream.

##  5 Experiments

We implemented our compression software in C. We use the GNU GCC 4.8 compiler
with the -O3 flag. To ease reproducibility, our software is available
online.111https://goo.gl/6Op1t4 and https://github.com/lemire/streamvbyte

We run the benchmark program on a Linux server with an Intel i7-4770 processor
($3.4\text{\,}\mathrm{G}\mathrm{H}\mathrm{z}$). This Haswell processor has
$32\text{\,}\mathrm{k}\mathrm{B}$ of L1 data cache and
$256\text{\,}\mathrm{k}\mathrm{B}$ of L2 cache per core with
$8\text{\,}\mathrm{M}\mathrm{B}$ of shared L3 cache. The machine has ample
memory ($32\text{\,}\mathrm{G}\mathrm{B}$ of dual-channel DDR3 1600 RAM).
Turbo Boost and Speed Step are disabled, so the processor runs consistently at
its rated speed of $3.4\text{\,}\mathrm{G}\mathrm{H}\mathrm{z}$. We measure
wall-clock times to decompress data from RAM to L1 cache. All tests are
single-threaded.

Search engines typically rely on posting lists: given a term, we create a list
of all document identifiers corresponding to documents where the term appears.
Instead of directly storing the identifiers, we use differential coding to
reduce the average number of bits required to store each compressed integer.
The document identifiers are sorted in increasing order ($x_{1},x_{2},\ldots$
where $x_{i}>x_{i-1}$ for $i=2,3,\ldots$), and we compress their successive
differences (e.g., $\delta_{1}=x_{1}-0,\delta_{2}=x_{2}-x_{1},\ldots$). To
recover the original identifiers during decompression, we need to compute a
prefix sum ($x_{i}=\delta_{i}+x_{i-1}$). When using vectorized formats, we
vectorize the computation of the prefix sum. All decoding times include
differential coding to reconstruct the original integers.

We use a collection of posting lists extracted from the ClueWeb09 (Category B)
data set. ClueWeb09 includes 50 million web pages. We have one posting list
for each of the 1 million most frequent words—after excluding stop words and
applying lemmatization. Documents are sorted lexicographically based on their
URL prior to attributing document identifiers.222The posting-list data is
freely available (http://goo.gl/DygoQM).

We want to sort the posting lists by compressibility. For this purpose, the
posting lists are grouped based on length: we store and process lists of
lengths $2^{K}$ to $2^{K+1}-1$ together for all values of $K$ needed by the
corpus. While the correlation is not perfect, shorter lists tend to be less
compressible than longer lists since their gaps tend to be larger.

We decode the compressed data sequentially to a buffer of $4096$ 32-bit
integers (half the size of the $32\text{\,}\mathrm{k}\mathrm{B}$ L1 cache).
For each group and each decoder, we compute the average decoding speed in
billions of 32-bit integers per second (Bis). So that disk access is not an
issue, the data is loaded in memory prior to processing. The length of the
arrays, their compressibility and the volume of data varies from group to
group.

Our results are summarized in Fig. 5a. For Stream VByte, the reported speed
ranges from $4.0\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$ for highly
compressible data to $1.1\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$ for less
compressible data. The second fastest codec is varint-G8IU with speeds ranging
from $2.7\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$ to
$1.1\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$. Next we have Masked VByte and
varint-GB with speeds ranging from
$2.6\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$ to
$0.5\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$. Though varint-GB is more than
$50\text{\,}\mathrm{\char 37\relax}$ faster than Masked VByte when the data is
poorly compressible, they are almost tied speed-wise when the data is more
compressible. Finally, we find VByte with speed ranging from
$1.1\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$ to
$0.3\text{\,}\mathrm{B}\mathrm{i}\mathrm{s}$. For all groups of posting lists,
Stream VByte is fastest of the algorithms considered. It is always at least
$\approx 2.5\times$ faster than the conventional VByte decoder and sometimes
nearly $5\times$ faster. Compared to varint-G8IU, Stream VByte can be twice as
fast. For reference, we also provide the copy speed of the uncompressed data
by blocks of up to $4096$ integers using the C function memcpy. For highly
compressible data, Stream VByte is faster than memcpy because fewer bytes are
read. In our worst case, Stream VByte decompresses at
$70\text{\,}\mathrm{\char 37\relax}$ of the corresponding memcpy speed.

Though they are faster, both Stream VByte and varint-G8IU use .5 to 2 more
bits per integer than VByte in these tests: see Fig. 5b. Stream VByte and
varint-GB have almost exactly the same storage requirements due to their
similar format. Also Masked VByte and VByte have exactly the same compressed
format.

(a) Decoding speed in billions of integers per second (Bis) versus the
compressibility of the data (in bits per integer for VByte) (b) Extra storage
space in bits per integer vs. the storage requirement of VByte

Figure 5: Results over sets of posting lists (ClueWeb)

Byte-oriented codecs make it convenient to program advanced operations
directly on the compressed stream. We benchmark two such operations: (1) we
seek the location of the first value greater or equal to a given target, and
retrieve this value, and (2) we select the $i^{\mathrm{th}}$ integer. Given a
bit width $b\leq 24$, we first generate an array of 256 random integers in
$[0,2^{b})$: $\delta_{1},\delta_{2},\ldots$. The prefix sum is computed
($\delta_{1},\delta_{1}+\delta_{2},\ldots$) and used as input data. We omit
varint-G8IU in this experiment. In Fig. 6a, we randomly seek a value in range.
In Fig. 6b, we randomly select the value at one of the indexes. In these
tests, Stream VByte offers the best speed and is up to three times faster than
VByte, with intermediate results for other codecs. The performance is
noticeably better when all deltas compress down to a single byte due the
simple and predictable code path: it happens when all deltas fit in 7 bits for
VByte and Masked VByte, and when they all fit in 8 bits for varint-GB and
Stream VByte.

(a) Seek speed (b) Select speed

Figure 6: Seek and select results over blocks of 256 random integers

## Acknowledgments

This work is supported by the National Research Council of Canada, under grant
26143. We thank L. Boystov from CMU for sharing the posting list collection.

## References

  * Stepanov et al. [2011] A. A. Stepanov, A. R. Gangolli, D. E. Rose, R. J. Ernst, P. S. Oberoi,  SIMD-based decoding of posting lists,  in: Proceedings of the 20th ACM International Conference on Information and Knowledge Management, CIKM ’11, ACM, New York, NY, USA, 2011, pp. 317–326.
  * Dean [2009] J. Dean,  Challenges in building large-scale information retrieval systems: invited talk,  in: Proceedings of the Second ACM International Conference on Web Search and Data Mining, WSDM ’09, ACM, New York, NY, USA, 2009, pp. 1–1.
  * Plaisance et al. [2015] J. Plaisance, N. Kurz, D. Lemire,  Vectorized VByte Decoding,  in: iSWAG ’15, pp. 1–6. http://arxiv.org/abs/1503.07387.
  * Lemire et al. [2016] D. Lemire, L. Boytsov, N. Kurz,  SIMD compression and the intersection of sorted integers,  Softw. Pract. Exp. 46 (2016) 723–749.