11institutetext: CISPA Helmholtz Center for Information Security, Saarbrücken,
Germany
22institutetext: Azure Research, Microsoft, Cambridge, United Kingdom
33institutetext: Saarland University, Saarbrücken, Germany

# Automata-Based Software Model Checking of Hyperproperties††thanks: This work
was partially supported by the European Research Council (ERC) Grant HYPER
(No. 101055412).

Bernd Finkbeiner 11 Hadar Frenkel 11 Jana Hofmann Research carried out while
at CISPA Helmholtz Center for Information Security.22 Janine Lohse 33

###### Abstract

We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper
Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal
Logic (LTL) with memory cells, functions and predicates, making it a
convenient and expressive logic to reason over software and other systems with
infinite data domains. HyperTSL further extends TSL to the specification of
hyperproperties – properties that relate multiple system executions. As such,
HyperTSL can express information flow policies like noninterference in
software systems. We augment HyperTSL with theories, resulting in HyperTSL(T),
and build on methods from LTL software verification to obtain model checking
algorithms for TSL and HyperTSL(T). This results in a sound but necessarily
incomplete algorithm for specifications contained in the
$\forall^{*}\exists^{*}$ fragment of HyperTSL(T). Our approach constitutes the
first software model checking algorithm for temporal hyperproperties with
quantifier alternations that does not rely on a finite-state abstraction.

##  1 Introduction

Hyperproperties [20] generalize trace properties [2] to system properties,
i.e., properties that reason about a system in its entirety and not just about
individual execution traces. Hyperproperties comprise many important
properties that are not expressible as trace properties, e.g., information
flow policies [20], sensitivity and robustness of cyber-physical systems, and
linearizability in distributed computing [11]. For software systems, typical
hyperproperties are program refinement or fairness conditions such as
symmetry.

For the specification of hyperproperties, Linear Temporal Logic [48] (LTL) has
been extended with trace quantification, resulting in Hyper Linear Temporal
Logic [19] (HyperLTL). There exist several model checking algorithms for
HyperLTL [19, 35, 22], but they are designed for finite-state systems and are
therefore not directly applicable to software. Existing algorithms for
software verification of temporal hyperproperties (e.g., [9, 1]) are, with the
exception of [10], limited to universal hyperproperties, i.e., properties
without quantifier alternation.

In this paper, we develop algorithms for model checking software systems
against $\forall^{*}\exists^{*}$ hyperproperties. Our approach is
complementary to the recently proposed approach of [10]. They require to be
given a finite-state abstraction of the system, based on which they can both
prove and disprove $\forall^{*}\exists^{*}$ hyperproperties. We do not require
abstractions and instead provide sound but necessarily incomplete
approximations to detect counterexamples of the specification.

The class of $\forall^{*}\exists^{*}$ hyperproperties contains many important
hyperproperties like program refinement or _generalized noninterference_ [45].
Generalized noninterference states that it is impossible to infer the value of
a high-security input by observing the low-security outputs. Unlike
noninterference, it does not require the system to be deterministic.
Generalized noninterference can be expressed as
$\varphi_{gni}=\forall\pi\exists\pi^{\prime}.\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(i_{\pi^{\prime}}=\lambda\wedge
c_{\pi}=c_{\pi^{\prime}})$. The formula states that replacing the value of the
high-security input $i$ with some dummy value $\lambda$ does not change the
observable output $c$.

The above formula can only be expressed in HyperLTL if $i$ and $c$ range over
a finite domain. This is a real limitation in the context of software model
checking, where variables usually range over infinite domains like integers or
strings. To overcome this limitation, our specifications build on Hyper
Temporal Stream Logic (HyperTSL) [21]. HyperTSL replaces HyperLTL’s atomic
propositions with memory cells together with predicates and update terms over
these cells. Update terms use functions to describe how the value of a cell
changes from the previous to the current step. This makes the logic especially
suited for specifying software properties.

HyperTSL was originally designed for the synthesis of software systems, which
is why all predicates and functions are uninterpreted. In the context of model
checking, we have a concrete system at hand, so we should interpret functions
and predicates according to that system. We therefore introduce HyperTSL(T) –
HyperTSL with interpreted theories – as basis for our algorithms.

##### Overview

Following [39], we represent our system as a symbolic automaton labeled with
program statements. Not every trace of such an automaton is also a valid
program execution: for example, a trace
$\mathit{assert}(n=0)~{};n--;~{}(\mathit{assert}(n=0))^{\omega}$ 111The
superscript $\omega$ denotes an infinite repetition of the program statement.
cannot be a program execution, as the second assertion will always fail. Such
a trace is called infeasible. In contrast, in a feasible trace, all assertions
can, in theory, succeed. As a first step, we tackle TSL model checking (Sec.
4) by constructing a program automaton whose feasible accepted traces
correspond to program executions that violate the TSL specification. To do so,
we adapt the algorithm of [26], which constructs such an automaton for LTL,
combining the given program automaton and an automaton for the negated
specification.

We then extend this algorithm for HyperTSL(T) formulas without quantifier
alternation (Sec. 5.1) by applying self-composition, a technique commonly used
for the verification of hyperproperties [6, 5, 29].

Next, in Sec. 5.2, we further extend this algorithm to finding counterexamples
for $\forall^{*}\exists^{*}$-HyperTSL(T) specifications (and, dually,
witnesses for $\exists^{*}\forall^{*}$ formulas). We construct an automaton
that over-approximates the combinations of program executions that satisfy the
existential part of the formula. If some program execution is not included in
the over-approximation, this execution is a counterexample proving that the
program violates the specification.

More concretely, for a HyperTSL(T) formula $\forall^{m}\exists^{n}\psi$, we
construct the product of the automaton for $\psi$ and the $n$-fold self-
composition of the program automaton. Every feasible trace of this product
corresponds to a choice of executions for the variables
$\pi_{1},\dots,\pi_{n}$ such that $\psi$ is satisfied. Next, we remove (some)
spurious witnesses by removing infeasible traces. We consider two types of
infeasibility: $k$-infeasibility, that is, a local inconsistency in a trace
appearing within $k$ consecutive timesteps; and infeasibility that is not
local, and is the result of some infeasible accepting cycles in the automaton.
In the next step, we project the automaton to the universally quantified
traces, obtaining an over-approximation of the trace combinations satisfying
the existential part of the formula. Finally, all that remains to check is
whether the over-approximation includes all combinations of feasible traces.

Lastly, in Sec. 6, we demonstrate our algorithm for two examples, including
generalized noninterference.

##### Contributions.

We present an automata-based algorithm for software model checking of
$\forall^{*}\exists^{*}$-hyperproperties. We summarize our contributions as
follows.

  * •

We extend HyperTSL with theories, a version of HyperTSL that is suitable for
model checking.

  * •

We adapt the approach of [26] to TSL(T) and alternation-free HyperTSL(T), and
thereby suggest the first model checking algorithm for both TSL(T) and
HyperTSL(T).

  * •

We further extend the algorithm for disproving $\forall^{*}\exists^{*}$
hyperproperties and proving $\exists^{*}\forall^{*}$ hyperproperties using a
feasibility analysis.

####  1.0.1 Related Work

Temporal stream logic extends linear temporal logic [48] and was originally
designed for synthesis [33]. For synthesis, the logic has been successfully
applied to synthesize the FPGA game ‘Syntroids’ [37], and to synthesize smart
contracts [32]. To advance smart contract synthesis, TSL has been extended to
HyperTSL in [21]. The above works use a version TSL that leaves functions and
predicates uninterpreted. While this choice is very well suited for the
purpose of synthesis, for model checking it makes more sense to use the
interpretation of the program at hand. TSL was extended with theories in [31],
which also analyzed the satisfiability problem of the logic. Neither TSL nor
HyperTSL model checking has been studied so far (with or without interpreted
theories).

For LTL, the model checking problem for infinite-state models has been
extensively studied, examples are [24, 13, 16, 26, 36]. Our work builds on the
automata-based LTL software model checking algorithm from [26]. There are also
various algorithms for verifying universal hyperproperties on programs, for
example, algorithms based on type theory [9, 1]. Major related work is [10],
which (in contrast to our approach) requires on predicate abstractions to
model check software against $\forall^{*}\exists^{*}$ HyperLTL specifications.
They can also handle asynchronous hyperproperties, which is currently beyond
our scope. Another proposal for the verification of $\forall\exists$
hyperproperties on software is [50]. Here, generalized constrained horn
clauses are used to verify functional specifications. The approach is not
applicable to reactive, non-terminating programs. Recently, it was also
proposed to apply model checkers for TLA (a logic capable of expressing
software systems as well as their properties) to verify
$\forall^{*}\exists^{*}$ hyperproperties [43].

Beyond the scope of software model checking, the verification of
hyperproperties has been studied for various system models and classes of
hyperproperties. There exist model checking algorithms for $\omega$-regular
properties [35, 30] and asynchronous hyperproperties [7, 12] in finite-state
Kripke structures, as well as timed systems [41], real-valued [47] and
probabilistic hyperproperties [3, 27, 28] (some of which study combinations of
the above).

##  2 Preliminaries

##### A Büchi Automaton

is a tuple $\mathcal{A}=(\Sigma,Q,\delta,q_{0},F)$ where $\Sigma$ is a finite
alphabet; $Q$ is a set of states; $\delta\subseteq Q\times\Sigma\times Q$ is
the transition relation; $q_{0}\in Q$ is the initial state; and $F\subseteq Q$
is the set of accepting states. A _run_ of the Büchi automaton $\mathcal{A}$
on a word $\sigma\in\Sigma^{\omega}$ is an infinite sequence
$q_{0}~{}q_{1}~{}q_{2}\dots\in Q^{\omega}$ of states such that for all
$i\in\mathbb{N},(q_{i},\sigma_{i},q_{i+1})\in\delta$. An infinite word
$\sigma$ is _accepted_ by $\mathcal{A}$ if there is a run on $\sigma$ with
infinitely many $i\in\mathbb{N}$ such that $q_{i}\in F$. The language of
$\mathcal{A}$, $\mathcal{L}(\mathcal{A})$, is the set of words accepted by
$\mathcal{A}$.

###  2.1 Temporal Stream Logic Modulo Theories TSL(T)

Temporal Stream Logic (TSL) [33] extends Linear Temporal Logic (LTL) [48] by
replacing Boolean atomic propositions with predicates over memory cells and
inputs, and with update terms that specify how the value of a cell should
change.

We present the formal definition of TSL modulo theories – TSL(T), based on the
definition of [31], which extends the definition [33]. The definition we
present is due to [44] and it slightly differs from the definition of [31];
The satisfaction of an update term is not defined by syntactic comparison, but
relative to the current and previous values of cells and inputs. This
definition suites the setting of model checking, where a concrete model is
given.

TSL(T) is defined based on a set of values $\mathbb{V}$ with
$\mathit{true},\mathit{false}\in\mathbb{V}$, a set of inputs $\mathbb{I}$ and
a set of memory cells $\mathbb{C}$. Update terms and predicates are
interpreted with respect to a given theory. A _theory_ is a tuple
$(\mathbb{F},\varepsilon)$, where $\mathbb{F}$ is a set of function symbols;
$\mathbb{F}_{n}$ is the set of functions of arity $n$; and
$\varepsilon:\left(\bigcup_{n\in\mathbb{N}}\mathbb{F}_{n}\times\mathbb{V}^{n}\right)\rightarrow\mathbb{V}$
is the interpretation function, evaluating a function with arity $n$. For our
purposes, we assume that every theory
$(\mathcal{T}_{\mathcal{F}},\varepsilon)$ contains at least
$\\{=,\vee,\neg\\}$ with their usual interpretations.

A _function term_ $\tau_{F}$ is defined by the grammar

$\displaystyle\tau_{F}::=c~{}|~{}i~{}|~{}f(\tau_{F},~{}\tau_{F},~{}\dots~{}\tau_{F})$

where $c\in\mathbb{C},i\in\mathbb{I},f\in\mathbb{F}$, and the number of
elements in $f$ matches its arity. An _assignment_
$a:(\mathbb{I}\cup\mathbb{C})\rightarrow\mathbb{V}$ is a function assigning
values to inputs and cells. We denote the set of all assignments by
$\mathsf{A}$. Given a concrete assignment, we can compute the value of a
function term.

The _evaluation function_
$\eta:\mathcal{T}_{\mathcal{F}}\times\mathsf{A}\rightarrow\mathbb{V}$ is
defined as

$\displaystyle\eta(c,a)$ $\displaystyle=a(c)$ $\displaystyle\text{for
}c\in\mathbb{C}$ $\displaystyle\eta(i,a)$ $\displaystyle=a(i)$
$\displaystyle\text{for }i\in\mathbb{I}$
$\displaystyle\eta(f~{}(\tau_{F1},\tau_{F2},\dots,\tau_{Fn}),a)$
$\displaystyle=\varepsilon(f,(\eta(\tau_{F1}),\eta(\tau_{F2}),\dots,\eta(\tau_{Fn})))$
$\displaystyle\text{for }f\in\mathbb{F}$

A _predicate term_ $\tau_{P}$ is a function term only evaluating to _true_ or
_false_. We denote the set of all predicate terms by $\mathcal{T}_{P}$.

For $c\in\mathbb{C}$ and $\tau_{F}\in\mathcal{T}_{\mathcal{F}}$, $\llbracket
c\leftarrowtail\tau_{F}\rrbracket$ is called an _update term_. Intuitively,
the update term $\llbracket c\leftarrowtail\tau_{F}\rrbracket$ states that $c$
should be updated to the value of $\tau_{F}$. If in the previous time step
$\tau_{F}$ evaluated to $v\in\mathbb{V}$, then in the current time step $c$
should have value $v$. The set of all update terms is $\mathcal{T}_{U}$. TSL
formulas are constructed as follows, for
$c\in\mathbb{C},\tau_{P}\in\mathcal{T}_{P},\tau_{F}\in\mathcal{T}_{\mathcal{F}}$.

$\varphi::=\tau_{P}~{}|~{}\llbracket
c\leftarrowtail\tau_{F}\rrbracket~{}|~{}\neg\varphi~{}|~{}\varphi\wedge\varphi~{}|~{}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi~{}|~{}\varphi\operatorname{\mathcal{U}}\varphi~{}$

The usual operators $\vee,\operatorname{\leavevmode\hbox to8.7pt{\vbox
to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ (“eventually”), and
$\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ (“globally”) can be
derived using the equations
$\varphi\vee\psi=\neg(\neg\varphi\wedge\neg\psi),~{}\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi=\mathit{true}\,\operatorname{\mathcal{U}}\varphi$
and $\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi=\neg\operatorname{\leavevmode\hbox
to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\varphi$.

Assume a fixed initial variable assignment $\zeta_{-1}$ (e.g., setting all
values to zero). The satisfaction of a TSL(T) formula with respect to a
computation $\zeta\in\mathsf{A}^{\omega}$ and a time point $t$ is defined as
follows, where we define $\zeta\models\varphi$ as $0,\zeta\models\varphi$.

$\displaystyle t,\zeta\models\tau_{P}$
$\displaystyle\Leftrightarrow\eta(\tau_{P},\zeta_{t})=\mathit{true}$
$\displaystyle t,\zeta\models\llbracket c\leftarrowtail\tau_{F}\rrbracket$
$\displaystyle\Leftrightarrow\eta(\tau_{F},\zeta_{t-1})=\zeta_{t}(c)$
$\displaystyle t,\zeta\models\neg\varphi$
$\displaystyle\Leftrightarrow\neg(t,\zeta\models\varphi)$ $\displaystyle
t,\zeta\models\varphi\wedge\psi$ $\displaystyle\Leftrightarrow
t,\zeta\models\varphi\text{ and }t,\zeta\models\psi$ $\displaystyle
t,\zeta\models\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$
$\displaystyle\Leftrightarrow t+1,\zeta\models\varphi$ $\displaystyle
t,\zeta\models\varphi\operatorname{\mathcal{U}}\psi$
$\displaystyle\Leftrightarrow\exists t^{\prime}\geq
t.~{}t^{\prime},\zeta\models\psi\text{ and }\forall t\leq
t^{\prime\prime}<t^{\prime}.~{}t^{\prime\prime},\zeta\models\varphi$

##  3 HyperTSL Modulo Theories

In this section, we introduce HyperTSL(T), HyperTSL with theories, which
enables us to interpret predicates and functions depending on the program at
hand. In [21], two versions of HyperTSL are introduced: HyperTSL and
HyperTSLrel. The former is a conservative extension of TSL to hyperproperties,
meaning that predicates only reason about a single trace. In HyperTSLrel,
predicates may relate multiple traces, which opens the door to expressing
properties like noninterference in infinite domains. Here, we build on
HyperTSLrel, allowing, in addition, update terms ranging over multiple traces.
Furthermore, we extend the originally uninterpreted functions and predicates
with an interpretation over theories. We denote this logic by HyperTSL(T).

The syntax of HyperTSL(T) is that of TSL(T), with the addition that cells and
inputs are now each assigned to a trace variable that represents a
computation. For example, $c_{\pi}$ now refers to the memory cell $c$ in the
computation represented by the trace $\pi$. Formally, let $\Pi$ be a set of
trace variables. We define a hyper-function term
$\hat{\tau_{F}}\in\hat{\mathcal{T}_{F}}$ as a function term using
$(\mathbb{I}\times\Pi)$ as the set of inputs and $(\mathbb{C}\times\Pi)$ as
the set of cells.

###### Definition 1

A _hyper-function term_ $\hat{\tau_{F}}$ is defined by the grammar

$\hat{\tau_{F}}::=c_{\pi}~{}|~{}i_{\pi}~{}|~{}f(\hat{\tau_{F}},~{}\hat{\tau_{F}},~{}\dots~{}\hat{\tau_{F}})$

where
$c_{\pi}\in\mathbb{C}\times\Pi,i_{\pi}\in\mathbb{I}\times\Pi,f\in\mathbb{F}$,
and the number of the elements in the tuple matches the function arity. We
denote by $\hat{\mathcal{T}_{F}}$ the set of all hyper-function terms.

Analogously, we define hyper-predicate terms
$\hat{\tau_{P}}\in\hat{\mathcal{T}_{P}}$ as hyper-function terms evaluating to
_true_ or _false_ ; hyper-assignments
$\hat{\mathsf{A}}=(\mathbb{I}\cup\mathbb{C})\times\Pi\rightarrow\mathbb{V}$ as
functions mapping cells and inputs of each trace to their current values;
hyper-computations $\hat{\zeta}\in\hat{\mathsf{A}}^{\omega}$ as hyper-
assignment sequences. See Fig. 1 for an example.

$s_{0}$$s_{1}$$s_{2}$c=0c=1c=1c=2

$\displaystyle\pi:=(c=0)~{}(c=1)^{\omega},~{}\pi^{\prime}:=((c=0)~{}(c=1)~{}(c=2))^{\omega}$
$\displaystyle\hat{a}_{1}:\\{c_{\pi}\mapsto 0,c_{\pi^{\prime}}\mapsto
0\\},\hat{a}_{2}:\\{c_{\pi}\mapsto 1,c_{\pi^{\prime}}\mapsto 1\\}$
$\displaystyle\hat{a}_{3}:\\{c_{\pi}\mapsto 1,c_{\pi^{\prime}}\mapsto
2\\},\hat{a}_{4}:\\{c_{\pi}\mapsto 1,c_{\pi^{\prime}}\mapsto 0\\}$

Figure 1: Left: A program automaton. Right: two traces $\pi$ and
$\pi^{\prime}$ of the program automaton. We interpret each trace as a
computation. When executing both traces simultaneously, every time point has a
corresponding hyper-assignment that assigns values to $c_{\pi}$ and
$c_{\pi^{\prime}}$. Those for the first four time steps are shown on the
right. Together, they define the hyper-computation
$\hat{\zeta}:=\hat{a}_{1}(\hat{a}_{2}~{}\hat{a}_{3}~{}\hat{a}_{4})^{\omega}$,
matching $\pi$ and $\pi^{\prime}$.

###### Definition 2

Let
$c_{\pi}\in\mathbb{C}\times\Pi,\hat{\tau_{P}}\in\hat{\mathcal{T}_{P}},\hat{\tau_{F}}\in\hat{\mathcal{T}_{F}}$.
A _HyperTSL(T) formula_ is defined by the following grammar:

$\displaystyle\varphi$
$\displaystyle::=\psi~{}|~{}\forall\pi.~{}\varphi~{}|~{}\exists\pi.~{}\varphi$
$\displaystyle\psi$ $\displaystyle::=\hat{\tau_{P}}~{}|~{}\llbracket
c_{\pi}\leftarrowtail\hat{\tau_{F}}\rrbracket~{}|~{}\neg\psi~{}|~{}\psi\wedge\psi~{}|~{}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi~{}|~{}\psi\operatorname{\mathcal{U}}\psi~{}$

To define the semantics of HyperTSL(T), we need the ability to extend a hyper-
computation to new trace variables, one for each path quantifier. Let
$\hat{\zeta}\in\hat{\mathsf{A}}^{\omega}$ be a hyper-computation, and let
$\pi,\pi^{\prime}\in\Pi,\zeta\in\mathsf{A}^{\omega}$ and
$x\in(\mathbb{I}\cup\mathbb{C})$. We define the extension of $\hat{\zeta}$ by
$\pi$ using the computation $\zeta$ as
$\hat{\zeta}[\pi,\zeta]~{}(x_{\pi^{\prime}})=\hat{\zeta}(x_{\pi^{\prime}})$
for $\pi^{\prime}\neq\pi$, and
$\hat{\zeta}[\pi,\zeta]~{}(x_{\pi})=\zeta(x_{\pi})$ for $\pi$.

###### Definition 3

The _satisfaction of a HyperTSL(T)-Formula_ w.r.t. a hyper- computation
$\hat{\zeta}\in\hat{\mathsf{A}}^{\omega}$, a set of computations $Z$ and a
time point $t$ is defined by

$\displaystyle t,Z,\hat{\zeta}\models\forall\pi.~{}\varphi$
$\displaystyle\Leftrightarrow\forall\zeta\in
Z.~{}t,~{}Z,~{}\hat{\zeta}[\pi,\zeta]\models\varphi$ $\displaystyle
t,Z,\hat{\zeta}\models\exists\pi.~{}\varphi$
$\displaystyle\Leftrightarrow\exists\zeta\in
Z.~{}t,~{}Z,~{}\hat{\zeta}[\pi,\zeta]\models\varphi$

The cases that do not involve path quantification are analogous to those of
TSL(T) as defined in Sec. 2.1. We define $Z\models\varphi$ as
$0,Z,\emptyset^{\omega}\models\varphi$.

##  4 Büchi Product Programs and TSL Model Checking

We now describe how we model the system and specification as Büchi automata,
adapting the automata of [26] to the setting of TSL. Then, we introduce our
model checking algorithm for TSL(T). In Sec 5.2 we build on this algorithm to
propose an algorithm for HyperTSL(T) model checking.

We use a symbolic representation of the system (see, for example, [39]), where
transitions are labeled with program statements, and all states are accepting.

###### Definition 4

Let $c\in\mathbb{C},\tau_{P}\in\mathcal{T}_{P}$ and
$\tau_{F}\in\mathcal{T}_{\mathcal{F}}$. We define the set of _(basic) program
statements_ as

$\displaystyle s_{0}$
$\displaystyle::=\mathit{assert}(\tau_{P})~{}|~{}c:=\tau_{F}~{}|~{}c:=*$
$\displaystyle s$ $\displaystyle::=s_{0}~{}|~{}s;s$

We call statements of the type $s_{0}$ _basic program statements_ , denoted by
$\mathit{Stmt}_{0}$; statements of type $s$ are denoted by $\mathit{Stmt}$.
The assignment $c:=*$ means that any value could be assigned to $c$.

A program automaton $\mathcal{P}$ is a Büchi automaton with
$\Sigma=\mathit{Stmt}$, that is,
$\mathcal{P}=(\mathit{Stmt},Q,q_{0},\delta,F)$ and $\delta\subseteq
Q\times\mathit{Stmt}\times Q$. When modeling the system we only need basic
statements, thus we have $\mathit{Stmt}=\mathit{Stmt}_{0}$; and $F=Q$ as all
states are accepting. See Fig. 1 for an illustration.

Using a program automaton, one can model `if` statements, `while` loops, and
non-deterministic choices. However, not every trace of the program automaton
corresponds to a program execution. For example, the trace
$(n:=\mathit{input}_{1});\mathit{assert}(n>0);\mathit{assert}(n<0);~{}\mathit{assert}(true)^{\omega}$
does not – the second assertion will always fail. Such a trace is called
infeasible. We call a trace feasible if it corresponds to a program execution
where all the assertions may succeed. We now define this formally.

###### Definition 5

A computation $\zeta$ _matches_ a trace $\sigma\in\mathit{Stmt}_{0}^{\omega}$
at time point $t$, denoted by $\zeta\smalltriangleleft_{t}\sigma$, if the
following holds:

$\displaystyle\text{if }\sigma_{t}=\mathit{assert}(\tau_{P}):$
$\displaystyle\eta(\tau_{P},\zeta_{t-1})=true~{}\text{ and }~{}\forall
c\in\mathbb{C}.~{}\zeta_{t}(c)=\zeta_{t-1}(c)$ $\displaystyle\text{if
}\sigma_{t}=c:=\tau_{F}:$
$\displaystyle\eta(\tau_{F},\zeta_{t-1})=\zeta_{t}(c)~{}\text{ and }~{}\forall
c^{\prime}\in\mathbb{C}\backslash\\{c\\}.~{}\zeta_{t}(c^{\prime})=\zeta_{t-1}(c^{\prime})$
$\displaystyle\text{if }\sigma_{t}=c:=*:$ $\displaystyle\forall
c\in\mathbb{C}\backslash\\{c\\}.~{}\zeta_{t}(c)=\zeta_{t-1}(c)$

where $\zeta_{-1}$ is the initial assignment. A computation $\zeta$ matches a
trace $\sigma\in\mathit{Stmt}_{0}^{\omega}$, denoted by
$\zeta\smalltriangleleft\sigma$, if $\forall
t\in\mathbb{N}.~{}\zeta\smalltriangleleft_{t}\sigma$.

###### Definition 6

A program automaton $\mathcal{P}$ over $\mathit{Stmt}_{0}$ satisfies a
TSL(T)-formula $\varphi$, if for all traces $\sigma$ of $P$ we have
$\forall\zeta\in\mathsf{A}^{\omega}.~{}\zeta\smalltriangleleft\sigma\Rightarrow\zeta\models\varphi$.

We now present an algorithm to check whether a program automaton $\mathcal{P}$
satisfies a TSL(T) formula. It is an adaption of the automaton-based LTL
software model checking approach by [26], where the basic idea is to first
translate the negated specification $\varphi$ into an automaton
$\mathcal{A}_{\neg\varphi}$, and then combine $\mathcal{A}_{\neg\varphi}$ and
$\mathcal{P}$ to a new automaton, namely the Büchi program product. The
program satisfies the specification iff the Büchi program product accepts no
feasible trace.

In [26], the Büchi program product is constructed similarly to the standard
product automata construction. To ensure that the result is again a program
automaton, the transitions are not labeled with pairs
$(s,l)\in\mathit{Stmt}_{0}\times 2^{AP}$, but with the program statement
$(s;~{}\mathit{assert}(l))$. A feasible accepted trace of the Büchi program
product then corresponds to a counterexample proving that the program violates
the specification. In the following, we discuss how we adapt the construction
of the Büchi program product for TSL(T) such that this property – a feasible
trace corresponds to a counterexample – remains true for TSL(T).

Let $\varphi$ be a TSL(T) specification. For the construction of
$\mathcal{A}_{\neg\varphi}$, we treat all update and predicate terms as atomic
propositions, resulting in an LTL formula $\neg\varphi_{\textit{LTL}}$, which
is translated to a Büchi automaton.222For the translation of LTL formulas to
Büchi automata, see, for example, [46, 4, 49]. For our version of the Büchi
program product, we need to merge a transition label $s$ from $\mathcal{P}$
with a transition label $l$ from $\mathcal{A}_{\neg\varphi_{\textit{LTL}}}$
into a single program statement such that the assertion of the combined
statement succeeds iff $l$ holds for the statement $s$. Note that $l$ is a set
of update and predicate terms. For the update terms $\llbracket
c\leftarrowtail\tau_{F}\rrbracket$ we cannot just use an assertion to check if
they are true, as we need to ‘save’ the value of $\tau_{F}$ before the
statement $s$ is executed.

Our setting differs from [26] also in the fact that their program statements
do not reason over input streams. We model the behavior of input streams by
using fresh memory cells that are assigned a new value at every time step. In
the following, we define a function $\mathit{combine}$ that combines a program
statement $s$ and a transition label $l$ to a new program statement as
described above.

###### Definition 7

Let $\upsilon=\\{\llbracket
c_{1}\leftarrowtail\tau_{F1}\rrbracket,\dots,\llbracket
c_{n}\leftarrowtail\tau_{Fn}\rrbracket\\}$ be the set of update terms
appearing in $\varphi$, let $\rho$ be the set of predicate terms appearing in
$\varphi$. Let $l\subseteq(\upsilon\cup\rho)$ be a transition label of
$\mathcal{A}_{\neg\varphi}$. Let $(tmp_{j})_{j\in\mathbb{N}}$ be a family of
fresh cells. Let $\mathbb{I}=\\{i_{1},\dots i_{m}\\}$. We define the function
$\mathit{combine}:\mathit{Stmt}\times\mathcal{P}(\mathcal{T}_{P}\cup\mathcal{T}_{U})\rightarrow\mathit{Stmt}$
as follows. The result of $\mathit{combine}(s,l)$ is composed of the program
statements in
$\mathit{save\\_values}_{l},s,\mathit{new\\_inputs},\mathit{check\\_preds}_{l}$
and $\mathit{check\\_updates}_{l}$. Then we have:

$\displaystyle\mathit{save\\_values}$
$\displaystyle:=\mathit{tmp}_{1}:=\tau_{F1};~{}\dots;\mathit{tmp}_{n}:=\tau_{Fn}$
$\displaystyle\mathit{new\\_inputs}$
$\displaystyle:=i_{1}:=*;~{}\dots~{};i_{m}:=*$
$\displaystyle\mathit{check\\_preds}_{l}$
$\displaystyle:=assert\left(\bigwedge_{\tau_{P}\in
l}\tau_{P}\wedge\bigwedge_{\tau_{P}\in\rho\backslash l}\neg\tau_{P}\right)$
$\displaystyle\mathit{check\\_updates}_{l}$
$\displaystyle:=assert\left(\bigwedge_{\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon}\begin{cases}c_{j}=\mathit{tmp}_{j}&\text{if
}\llbracket c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in l\\\
c_{j}\neq\mathit{tmp}_{j}&\text{else}\end{cases}\right)$
$\displaystyle\mathit{combine}(s,l)$
$\displaystyle:=\mathit{save\\_values};~{}s;~{}\mathit{new\\_inputs};~{}\mathit{check\\_preds}_{l};~{}\mathit{check\\_updates}_{l}$

We can extend this definition to combining traces instead of single transition
labels. This leads to a function
$\mathit{combine}:\mathit{Stmt}^{\omega}\times\mathcal{P}(\mathcal{T}_{P}\cup\mathcal{T}_{U})^{\omega}\rightarrow\mathit{Stmt}^{\omega}$.
Note that the result of $\mathit{combine}$ is again a program statement in
$\mathit{Stmt}$ (or a trace $\mathit{Stmt}^{\omega}$) over the new set of
cells $\mathbb{C}\cup\mathbb{I}\cup(tmp_{j})_{j\in\mathbb{N}}$, which we call
$\mathbb{C}^{*}$.

###### Example 1

Let $\mathbb{I}=\\{i\\}$. Then the result of
$\mathit{combine}(n:=42,\\{\llbracket n\leftarrowtail n+7\rrbracket,n>0\\})$
is
$\mathit{tmp}_{0}:=n+7;~{}n:=42;~{}i:=*;~{}\mathit{assert}(n>0);~{}\mathit{assert}(n=\mathit{tmp}_{0})$.

As $\mathit{combine}$ leads to composed program statements, we now need to
extend the definition of feasibility to all traces. To do so, we define a
function
$\mathit{flatten}:\mathit{Stmt}^{\omega}\rightarrow{\mathit{Stmt}_{0}}^{\omega}$
that takes a sequence of program statements and transforms it into a sequence
of basic program statements by converting a composed program statement into
multiple basic program statements.

###### Definition 8

A trace $\sigma\in\mathit{Stmt}^{\omega}$ _matches_ a computation $\zeta$,
denoted by $\zeta\smalltriangleleft\sigma$ if
$\zeta\smalltriangleleft\mathit{flatten}(\sigma)$. A trace $\sigma$ is
_feasible_ if there is a computation $\zeta$ such that
$\zeta\smalltriangleleft\sigma$.

###### Definition 9

(Combined Product) Let $\mathcal{P}=(Stmt,Q,q_{0},\delta,Q)$ be a program
automaton and
$\mathcal{A}=(\mathcal{P}(\mathcal{T}_{P}\cup\mathcal{T}_{U}),Q^{\prime},q_{0}^{\prime},\delta^{\prime},F^{\prime})$
be a Büchi automaton (for example, the automaton
$\mathcal{A}_{\neg\varphi_{LTL}}$). The combined product
$\mathcal{P}\otimes\mathcal{A}$ is an automaton $\mathcal{B}=(Stmt,Q\times
Q^{\prime},(q_{0},q_{0}^{\prime}),\delta_{B},F_{B})$, where

$\displaystyle F_{B}$ $\displaystyle=\\{(q,q^{\prime})\mid q\in Q\wedge
q^{\prime}\in F^{\prime}\\}$ $\displaystyle\delta_{B}$
$\displaystyle=\\{((p,q),\mathit{combine}(s,l),(p^{\prime},q^{\prime}))~{}|~{}(p,s,p^{\prime})\in\delta\wedge(q,l,q^{\prime})\in\delta^{\prime}\\}$

###### Theorem 4.1

Let $\mathcal{P}$ be a program automaton over $\mathit{Stmt}_{0}$. Let
$\varphi$ be a TSL(T) formula. Then $\mathcal{P}$ satisfies $\varphi$ if and
only if $\mathcal{P}\otimes\mathcal{A}_{\neg\varphi_{LTL}}$ has no feasible
trace.

######  Proof (sketch)

If $\zeta\smalltriangleleft\sigma$ is a counterexample, we can construct a
computation $\tilde{\zeta}$ that matches the corresponding combined trace in
$\mathcal{P}\otimes\mathcal{A}_{\neg\varphi_{LTL}}$, and vice versa. The
formal construction is given in App. 0.A.4.

We can now apply Thm. 4.1 to solve the model checking problem by testing
whether $\mathcal{P}\otimes\mathcal{A}_{\neg\varphi_{LTL}}$ does not accept
any feasible trace, using the feasibility check in [26] as a black box. The
algorithm of [26] is based on counterexample-guided abstraction refinement
(CEGAR [18]). Accepted traces are checked for feasibility. First, finite
prefixes of the trace are checked using an SMT-solver. If they are feasible, a
ranking function synthesizer is used to check whether the whole trace
eventually terminates. If the trace is feasible, it serves as a
counterexample. If not, the automaton is refined such that it now does not
include the spurious counterexample trace anymore, and the process is
repeated. For more details, we refer to [26]. The limitations of SMT-solvers
and ranking function synthesizers also limit the functions and predicates that
can be used in both the program and in the TSL(T) formula.

##  5 HyperTSL(T) Model Checking

We now turn to the model checking problem of HyperTSL(T). We start with
alternation-free formulas and continue with $\forall^{*}\exists^{*}$ formulas.

###  5.1 Alternation-free HyperTSL(T)

In this section, we apply the technique of self-composition to extend the
algorithm of Sec. 4 to alternation-free HyperTSL(T). First, we define what it
means for a program automaton to satisfy a HyperTSL(T) formula.

###### Definition 10

Let $\mathcal{P}$ be a program automaton over $\mathit{Stmt}_{0}$, let
$\varphi$ be a HyperTSL(T) formula and let
$Z=\\{\zeta\in\mathsf{A}^{\omega}~{}|~{}\exists\sigma.~{}\zeta\smalltriangleleft\sigma\text{
and }\sigma\text{ is a trace of }\mathcal{P}\\}$. We say that $\mathcal{P}$
_satisfies_ $\varphi$ if $Z\models\varphi$.

###### Definition 11

Let $\mathcal{P}=(\mathit{Stmt},Q,q_{0},\delta,Q)$ be a program automaton. The
_$n$ -fold self-composition_ of $\mathcal{P}$ is
$\mathcal{P}^{n}=(\mathit{Stmt}^{\prime},Q^{n},q_{0}^{n},\delta^{n},Q^{n})$,
where $\mathit{Stmt}^{\prime}$ are program statements over the set of inputs
$\mathbb{I}\times\Pi$ and the set of cells $\mathbb{C}\times\Pi$ and where
$Q^{n}=Q\times\dots\times Q$, $q_{0}^{n}=(q_{0},\dots,q_{0})$ and

$\displaystyle\delta^{n}=$
$\displaystyle\\{((q_{1},\dots,q_{n}),((s_{1})_{\pi_{1}};\dots;(s_{n})_{\pi_{n}}),(q_{1}^{\prime},\dots,q_{n}^{\prime}))$
$\displaystyle\quad\mid\forall 1\leq i\leq
n.~{}(q_{i},s_{i},q_{i}^{\prime})\in~{}\delta\\}$

where $(s)_{\pi}$ renames every cell $c$ used in $s$ to $c_{\pi}$ and every
input $i$ to $i_{\pi}$.

###### Theorem 5.1

A program automaton $\mathcal{P}$ over $\mathit{Stmt}_{0}$ satisfies a
universal HyperTSL(T) formula
$\varphi=\forall\pi_{1}.~{}\dots\forall\pi_{n}.~{}\psi$ iff
$\mathcal{P}^{n}\otimes\mathcal{A}_{\neg\psi_{LTL}}$ has no feasible trace.

###### Theorem 5.2

A program automaton $P$ over $\mathit{Stmt}_{0}$ satisfies an existential
HyperTSL(T) formula $\varphi=\exists\pi_{1}.~{}\dots\exists\pi_{n}.~{}\psi$
iff $\mathcal{P}^{n}\otimes\mathcal{A}_{\psi_{LTL}}$ has some feasible trace.

The proofs of are analogous to the proof of Thm. 4.1 and are provided in App.
0.A.5.

###  5.2  $\forall^{*}\exists^{*}$ HyperTSL(T)

In this section, we present a sound but necessarily incomplete algorithm for
finding counterexamples for $\forall^{*}\exists^{*}$ HyperTSL(T)
formulas.333Note that the algorithms of Sec. 4 and Sec. 5.1 are also
incomplete, due to the feasibility test. However, the incompleteness of the
algorithm we provide in this section is inherent to the quantifier alternation
of the formula. Such an algorithm can also provide witnesses
$\exists^{*}\forall^{*}$ formulas. As HyperTSL(T) is built on top of HyperLTL,
we combine ideas from finite-state HyperLTL model checking [35] with the
algorithms of Sec. 4 and Sec. 5.1.

Let $\varphi=\forall^{m}\exists^{n}.\psi$. For HyperLTL model checking, [35]
first constructs an automaton containing the system traces satisfying
$\psi_{\exists}:=\exists^{n}.\psi$, and then applies complementation to
extract counterexamples for the $\forall\exists$ specification. Consider the
automaton $\mathcal{P}^{n}\otimes\mathcal{A}_{\psi_{LTL}}$ from Sec. 4, whose
feasible traces correspond to the system traces satisfying $\psi_{\exists}$.
If we would be able to remove all infeasible traces, we could apply the
finite-state HyperLTL model checking construction. Unfortunately, removing all
infeasibilities is impossible in general, as the result would be a finite-
state system describing exactly an infinite-state system. Therefore, the main
idea of this section is to remove parts of the infeasible traces from
$\mathcal{P}^{n}\otimes\mathcal{A}_{\psi_{LTL}}$, constructing an over-
approximation of the system traces satisfying $\psi_{\exists}$. A
counterexample disproving $\varphi$ is then a combination of system traces
that is not contained in the over-approximation.

We propose two techniques for removing infeasibility. The first technique
removes k-infeasibility from the automaton, that is, a local inconsistency in
a trace, occurring within $k$ consecutive time steps. When choosing $k$, there
is a tradeoff: if $k$ is larger, more counterexamples can be identified, but
the automaton construction gets exponentially larger.

The second technique removes infeasible accepting cycles from the automaton.
It might not be possible to remove all of them, thus we bound the number of
iterations. We present an example and then elaborate on these two methods.

###### Example 2

The trace $t_{1}$ below is 3-infeasible, because regardless of the value of
$n$ prior to the second time step, the assertion in the fourth time step will
fail.

$t_{1}=(n--;~{}\mathit{assert}(n>=0))~{}(n:=1;~{}\mathit{assert}(n>=0))~{}(n--;~{}\mathit{assert}(n>=0))^{\omega}$

In contrast, the trace
$t_{2}=(n:=*)~{}(n--;~{}\mathit{assert}(n>=0))^{\omega}$ is not $k$-infeasible
for any $k$, because the value of $n$ can always be large enough to pass the
first $k$ assertions. Still, the trace is infeasible because $n$ cannot
decrease forever without dropping below zero. If such a trace is accepted by
an automaton, $n--;~{}\mathit{assert}(n>=0)$ corresponds to an infeasible
accepting cycle.

####  5.2.1 Removing $k$-infeasibility

To remove $k$-infeasibility from an automaton, we construct a new program
automaton that ‘remembers’ the $k-1$ previous statements. The states of the
new automaton correspond to paths of length $k$ in the original automaton. We
add a transition labeled with $l$ between two states $p$ and $q$ if we can
extend the trace represented by $p$ with $l$ such that the resulting trace is
$k$-feasible. Formally, we get:

###### Definition 12

Let $k\in\mathbb{N}$, $\sigma\in\mathit{Stmt}^{\omega}$. We say that $\sigma$
is _$k$ -infeasible_ if there exists $j\in\mathbb{N}$ such that
$\sigma_{j}\sigma_{j+1}\dots\sigma_{j+k-1};\mathit{assert}(true)^{\omega}$ is
infeasible for all possible initial assignments $\zeta_{-1}$. We then also
call the subsequence $\sigma_{j}\sigma_{j+1}\dots\sigma_{j+k-1}$ infeasible.
If a trace is not $k$-infeasible, we call it $k$-feasible.444Whether a
subsequence $\sigma_{j}\sigma_{j+1}\dots\sigma_{j+k-1}$ is a witness of
k-infeasibility can be checked using an SMT-solver, e.g, [25, 14, 15, 17].

###### Definition 13

Let $\mathcal{P}=(\mathit{Stmt},Q,q_{0},\delta,F)$ be a program automaton. Let
$k\in\mathbb{N}$. We define $\mathcal{P}$ without $k$-infeasibility, as
$\mathcal{P}_{k}=(\mathit{Stmt},Q^{\prime},q_{0},\delta^{\prime},F^{\prime})$
where

$\displaystyle Q^{\prime}:=$
$\displaystyle\\{(q_{1},s_{1},q_{2}\dots,s_{k-1},q_{k})\mid(q_{1},s_{1},q_{2})\in\delta\wedge\dots\wedge(q_{k-1},s_{k-1},q_{k})\in\delta\\}~{}\cup$
$\displaystyle\\{(q_{0},s_{0},q_{1}\dots,s_{k^{\prime}-1},q_{k^{\prime}})\mid
k^{\prime}<k-1\wedge(q_{0},s_{0},q_{1})\in\delta\wedge\dots$
$\displaystyle\phantom{(q_{0},s_{0},q_{1}\dots,s_{k^{\prime}-1},q_{k^{\prime}})\mid}\quad\wedge(q_{k^{\prime}-1},s_{k^{\prime}-1},q_{k^{\prime}})\in\delta\\}$
$\displaystyle\delta^{\prime}:=$
$\displaystyle\\{((q_{1},s_{1},q_{2}\dots,s_{k-1},q_{k}),s_{k},(q_{2},s_{2},\dots,q_{k},s_{k},q_{k+1}))\in
Q^{\prime}\times\mathit{Stmt}\times Q^{\prime}$ $\displaystyle\quad\mid
s_{1}\dots s_{k}\text{ feasible}\\}~{}\cup$
$\displaystyle\\{((q_{0},s_{0},q_{1}\dots,s_{k^{\prime}-1},q_{k^{\prime}}),s_{k^{\prime}},(q_{0},s_{0},\dots,q_{k^{\prime}},s_{k^{\prime}},q_{k^{\prime}+1}))\in
Q^{\prime}\times\mathit{Stmt}\times Q^{\prime}$ $\displaystyle\quad\mid
k^{\prime}<k-1\wedge s_{0}\dots s_{k^{\prime}}\text{ feasible}\\}$
$\displaystyle F^{\prime}:=$
$\displaystyle\\{(q_{1},s_{1},q_{2}\dots,s_{k-1},q_{k})\in Q^{\prime}\mid
q_{k}\in F\\}~{}\cup$
$\displaystyle\\{(q_{0},s_{0},q_{1}\dots,s_{k^{\prime}-1},q_{k^{\prime}})\in
Q^{\prime}\mid k^{\prime}<k-1\wedge q_{k^{\prime}}\in F\\}$

###### Theorem 5.3

$\mathcal{P}_{k}$ accepts exactly the $k$-feasible traces of $\mathcal{P}$.

The proof follows directly from the construction above, see App. 0.A.3 for
details.

####  5.2.2 Removing Infeasible Accepting Cycles

For removing infeasible accepting cycles, we first enumerate all simple cycles
of the automaton (using, e.g., [42]), adding also cycles induced by self-
loops. For each cycle $\varrho$ that contains at least one accepting state, we
test its feasibility: first, using an SMT-solver to test if $\varrho$ is
locally infeasible; then, using a ranking function synthesizer (e.g., [23, 8,
38]) to test if $\varrho^{\omega}$ is infeasible. If we successfully prove
infeasibility, we refine the model, using the methods from [39, 40]. This
refinement is formalized in the following.

###### Definition 14

Let $\mathcal{P}=(\mathit{Stmt},Q,q_{0},\delta,F)$ be a program automaton. Let
$\varrho=(q_{1},s_{1},q_{2})(q_{2},s_{2},q_{3})\dots(q_{n},s_{n},q_{1})$ be a
sequence of transitions of $\mathcal{P}$. We say that $\varrho$ is an
_infeasible accepting cycle_ if there is a $1\leq j\leq n$ with $q_{j}\in F$
and $(s_{1}s_{2}\dots s_{n-1})^{\omega}$ is infeasible for all possible
initial assignments $\zeta_{-1}$.

###### Definition 15

Let $\mathcal{P}$ be a program automaton and
$C\subseteq(Q\times\mathit{Stmt}\times Q)^{\omega}$ be a set of infeasible
accepting cycles of $\mathcal{P}$. Furthermore, let

$\varrho=(q_{1},s_{1},q_{2})(q_{2},s_{2},q_{3})\dots(q_{n-1},s_{n-1},q_{n})\in~{}C.$

The automaton $\mathcal{A}_{\varrho}$ for $\varrho$ is
$\mathcal{A}_{\varrho}=(\mathit{Stmt},Q=\\{q_{0},q_{1},\dots
q_{n}\\},q_{0},\delta,Q\backslash\\{q_{0}\\})$ where

$\displaystyle\delta~{}=~{}$ $\displaystyle\\{(q_{0},s,q_{0})\mid
s\in\mathit{Stmt}\\}$ $\displaystyle\cup\\{(q_{j},s_{j},q_{j+1})\mid 1\leq
j<n\\}\cup\\{(q_{0},s_{1},q_{2}),(q_{n},s_{n},q_{1})\\}.$

Then, $\mathcal{A}_{\varrho}$ accepts exactly the traces that end with
$\varrho^{\omega}$, without any restriction on the prefix. See Fig. 2 for an
example. To exclude the traces of $\mathcal{A}_{\varrho}$ from $\mathcal{P}$,
we define $\mathcal{P}_{C}:=\mathcal{P}\backslash\left(\bigcup_{\varrho\in
C}\mathcal{A}_{\varrho}\right)$.555For two automata
$\mathcal{A}_{1},\mathcal{A}_{2}$ we use
$\mathcal{A}_{1}\backslash\mathcal{A}_{2}$ to denote the intersection of
$\mathcal{A}_{1}$ with the complement of $\mathcal{A}_{2}$, resulting in the
language $\mathcal{L}(\mathcal{A}_{1})\setminus\mathcal{L}(\mathcal{A}_{2})$.
This construction can be repeated to exclude infeasible accepted cycles that
are newly created in $\mathcal{P}_{C}$. We denote the result of iterating this
process $k^{\prime}$ times by $\mathcal{P}_{C(k^{\prime})}$.

####  5.2.3 Finding Counterexamples for $\forall^{*}\exists^{*}$
HyperTSL(T)-Formulas

Consider now a HyperTSL(T) formula $\varphi=\forall^{1\cdots
m}\exists^{m+1\cdots n}.\psi$ and a program automaton $\mathcal{P}$.

$q_{0}$$q_{2}$$q_{1}$$*$$n--$$n--$$assert(n\geq 0)$ Figure 2: Automaton
$\mathcal{A}_{\varrho}$ for the infeasible cycle
$\varrho=(q_{1},~{}n--,~{}q_{2})(q_{2},~{}assert(n>0),~{}q_{1})$. Label $*$
denotes an edge for every (relevant) statement.

For finding a counterexample, we first construct the combined product
$\mathcal{P}^{n}\otimes\mathcal{A}_{\psi}$. Each feasible accepted trace of
$\mathcal{P}^{n}\otimes\mathcal{A}_{\psi}$ corresponds to a combination of $n$
feasible program traces that satisfy $\psi$. Next, we eliminate
$k$-infeasibility and remove $k^{\prime}$-times infeasible accepting cycles
from the combined product, resulting in the automaton
$(\mathcal{P}^{n}\otimes\mathcal{A}_{\psi})_{k,C(k^{\prime})}$. Using this
modified combined product, we obtain an over-approximation of the program
execution combinations satisfying the existential part of the specification.
Each trace of the combined product is a combination of $n$ program executions
and a predicate/update term sequence. We then project the $m$ universally
quantified program executions from a feasible trace, obtaining a tuple of $m$
program executions that satisfy the existential part of the formula. Applying
this projection to all traces of
$(\mathcal{P}^{n}\otimes\mathcal{A}_{\psi})_{k,C(k^{\prime})}$ leads to an
over-approximation of the program executions satisfying the existential part
of the specification. Formally:

###### Definition 16

Let $\mathcal{P}$ be a program automaton, let $m\leq n\in\mathbb{N}$, and let
$\mathcal{A}_{\psi}$ be the automaton for the formula $\psi$. Let
$(\mathcal{P}^{n}\otimes\mathcal{A})_{k,C(k^{\prime})}=(\mathit{Stmt},Q,q_{0},\delta,F)$.
We define the _projected automaton_
$(\mathcal{P}^{m}\otimes\mathcal{A})_{k,C(k^{\prime})}^{\forall}=(\mathit{Stmt},Q,q_{0},\delta^{\forall},F)$
where $\delta^{\forall}=\\{(q,(s_{1};\dots;~{}s_{m}),q^{\prime})\mid\exists
s_{m+1},\dots
s_{n},l.~{}(q,\mathit{combine}(s_{1};\dots;~{}s_{n},l),q^{\prime})\in\delta\\}$.

The notation $s_{1};s_{2}$ refers to a sequence of statements, as given in
Def. 4. For more details on the universal projection we refer the reader
to[34].

Now, it only remains to check whether the over-approximation contains all
tuples of $m$ feasible program executions. If not, a counterexample is found.
This boils down to testing if
$\mathcal{P}^{m}\backslash(\mathcal{P}^{n}\otimes\mathcal{A}_{\psi})_{k,C(k^{\prime})}^{\forall}$
has some feasible trace. Thm. 5.4 states the soundness of our algorithm. See
App. 0.A.6 for its proof.

###### Theorem 5.4

Let $\varphi=\forall^{1\cdots m}\exists^{m+1\cdots n}.\psi$ be a HyperTSL(T)
formula. If the automaton
$\mathcal{P}^{m}\backslash(\mathcal{P}^{n}\otimes\mathcal{A}_{\psi})_{k,C(k^{\prime})}^{\forall}$
has a feasible trace, then $\mathcal{P}$ does not satisfy $\varphi$.

##  6 Demonstration of the Algorithm

In this section, we apply the algorithm of Sec. 5.2 to two simple examples,
demonstrating that removing some infeasibilities can already be sufficient for
identifying counterexamples.

####  6.0.1 Generalized Noninterference

Recall the formula
$\varphi_{gni}=\forall\pi.~{}\exists\pi^{\prime}.~{}\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(i_{\pi^{\prime}}=\lambda\wedge
c_{\pi}=c_{\pi^{\prime}})$ introduced in Sec. 1, specifying generalized
noninterference. We model-check $\varphi_{gni}$ on the program automaton
$\mathcal{P}$ of Fig. 3 (left), setting $\lambda=0$. The program $\mathcal{P}$
violates $\varphi_{gni}$ since for the trace $(assert(i<0)~{}c:=0)^{\omega}$
there is no other trace where on which $c$ is equal, but $i=0$.

$q_{0}$$q_{1}$$q_{2}$$A(i<0)$$A(i\geq 0)$$c:=0$$c:=1$

$q_{0}q_{0}$$q_{1}q_{1}$$q_{1}q_{2}$$q_{2}q_{1}$$q_{2}q_{2}$$A(i_{\pi}<0\wedge
i_{\pi^{\prime}}<0)$$A(i_{\pi}\geq 0\wedge i_{\pi^{\prime}}\geq
0)$$A(i_{\pi}\geq 0\wedge i_{\pi^{\prime}}<0)$$A(i_{\pi}<0\wedge
i_{\pi^{\prime}}\geq
0)$$c_{\pi}:=0;c_{\pi^{\prime}}:=0$$c_{\pi}:=1;c_{\pi^{\prime}}:=1$$c_{\pi}:=1;c_{\pi^{\prime}}:=0$$c_{\pi}:=0;c_{\pi^{\prime}}:=1$

Figure 3: Left: The program automaton $\mathcal{P}$ used in the first example.
Right: The program automaton $\mathcal{P}^{2}$. For brevity, we use $A$ for
$assert$ and join consecutive assertions.

The automaton for $\psi=\operatorname{\leavevmode\hbox to6.97pt{\vbox
to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(i_{\pi^{\prime}}=0\wedge
c_{\pi}=c_{\pi^{\prime}})$ consists of a single accepting state with the self-
loop labeled with $\tau_{P}=(i_{\pi^{\prime}}=0\wedge
c_{\pi}=c_{\pi^{\prime}})$. For this example, it suffices to choose $k=1$. To
detect $1$-inconsistencies we construct $\mathcal{P}^{2}$ (Fig 3, right).
Then, $(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})_{k}$ is the combined product
with all $1$-inconsistent

$q_{0}q_{0}$$q_{1}q_{1}$$q_{1}q_{2}$$q_{2}q_{1}$$q_{2}q_{2}$$assert(i\geq
0)$$assert(i<0)$$c:=0$$c:=1$ Figure 4: program automaton
$(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})_{k}^{\forall}$

transitions removed (see Fig. 5 for the combined product).

$q_{0}q_{0}$$q_{1}q_{1}$$q_{1}q_{2}$$q_{2}q_{1}$$q_{2}q_{2}$$i:=*;A(i_{\pi}<0\wedge
i_{\pi^{\prime}}<0\wedge\tau_{P})$$i:=*;A(i_{\pi}\geq 0\wedge
i_{\pi^{\prime}}\geq 0\wedge\tau_{P})$$i:=*;A(i_{\pi}\geq 0\wedge
i_{\pi^{\prime}}<0\wedge\tau_{P})$$i:=*;A(i_{\pi}<0\wedge i_{\pi^{\prime}}\geq
0\wedge\tau_{P})$$i:=*;c_{\pi}:=0;c_{\pi^{\prime}}:=0;A(\tau_{P})$$i:=*;c_{\pi}:=1;c_{\pi^{\prime}}:=1;A(\tau_{P})$$i:=*;c_{\pi}:=1;c_{\pi^{\prime}}:=0;A(\tau_{P})$$i:=*;c_{\pi}:=0;c_{\pi^{\prime}}:=1;A(\tau_{P})$
Figure 5: The combined product $(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})$

The automaton $(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})_{k}^{\forall}$ is
shown in Fig. 4. It does not contain the trace
$\sigma=\mathit{assert}(i<0)~{}(c:=0)^{\omega}$ which is a feasible trace of
$\mathcal{P}$. Therefore, $\sigma$ is a feasible trace accepted by
$\mathcal{P}\backslash(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})_{k}^{\forall}$
and is a counterexample proving that $\mathcal{P}$ does not satisfy
generalized noninterference – there is no feasible trace that agrees on the
value of the cell $c$ but has always $i=0$.

####  6.0.2 The Need of Removing Cycles

We now present an example in which removing $k$-infeasibility is not
sufficient, but removing infeasible accepting cycles leads to a
counterexample. Consider the specification
$\varphi=\forall\pi\exists\pi^{\prime}.\operatorname{\leavevmode\hbox
to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}(p_{\pi}\neq
p_{\pi^{\prime}}\wedge n_{\pi}<n_{\pi^{\prime}})$ and the program automaton
$\mathcal{P}_{cy}$ of Fig. 6. The formula $\varphi$ states that for every
trace $\pi$, there is another trace $\pi^{\prime}$ which differs from $\pi$ on
$p$, but in which $n$ is always greater. The trace
$\pi=(n:=*);(p:=*);\mathit{assert}(p=0);(n--)^{\omega}$ is a counterexample
for $\varphi$ in $\mathcal{P}_{cy}$ as any trace $\pi^{\prime}$ which differs
on $p$ will decrease its $n$ by $2$ in every time step, and thus
$n_{\pi^{\prime}}$ will eventually drop below $n_{\pi}$.

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$q_{4}$$n:=*$$p:=*$$A(p=0)$$A(p\neq
0)$$n--$$n:=n-2$

$q_{0}q_{0}$$q_{1}q_{1}$$q_{2}q_{2}$$q_{3}q_{4}$$q_{4}q_{3}$$q_{3}q_{3}$$q_{4}q_{4}$$n_{\pi}:=*;n_{\pi^{\prime}}:=*$$p_{\pi}:=*;p_{\pi^{\prime}}:=*$$A(p_{\pi}=0\wedge
p_{\pi^{\prime}}=0)$$A(p_{\pi}\neq 0\wedge p_{\pi^{\prime}}\neq
0)$$A(p_{\pi}=0\wedge p_{\pi^{\prime}}\neq 0)$$A(p_{\pi}\neq 0\wedge
p_{\pi^{\prime}}=0)$$n_{\pi}--;n_{\pi^{\prime}}--$$n_{\pi}:=n_{\pi}-2;n_{\pi^{\prime}}:=n_{\pi^{\prime}}-2$Y1.0e0]pt$n_{\pi}:=n_{\pi}-2;$$n_{\pi^{\prime}}--$Y1.0e0]pt$n_{\pi}--;$$n_{\pi^{\prime}}:=n_{\pi^{\prime}}-2$

Figure 6: Left: The program automaton $\mathcal{P}_{cy}$, Right: The program
automaton $\mathcal{P}_{cy}^{2}$.

The automaton $\mathcal{P}_{cy}^{2}$ is shown in Fig. 6. In the combined
product, the structure of the automaton stays the same, and
$\mathit{assert}(p_{\pi}\neq p_{\pi^{\prime}}\wedge n_{\pi}<n_{\pi}^{\prime})$
is added to every state. Removing local $k$-infeasibilities is not sufficient
here; assume $k=1$. The only $1$-infeasible transition is the transition from
$q_{2}q_{2}$ to $q_{3}q_{3}$, and this does not eliminate the counterexample
$\pi$. Greater $k$’s do not work as well, as the remaining traces of the
combined product are not $k$ infeasible for any $k$.

However, the self-loop at $q_{3}q_{4}$ is an infeasible accepting cycle – the
sequence
$(n_{\pi}--;~{}n_{\pi^{\prime}}:=n_{\pi^{\prime}}-2;~{}\mathit{assert}(n_{\pi}<n_{\pi^{\prime}}))^{\omega}$
must eventually terminate. We choose $k^{\prime}=1$ removing all traces ending
with this cycle. Next, we project the automaton to the universal part. The
trace $\pi$ is not accepted by the automaton
$(\mathcal{P}^{2}\otimes\mathcal{A}_{\psi})^{\forall}_{1,C(1)}$. But since
$\pi$ is in $\mathcal{P}$ and feasible, it is identified as a counterexample.

##  7 Conclusions

We have extended HyperTSL with theories, resulting in HyperTSL(T), and
provided the first infinite-state model checking algorithms for both TSL(T)
and HyperTSL(T). As this is the first work to study (Hyper)TSL model checking,
these are also the first algorithms for _finite-state_ model checking for
(Hyper)TSL. For TSL(T), we have adapted known software model checking
algorithm for LTL to the setting of TSL(T). We then used the technique of
self-composition to generalize this algorithm to the alternation-free fragment
of HyperTSL(T).

We have furthermore described a sound but necessarily incomplete algorithm for
finding counterexamples for $\forall^{*}\exists^{*}$-HyperTSL(T) formulas (and
witnesses proving $\exists^{*}\forall^{*}$ formulas). Our algorithm makes it
possible to find program executions violating properties like generalized
noninterference, which is only expressible by using a combination of universal
and existential quantifiers.

Finding model checking algorithms for other fragments of HyperTSL(T), and
implementing our approach, remains as future work.

## References

  * [1] Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub.  A relational logic for higher-order programs.  Proc. ACM Program. Lang., 1(ICFP):21:1–21:29, 2017.
  * [2] B. Alpern and F.B. Schneider.  Defining liveness.  Information Processing Letters, pages 181–185, 1985.
  * [3] Shiraj Arora, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, and Danny Bøgsted Poulsen.  Statistical model checking for probabilistic hyperproperties of real-valued signals.  In Owolabi Legunsen and Grigore Rosu, editors, Model Checking Software - 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings, volume 13255 of Lecture Notes in Computer Science, pages 61–78. Springer, 2022.
  * [4] Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, and Jan Strejcek.  LTL to büchi automata translation: Fast and more deterministic.  In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7214 of Lecture Notes in Computer Science, pages 95–109. Springer, 2012.
  * [5] Gilles Barthe, Juan Manuel Crespo, and César Kunz.  Beyond 2-safety: Asymmetric product programs for relational program verification.  In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6-8, 2013. Proceedings, volume 7734 of Lecture Notes in Computer Science, pages 29–43. Springer, 2013.
  * [6] Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk.  Secure information flow by self-composition.  Math. Struct. Comput. Sci., 21(6):1207–1252, 2011.
  * [7] Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and César Sánchez.  A temporal logic for asynchronous hyperproperties.  In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pages 694–717. Springer, 2021.
  * [8] Amir M. Ben-Amram and Samir Genaim.  On the linear ranking problem for integer linear-constraint loops.  In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, pages 51–62. ACM, 2013.
  * [9] Nick Benton.  Simple relational correctness proofs for static analyses and program transformations.  In Neil D. Jones and Xavier Leroy, editors, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pages 14–25. ACM, 2004.
  * [10] Raven Beutner and Bernd Finkbeiner.  Software verification of hyperproperties beyond k-safety.  In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 341–362. Springer, 2022.
  * [11] Borzoo Bonakdarpour, César Sánchez, and Gerardo Schneider.  Monitoring hyperproperties by combining static analysis and runtime verification.  In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II, volume 11245 of Lecture Notes in Computer Science, pages 8–27. Springer, 2018.
  * [12] Laura Bozzelli, Adriano Peron, and César Sánchez.  Expressiveness and decidability of temporal logics for asynchronous hyperproperties.  In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 27:1–27:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
  * [13] Aaron R. Bradley.  Sat-based model checking without unrolling.  In Ranjit Jhala and David A. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, volume 6538 of Lecture Notes in Computer Science, pages 70–87. Springer, 2011.
  * [14] Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, and Aliaksei Tsitovich.  The opensmt solver.  In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010\. Proceedings, volume 6015 of Lecture Notes in Computer Science, pages 150–153. Springer, 2010.
  * [15] Jürgen Christ, Jochen Hoenicke, and Alexander Nutz.  Smtinterpol: An interpolating SMT solver.  In Alastair F. Donaldson and David Parker, editors, Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, volume 7385 of Lecture Notes in Computer Science, pages 248–254. Springer, 2012.
  * [16] Alessandro Cimatti and Alberto Griggio.  Software model checking via IC3.  In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 277–293. Springer, 2012.
  * [17] Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani.  The mathsat5 SMT solver.  In Nir Piterman and Scott A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013\. Proceedings, volume 7795 of Lecture Notes in Computer Science, pages 93–107. Springer, 2013.
  * [18] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.  Counterexample-guided abstraction refinement.  In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer, 2000.
  * [19] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez.  Temporal logics for hyperproperties.  In Martín Abadi and Steve Kremer, editors, Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8414 of Lecture Notes in Computer Science, pages 265–284. Springer, 2014.
  * [20] Michael R. Clarkson and Fred B. Schneider.  Hyperproperties.  J. Comput. Secur., 18(6):1157–1210, 2010.
  * [21] Norine Coenen, Bernd Finkbeiner, Jana Hofmann, and Julia Tillman.  Smart contract synthesis modulo hyperproperties.  To appear at the 36th IEEE Computer Security Foundations Symposium (CSF 2023), 2023.
  * [22] Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup.  Verifying hyperliveness.  In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 121–139. Springer, 2019.
  * [23] Michael Colón and Henny Sipma.  Practical methods for proving program termination.  In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 442–454. Springer, 2002.
  * [24] Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, and Sergio Mover.  Infinite-state liveness-to-safety via implicit abstraction and well-founded relations.  In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 271–291. Springer, 2016.
  * [25] Leonardo Mendonça de Moura and Nikolaj S. Bjørner.  Z3: an efficient SMT solver.  In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer, 2008.
  * [26] Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, and Andreas Podelski.  Fairness modulo theory: A new approach to LTL software model checking.  In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 49–66. Springer, 2015.
  * [27] Rayna Dimitrova, Bernd Finkbeiner, and Hazem Torfah.  Probabilistic hyperproperties of markov decision processes.  In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 484–500. Springer, 2020.
  * [28] Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, and Borzoo Bonakdarpour.  Hyperprob: A model checker for probabilistic hyperproperties.  In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 657–666. Springer, 2021.
  * [29] Marco Eilers, Peter Müller, and Samuel Hitz.  Modular product programs.  ACM Trans. Program. Lang. Syst., 42(1):3:1–3:37, 2020.
  * [30] Bernd Finkbeiner.  Model checking algorithms for hyperproperties (invited paper).  In Fritz Henglein, Sharon Shoham, and Yakir Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 3–16. Springer, 2021.
  * [31] Bernd Finkbeiner, Philippe Heim, and Noemi Passing.  Temporal stream logic modulo theories.  In Patricia Bouyer and Lutz Schröder, editors, Foundations of Software Science and Computation Structures - 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13242 of Lecture Notes in Computer Science, pages 325–346. Springer, 2022.
  * [32] Bernd Finkbeiner, Jana Hofmann, Florian Kohn, and Noemi Passing.  Reactive synthesis of smart contract control flows.  CoRR, abs/2205.06039, 2022.
  * [33] Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito.  Temporal stream logic: Synthesis beyond the bools.  In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 11561 of Lecture Notes in Computer Science, pages 609–629. Springer, 2019.
  * [34] Bernd Finkbeiner and Noemi Passing.  Synthesizing dominant strategies for liveness.  In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 37:1–37:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
  * [35] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez.  Algorithms for model checking HyperLTL and HyperCTL*.  In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 30–48. Springer, 2015.
  * [36] Hadar Frenkel, Orna Grumberg, and Sarai Sheinvald.  An automata-theoretic approach to model-checking systems and specifications over infinite data domains.  J. Autom. Reason., 63(4):1077–1101, 2019.
  * [37] Gideon Geier, Philippe Heim, Felix Klein, and Bernd Finkbeiner.  Syntroids: Synthesizing a game for fpgas using temporal logic specifications.  In Clark W. Barrett and Jin Yang, editors, 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019, pages 138–146. IEEE, 2019.
  * [38] Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski.  Linear ranking for linear lasso programs.  In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 365–380. Springer, 2013.
  * [39] Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski.  Software model checking for people who love automata.  In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 36–52. Springer, 2013.
  * [40] Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski.  Termination analysis by learning terminating programs.  In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 797–813. Springer, 2014.
  * [41] Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones.  On verifying timed hyperproperties.  In Johann Gamper, Sophie Pinchinat, and Guido Sciavicco, editors, 26th International Symposium on Temporal Representation and Reasoning, TIME 2019, October 16-19, 2019, Málaga, Spain, volume 147 of LIPIcs, pages 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
  * [42] Donald B. Johnson.  Finding all the elementary circuits of a directed graph.  SIAM J. Comput., 4(1):77–84, 1975.
  * [43] Leslie Lamport and Fred B. Schneider.  Verifying hyperproperties with TLA.  In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pages 1–16. IEEE, 2021.
  * [44] Benedikt Maderbacher and Roderick Bloem.  Reactive synthesis modulo theories using abstraction refinement.  CoRR, abs/2108.00090, 2021.
  * [45] Daryl McCullough.  Noninterference and the composability of security properties.  In Proceedings of the 1988 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 18-21, 1988, pages 177–186. IEEE Computer Society, 1988.
  * [46] Shohei Mochizuki, Masaya Shimakawa, Shigeki Hagihara, and Naoki Yonezaki.  Fast translation from LTL to büchi automata via non-transition-based automata.  In Stephan Merz and Jun Pang, editors, Formal Methods and Software Engineering - 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings, volume 8829 of Lecture Notes in Computer Science, pages 364–379. Springer, 2014.
  * [47] Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson.  Hyperproperties of real-valued signals.  In Jean-Pierre Talpin, Patricia Derler, and Klaus Schneider, editors, Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017, pages 104–113. ACM, 2017.
  * [48] Amir Pnueli.  The temporal logic of programs.  In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57. IEEE Computer Society, 1977.
  * [49] Yih-Kuen Tsay and Moshe Y. Vardi.  From linear temporal logics to büchi automata: The early and simple principle.  In Ernst-Rüdiger Olderog, Bernhard Steffen, and Wang Yi, editors, Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday, volume 13030 of Lecture Notes in Computer Science, pages 8–40. Springer, 2021.
  * [50] Hiroshi Unno, Tachio Terauchi, and Eric Koskinen.  Constraint-based relational verification.  In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pages 742–766. Springer, 2021.

##  Appendix 0.A Detailed Correctness Proofs

###  0.A.1 Hyper Linear Temporal Logic (HyperLTL)

Let AP be a finite set of atomic propositions and let $\Pi$ be a finite set of
trace variables. Then, a HyperLTL formula is defined by the grammar

$\displaystyle\varphi::=a_{\pi}\mid\neg\varphi\mid\varphi\wedge\varphi\mid\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
where $a\in AP$ and $\pi\in\Pi$.

The satisfaction of a HyperLTL formula is defined with respect to a mapping
$m:\Pi\rightarrow(2^{AP})^{\omega}$ of trace variables to traces. For treating
the quantifiers, we need the notion of extending such a mapping for a new
trace variable. We define

$\displaystyle m[\pi\rightarrow s](\pi)$ $\displaystyle=s$ $\displaystyle
m[\pi\rightarrow s](\pi^{\prime})$ $\displaystyle=m(\pi^{\prime})$
$\displaystyle\text{for }\pi\neq\pi^{\prime}$

The satisfaction of a HyperLTL formula with respect to a set of traces
$Z\subseteq{2^{AP}}^{\omega}$, a mapping of trace variables to traces
$m:\Pi\rightarrow{2^{AP}}^{\omega}$ and a time point $t$ is recursively
defined by

$\displaystyle Z,t,m\models_{LTL}a_{\pi}$ $\displaystyle\Leftrightarrow a\in
m(\pi)_{t}$ $\displaystyle Z,t,m\models_{LTL}\neg\varphi$
$\displaystyle\Leftrightarrow\neg(Z,t,m\models_{LTL}\varphi)$ $\displaystyle
Z,t,m\models_{LTL}\varphi\wedge\psi$ $\displaystyle\Leftrightarrow
Z,t,m\models_{LTL}\varphi\wedge Z,t,m\models\psi$ $\displaystyle
Z,t,m\models_{LTL}\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi$
$\displaystyle\Leftrightarrow Z,t+1,m\models_{LTL}\varphi$ $\displaystyle
Z,t,m\models_{LTL}\varphi\operatorname{\mathcal{U}}\psi$
$\displaystyle\Leftrightarrow\exists t^{\prime}\geq
t.~{}Z,t^{\prime},m\models_{LTL}\psi\wedge\forall t\leq
t^{\prime\prime}<t^{\prime}.~{}Z,t^{\prime\prime},m\models_{LTL}\varphi$
$\displaystyle Z,t,m\models_{LTL}\forall\pi.~{}\varphi$
$\displaystyle\Leftrightarrow\forall s\in Z.~{}m[\pi\rightarrow
s]\models_{LTL}\varphi$ $\displaystyle
Z,t,m\models_{LTL}\exists\pi.~{}\varphi$ $\displaystyle\Leftrightarrow\exists
s\in Z.~{}m[\pi\rightarrow s]\models_{LTL}\varphi$

We define $Z\models_{LTL}\varphi$ as $Z,0,\emptyset\models_{LTL}\varphi$.

For the sepcial case in which there is only one trace quantifier, and this is
a universal quantifier, we are in the fragment of LTL.

###  0.A.2 Similiarity of LTL and TSL

The following lemma states an important relation between (Hyper)TSL and LTL.
The LTL semantics is defined with respect to a sequence of subsets of atomic
propositions, while the semantics of a TSL-formula or quantifier-free HyperTSL
formula is defined with respect to a (hyper-)computation. A crucial
observation for this thesis is that we can ‘translate’ between the two – a
(hyper-)computation defines a sequence of predicate and update term subsets.
For each time point, the subset contains exactly the predicate and update
terms that are true now.

###### Definition 17

Let
$\hat{\zeta}\in\hat{\mathsf{A}}^{\omega},\rho\subseteq\hat{\mathcal{T}_{P}},\upsilon\subseteq\hat{\mathcal{T}_{U}}$.
We define

$\displaystyle Seq(\hat{\zeta},\rho,\upsilon)_{t}$
$\displaystyle=\\{\hat{\tau_{P}}\in\rho\mid
t,\emptyset,\hat{\zeta}\models\hat{\tau_{P}}\\}\cup\\{\llbracket
c\leftarrowtail\hat{\tau_{F}}\rrbracket\in\upsilon\mid
t,\emptyset,\hat{\zeta}\models\llbracket c\leftarrowtail\tau_{F}\rrbracket\\}$
$\displaystyle Seq(\hat{\zeta},\rho,\upsilon)$
$\displaystyle=Seq(\hat{\zeta},\rho,\upsilon)_{0}~{}Seq(\hat{\zeta},\rho,\upsilon)_{1}~{}Seq(\hat{\zeta},\rho,\upsilon)_{2}\dots$

If $\rho$ and $\upsilon$ are clear from the context, we also omit these
arguments.

###### Lemma 1

Let $t\in\mathbb{N}$. Let $\varphi$ be a HyperTSL-formula without quantifiers.
Let
$\rho\subseteq\hat{\mathcal{T}_{P}},\upsilon\subseteq\hat{\mathcal{T}_{U}}$ be
the sets of predicate and update terms appearing in $\varphi$, respectively.
Then

$\displaystyle t,Seq(\hat{\zeta})\models_{LTL}\varphi\Leftrightarrow
t,\emptyset,\hat{\zeta}\models\varphi$

###### Proof

(Lemma 1) Proof by structural induction over $\varphi$.

  * •

Case $\varphi=\hat{\tau_{P}}$

$\displaystyle
t,Seq(\hat{\zeta})\models_{LTL}\hat{\tau_{P}}\Leftrightarrow\hat{\tau_{P}}\in
Seq(\hat{\zeta})_{t}\Leftrightarrow
t,\emptyset,\hat{\zeta}\models\hat{\tau_{P}}$

  * •

Case $\varphi=\llbracket c_{\pi}\leftarrowtail\hat{\tau_{F}}\rrbracket$

$\displaystyle t,Seq(\hat{\zeta})\models_{LTL}\llbracket
c_{\pi}\leftarrowtail\hat{\tau_{F}}\rrbracket\Leftrightarrow\hat{\tau_{P}}\in
Seq(\hat{\zeta})_{t}\Leftrightarrow t,\emptyset,\hat{\zeta}\models\llbracket
c_{\pi}\leftarrowtail\hat{\tau_{F}}\rrbracket$

  * •

Case $\varphi=\neg\psi$

$\displaystyle
t,Seq(\hat{\zeta})\models_{LTL}\neg\psi\Leftrightarrow\neg(t,Seq(\hat{\zeta})\models_{LTL}\psi)\Leftrightarrow\neg(t,\emptyset,\hat{\zeta}\models\psi)\Leftrightarrow
t,\emptyset,\hat{\zeta}\models\neg\psi$

  * •

Case $\varphi=\psi\wedge\psi^{\prime}$

$\displaystyle t,Seq(\hat{\zeta})\models_{LTL}\psi\wedge\psi^{\prime}$
$\displaystyle\Leftrightarrow$ $\displaystyle
t,Seq(\hat{\zeta})\models_{LTL}\psi\wedge
t,Seq(\hat{\zeta})\models_{LTL}\psi^{\prime}$ $\displaystyle\Leftrightarrow$
$\displaystyle t,\emptyset,\hat{\zeta}\models\psi\wedge
t,\emptyset,\hat{\zeta}\models\psi^{\prime}$ $\displaystyle\Leftrightarrow$
$\displaystyle t,\emptyset,\hat{\zeta}\models\psi\wedge\psi^{\prime}$

  * •

Case $\varphi=\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi$

$\displaystyle t,Seq(\hat{\zeta})\models_{LTL}\operatorname{\leavevmode\hbox
to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip
3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi\Leftrightarrow
t+1,Seq(\hat{\zeta})\models_{LTL}\psi\Leftrightarrow
t+1,\emptyset,\hat{\zeta}\models\psi\Leftrightarrow
t,\emptyset,\hat{\zeta}\models\operatorname{\leavevmode\hbox to7.41pt{\vbox
to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\psi$

  * •

Case $\varphi=\psi\operatorname{\mathcal{U}}\psi^{\prime}$

$\displaystyle
t,Seq(\hat{\zeta})\models_{LTL}\psi\operatorname{\mathcal{U}}\psi^{\prime}$
$\displaystyle\Leftrightarrow$ $\displaystyle\exists t^{\prime}\geq
t.~{}t^{\prime},Seq(\hat{\zeta})\models_{LTL}\psi^{\prime}\wedge\forall t\leq
t^{\prime\prime}<t^{\prime}.~{}t^{\prime\prime},Seq(\hat{\zeta})\models_{LTL}\psi$
$\displaystyle\Leftrightarrow$ $\displaystyle\exists t^{\prime}\geq
t.~{}t^{\prime},Z,\hat{\zeta}\models\psi^{\prime}\wedge\forall t\leq
t^{\prime\prime}<t^{\prime}.~{}t^{\prime\prime},Z,\hat{\zeta}\models\psi$
$\displaystyle\Leftrightarrow$ $\displaystyle
t,\emptyset,\hat{\zeta}\models\psi\operatorname{\mathcal{U}}\psi^{\prime}$

###  0.A.3 Proof of Theorem 5.3

###### Proof

$\Rightarrow$ Let $q_{0},q_{1},q_{2}\dots\in Q^{\omega}$ be a run of $P$ on
the $k$-feasible trace $\sigma$. Then, for every $j\in\mathbb{N}$,

$e_{j}=((q_{j},\sigma_{j},q_{j+1}\dots,\sigma_{j+k-2},q_{j+k-1}),\sigma_{j+k-1},(q_{j+1},\sigma_{j+1},\dots,q_{j+k-1},\sigma_{j+k-1},q_{j+k}))$

is a transition of $P_{k}$. Moreover, for every $k^{\prime}<k$,

$e_{k^{\prime}}=((q_{0},s_{0},q_{1}\dots,\sigma_{k^{\prime}-1},q_{k^{\prime}}),\sigma_{k^{\prime}},(q_{0},\sigma_{0},\dots,q_{k^{\prime}},\sigma_{k^{\prime}},q_{k^{\prime}+1}))$

is also a transition of $P_{k}$. Thus, $q_{0},q_{1},\dots$ is accepted by
$P_{k}$.

$\Leftarrow$ Let $\sigma$ be a trace of $P$ accepted by $P_{k}$. Then, there
exist states of $P$ $q_{0},q_{1}\dots$ such that for every $j\in\mathbb{N}$,
$e_{j}$ from above is a transition of $P_{k}$. Thus, by the definition of
$P_{k}$ for every $j$, $\sigma_{j}\dots\sigma_{j+k-1}$ is feasible. Thus,
$\sigma$ is $k$-feasible.  $\square$

###  0.A.4 Proof of Theorem 4.1

The main idea of the correctness proof is a construction that, given a
computation $\zeta$ that matches a program trace $\sigma$, constructs a
computation matching the combined trace $\mathit{combine}(\sigma,Seq(\zeta))$
and vice versa ($Seq$ was defined in Definition 17). This gives us the
necessary feasibility proofs. To do so, we define two operations,
$\widetilde{(-)}$ and $(-)_{|\sigma}$ that ‘nearly’ invert each other: we have
that $(\widetilde{\zeta})_{|\sigma}=\zeta$ and if
$\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$ for some $X$, we also have
that $\widetilde{\zeta_{|\sigma}}=\zeta$. In Lemma 2 we show that if
$\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$ for some $X$, then
$\zeta_{|\sigma}\smalltriangleleft\sigma$. In Lemma 3 we show that then, we
also have that $X=Seq(\zeta_{|\sigma})$. Lemma 4 states the other direction:
if $\zeta\smalltriangleleft\sigma$, then also
$\widetilde{\zeta}\smalltriangleleft\mathit{combine}(\sigma,Seq(\zeta))$.
Those three lemmata give us the feasibility proofs needed for the algorithm’s
correctness. Lemma 1 then gives the equivalence between the violation of the
TSL-formula by $\zeta$ and the sequence $Seq(\zeta)$ being accepted by
$A_{\neg\varphi}$, needed for reasoning about the existence of a trace
$\mathit{combine}(\sigma,Seq(\zeta))$ in the Büchi program product.

We start with definining the operation $\widetilde{(-)}$. Let
$\sigma\in\mathit{Stmt}^{\omega}$ and $\zeta\smalltriangleleft\sigma$. We need
to extend this computation to one that matches
$\mathit{combine}(\sigma,Seq(\zeta))$. For every time point $t$, we need to
introduce computation steps that match
$\mathit{combine}(\sigma_{t},Seq(\zeta)_{t})=$
$\mathit{save\\_values}_{{Seq(\zeta)_{t}}};~{}\sigma_{t};~{}\mathit{new\\_inputs};~{}\mathit{check\\_preds}_{{Seq(\zeta)_{t}}};~{}\mathit{check\\_updates}_{{Seq(\zeta)_{t}}}$.
While executing $\mathit{save\\_values}_{{Seq(\zeta)_{t}}}$, the values of the
temporary variables are changed as required by the statements
$tmp_{j}:=\tau_{Fj}$. When the actual statement $\sigma_{t}$ is executed, the
computation changes to $\zeta_{t}$, but still with the ‘old’ input values and
extended with values for the temporal variables. Next, when executing
$\mathit{new\\_inputs}$, we stepwise change the input values to those in
$\zeta_{t}$. Then, the assertions are executed and the computation cannot
change anymore.

In the following, we also need the notion of extending an assignment: we
define $a[c\mapsto v](c)=v$ and $a[c\mapsto v](c^{\prime})=a(c^{\prime})$ for
$c\neq c^{\prime}$.

Let $\upsilon\subseteq\mathcal{T}_{U}$ be in the following the set of update
terms, and $\rho\subseteq\mathcal{T}_{P}$ the set of predicate terms appearing
in the formula $\varphi$.

###### Definition 18

Let $\mathbb{I}=\\{i_{1},\dots i_{n}\\}$ be the set of inputs and
$\upsilon=\\{\llbracket
c_{1}\leftarrowtail\tau_{F1}\rrbracket,\dots,\llbracket
c_{m}\leftarrowtail\tau_{Fm}\rrbracket\\}$. Given a computation $\zeta$, we
define the adapted computation $\widetilde{\zeta}$ as follows.

$\displaystyle a^{\mathit{tmp}_{1}}_{t}$
$\displaystyle:=\zeta_{t-1}[\mathit{tmp}_{1}\mapsto\eta(\tau_{F1},\zeta_{t-1})]$
$\displaystyle a^{\mathit{tmp}_{j}}_{t}$
$\displaystyle:=a^{\mathit{tmp}_{j-1}}[\mathit{tmp}_{j}\mapsto\eta(\tau_{Fj},\zeta_{t-1})]$
$\displaystyle\text{for }1<j\leq m$ $\displaystyle a_{t}$
$\displaystyle:=\zeta_{t}[\mathit{tmp}_{1}\mapsto\eta(\tau_{F1},\zeta_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\tau_{Fm},\zeta_{t-1}),$
$\displaystyle~{}~{}~{}~{}~{}~{}~{}~{}i_{1}\mapsto\zeta_{t-1}(i_{1}),~{}\dots,~{}i_{n}\mapsto\zeta_{t-1}(i_{n})]$
$\displaystyle a^{i_{1}}_{t}$
$\displaystyle:=a_{t}[i_{1}\mapsto\zeta_{t}(i_{1})]$ $\displaystyle
a^{i_{j}}_{t}$ $\displaystyle:=a^{i_{j-1}}[i_{j}\mapsto\zeta_{t}(i_{j})]$
$\displaystyle\text{for }1<j\leq n$ $\displaystyle\widetilde{\zeta_{t}}$
$\displaystyle:=a^{\mathit{tmp}_{1}}_{t}\dots
a^{\mathit{tmp}_{m}}_{t}~{}a_{t}~{}a^{i_{1}}_{t}~{}\dots~{}a^{i_{n}}_{t}~{}a^{i_{n}}_{t}~{}a^{i_{n}}_{t}$
$\displaystyle\widetilde{\zeta}$
$\displaystyle:=\widetilde{\zeta_{0}}~{}\widetilde{\zeta_{1}}\dots$

Note that this is the only possibility to adapt a computation
$\zeta\smalltriangleleft\sigma$ such that the result could match
$\mathit{combine}(\sigma,X)$ for any $X$.

Also note that
$a_{t}^{i_{n}}=\zeta_{t}[tmp_{1}\mapsto\eta(\tau_{F1},\zeta_{t-1}),\dots,tmp_{m}\mapsto\eta(\tau_{Fm},\zeta_{t-1})]$.

We can also define the left inverse of this operation: reducing a computation
that matches $\mathit{combine}(\sigma,X)$ to a computation that matches
$\sigma$.

###### Definition 19

Let
$\sigma\in\mathit{Stmt}^{\omega},X\in\mathcal{P}(\mathcal{T}_{P}\cup\mathcal{T}_{U})^{\omega}$
and $\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$. We define the reduced
computation $\zeta_{|\sigma}$ as follows.

$\displaystyle\iota(j)$
$\displaystyle:=(|\mathbb{I}|+|\upsilon|+3)\cdot(j+1)-3$
$\displaystyle\zeta_{|\sigma}(U)$
$\displaystyle:=(\zeta_{\iota(0)})_{|(\mathbb{I}\cup\mathbb{C})}~{}(\zeta_{\iota(1)})_{|(\mathbb{I}\cup\mathbb{C})}\dots$

where $a_{|(\mathbb{I}\cup\mathbb{C})}$ means restricting the domain of the
assignment to the original inputs and cells, thus excluding the temporal
variables $tmp_{1},tmp_{2}\dots$

Note that if $\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$, we also have
that $\zeta=\widetilde{\zeta_{|\sigma}}$, as this is the only computation that
could potentially match $\mathit{combine}(\sigma,X)$ and equals
$\zeta_{|\sigma}$ when restricted to $\sigma$.

###### Lemma 2

If $\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$, then
$\zeta_{|\sigma}\smalltriangleleft\sigma$.

###### Proof

We have to show that $\forall
t\in\mathbb{N}.~{}\zeta_{|\sigma}\smalltriangleleft_{t}\sigma$

Recall that $\zeta=\widetilde{\zeta_{|\sigma}}$ and

$\displaystyle\widetilde{(\zeta_{|\sigma})_{t}}=a^{tmp_{1}}_{t}\dots
a^{tmp_{m}}_{t}~{}a_{t}~{}a^{i_{1}}_{t}~{}\dots~{}a^{i_{n}}_{t}~{}a^{i_{n}}_{t}~{}a^{i_{n}}_{t}$

  * •

Case $\sigma_{t}=\mathit{assert}(\tau_{P})$
We know that
$\zeta\smalltriangleleft_{\iota(t)-|\mathbb{I}|}\mathit{combine}(\sigma,X)$.
The corresponding statement is $\sigma_{j}$, thus

$\displaystyle\eta(\tau_{P},\zeta_{\iota(t)-|\mathbb{I}|-1})=true~{}~{}~{}\wedge\forall
c\in\mathbb{C}^{*}.~{}\zeta_{\iota(t)-|\mathbb{I}|}(c)=\zeta_{\iota(t)-|\mathbb{I}|-1}(c)$

Moreover, $(\zeta_{\iota(t)-|\mathbb{I}|-1})=a_{t}^{tmp_{m}}$. This equals
$(\zeta_{|\sigma})_{t-1}$ extended with values for the temporary variables. As
$\tau_{P}$ does not contain the temporal variables, this means that
$\eta(\tau_{P},((\zeta_{|\sigma})_{t-1})_{|(\mathbb{I}\cup\mathbb{C})})$ is
also true. It remains to show that

$\displaystyle\forall
c\in\mathbb{C}.~{}(\zeta_{\iota(t-1)})_{|(\mathbb{I}\cup\mathbb{C})}(c)=(\zeta_{\iota(t)})_{|(\mathbb{I}\cup\mathbb{C})}(c)$

This is true as the only cells changed in
$\zeta_{\iota(t-1)}\dots\zeta_{\iota(t)-|\mathbb{I}|-1}$ and in
$\zeta_{\iota(t)-|\mathbb{I}|},\dots\zeta_{\iota(t)}$ are cells from
$\mathbb{C}^{*}\backslash\mathbb{C}$.

  * •

The two remaining cases are analogous.

###### Lemma 3

If $\zeta\smalltriangleleft combine(\sigma,X)$, then $X=Seq(\zeta_{|\sigma})$.

###### Proof

We prove $\forall t.~{}X_{t}=Seq(\zeta_{|\sigma})_{t}$. We know that
$\zeta\smalltriangleleft_{\iota(t)+1}\mathit{combine}(\sigma,X)$. The
corresponding statement is $\mathit{check\\_preds}_{X_{t}}$. Set
$h=\left(\bigwedge_{\tau_{P}\in{X_{t}}}\tau_{P}\wedge\bigwedge_{\tau_{P}\in\rho\backslash{X_{t}}}\neg\tau_{P}\right)$.
This means that

$\displaystyle\eta(h,\zeta_{\iota(t)+1})=true~{}~{}~{}\wedge\forall
c\in\mathbb{C}^{*}.~{}\zeta_{\iota(t)+1}(c)=\zeta_{\iota(t)}(c)$

This implies that
$true=\eta((h,\zeta_{\iota(t)})_{|(\mathbb{I}\cup\mathbb{C})})=\eta(h,(\zeta_{|\sigma})_{t})$.
Therefore, for all $\tau_{P}\in\rho$

$\displaystyle\tau_{P}\in Seq(\zeta_{|\sigma})_{t}\Leftrightarrow
t,\zeta_{|\sigma}\models\tau_{P}\Leftrightarrow\eta(\tau_{P},\zeta_{\iota(t)})=true\Leftrightarrow\tau_{P}\in{X_{t}}$

For the update terms, we know that
$\zeta\smalltriangleleft_{\iota(t)+2}\mathit{combine}(\sigma,X)$. The
corresponding statement is $\mathit{check\\_updates}_{X_{t}}.$ Set
$h=\left(\bigwedge_{\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon}\begin{cases}c_{j}=tmp_{j}&\text{if
}\llbracket c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in X_{t}\\\ c_{j}\neq
tmp_{j}&\text{else}\end{cases}\right)$ As before, we know that
$\eta(h,(\zeta_{|\sigma})_{t})=true$. Moreover, we know that for each $j$,
$(\zeta_{|\sigma})_{t}(tmp_{j})=\eta(\tau_{Fj},(\zeta_{|\sigma})_{t-1})$ by
definition 18 Therefore, for every $\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon,$

$\displaystyle\llbracket c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in
Seq(\zeta_{|\sigma})_{t}$ $\displaystyle\Leftrightarrow
t,\zeta_{|\sigma}\models\llbracket c_{j}\leftarrowtail\tau_{Fj}\rrbracket$
$\displaystyle\Leftrightarrow\eta({\tau_{Fj}},\zeta_{\iota(t-1)})=\eta(c_{j},\zeta_{\iota(t)})$
$\displaystyle\Leftrightarrow\eta(c_{j}=tmp_{j},\zeta_{\iota(t)})=true$
$\displaystyle\Leftrightarrow\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in X_{t}$

###### Lemma 4

If $\zeta\smalltriangleleft\sigma$, then
$\widetilde{\zeta}\smalltriangleleft\mathit{combine}(\sigma,Seq(\zeta))$

###### Proof

We have to show that for all $t$,
$\widetilde{\zeta}\smalltriangleleft_{t}\mathit{combine}(\sigma,Seq(\zeta))$.
This is clear for all time steps except for those of kind
$\mathit{check\\_preds}$ or $\mathit{check\\_updates}$ by the definition of
$\widetilde{\zeta}$.

First consider $\mathit{check\\_preds}$. We need to show that $\forall t$,
$\widetilde{\zeta}\smalltriangleleft_{\iota(t)+1}\mathit{combine}(\sigma,Seq(\zeta))$.
This boils down to

$\displaystyle\eta\left(\left(\bigwedge_{\tau_{P}\in{Seq(\zeta)_{t}}}\tau_{P}\wedge\bigwedge_{\tau_{P}\in\rho\backslash{Seq(\zeta)_{t}}}\neg\tau_{P}\right),\widetilde{\zeta}_{\iota(t)}\right)=true$

As the temporary variables $\mathit{tmp}_{1},\mathit{tmp}_{2}\dots$ are not
used in any $\tau_{P}\in\rho$, this is by definition 18 equivalent to

$\displaystyle\forall\tau_{P}\in\rho.~{}\tau_{P}\in
Seq(\zeta)_{t}\Leftrightarrow\eta(\tau_{P},\zeta_{t})=true$

This is true by the definition of $Seq(\zeta)_{t}$.

Now consider $\mathit{check\\_updates}$. We need to show that $\forall t$,
$\widetilde{\zeta}\smalltriangleleft_{\iota(t)+2}\mathit{combine}(\sigma,Seq(\zeta))$.
This boils down to

$\displaystyle\eta\left(\left(\bigwedge_{\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon}\begin{cases}c_{j}=\mathit{tmp}_{j}&\text{if
}\llbracket c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in Seq(\zeta)_{t}\\\
c_{j}\neq\mathit{tmp}_{j}&\text{else}\end{cases}\right),\widetilde{\zeta}_{\iota(t)}\right)=true$

Which is equivalent to

$\displaystyle\forall\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon.~{}\eta(c_{j}=\mathit{tmp}_{j},\widetilde{\zeta}_{\iota(t)})=true\Leftrightarrow\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in Seq(\zeta)_{t}$

We know that
$\widetilde{\zeta}_{\iota(t)}(\mathit{tmp}_{j})=\eta(\tau_{Fj},\zeta_{t-1})$.
Thus this is equivalent to

$\displaystyle\forall\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon.~{}\eta(\tau_{Fj},\zeta_{t-1})=\zeta_{t}(c)\Leftrightarrow\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in Seq(\zeta)_{t}$

which is again true by the definition of $Seq(\zeta)_{t}$.

Now, we have all the lemmas needed to prove Theorem 4.1

###### Proof

(Theorem 4.1)
$\Rightarrow$ Assume that $P\otimes A_{\neg\varphi}$ has a feasible trace.
Then, this is a trace $\mathit{combine}(\sigma,X)$ for some
$\sigma\in\mathcal{L}(P)$ and $X\in\mathcal{L}(A_{\neg\varphi})$. Moreover,
$\zeta\smalltriangleleft\mathit{combine}(\sigma,X)$ for some
$\zeta\in\mathsf{A}^{\omega}$. By Lemma 3, we know that $X=Seq(\zeta)$ and by
Lemma 2 we know that $\zeta\smalltriangleleft\sigma$. By the correctness of
$A_{\varphi}$, we know that $Seq(\zeta)\models_{LTL}\neg\varphi$, which by
Lemma 1 means that $\zeta\models\neg\varphi$. Thus $\zeta$ is a counterexample
that proves that $P$ does not satisfy $\varphi$.

$\Leftarrow$ Assume that $P$ does not satisfy $\varphi$. Then, there is a
trace $\sigma\in\mathcal{L}(P)$ and a computation $\zeta$ such that
$\zeta\smalltriangleleft\sigma$ and $\zeta\models\neg\varphi$. This means by
Lemma 1 that $Seq(\zeta)\models_{LTL}\neg\varphi$, so $Seq(\zeta)$ is accepted
by $A_{\neg\varphi}$. Then, $\mathit{combine}(\sigma,Seq(\zeta))$ is a trace
of $P\otimes A_{\neg\varphi}$. By Lemma 4,
$\widetilde{\zeta}\smalltriangleleft\mathit{combine}(\sigma,Seq(\zeta))$, so
this is also a feasible trace.

###  0.A.5 Proof of Theorems 5.1 and 5.2

As the two theorems are dual, it suffices to give the proof for Theorem 5.1.

The proof is analogous to the proof of Theorem 4.1, but we have to deal with
multiple traces and thus even more indices now. We give it here for
completeness.

Given $n$ program traces $\sigma_{\pi_{1}},\dots\sigma_{\pi_{n}}$, we define
$\sigma_{j}=({(\sigma_{\pi_{1}})_{\pi_{1}}}_{j};{(\sigma_{\pi_{2}})_{\pi_{2}}}_{j};\dots(\sigma_{\pi_{n}})_{\pi_{n}}{}_{j})$
and $\sigma=\sigma_{1}\sigma_{2}\dots$. Let
$\zeta_{\pi_{1}}\smalltriangleleft\sigma_{\pi_{1}}\wedge\dots\wedge\zeta_{\pi_{n}}\smalltriangleleft\sigma_{\pi_{n}}$.
Let
$\hat{\zeta}=\emptyset[\pi_{1},\zeta_{\pi_{1}}]\dots[\pi_{n},\zeta_{\pi_{n}}]$.
Those computations are extendable to a computation that matches
$\mathit{combine}(\sigma,Seq(\hat{\zeta}))$ For every time point $t$, we need
to introduce the computation steps that match
$\mathit{combine}(\sigma_{t},X_{t})=\mathit{save\\_values};~{}\sigma_{t};~{}\mathit{new\\_inputs};~{}\mathit{check\\_preds}_{X_{t}};~{}\mathit{check\\_updates}_{X_{t}}$.
While executing $\mathit{save\\_values}$, the values of the relevant temporary
variables are changed as required by the statements
$tmp_{j}:=\hat{\tau_{Fj}}$. After the actual statements $\sigma_{t}$ are
executed, the computation changes to $\hat{\zeta}_{t}$, but still with the
‘old’ inputs and extended with values for the temporal variables. Next, when
executing $\mathit{new\\_inputs}$, we stepwise change the input values to
those in $\hat{\zeta}_{t}$. Then, the assertions are executed and the
computation cannot change anymore.

In the following, we also need the notion of extending a hyper-assignment: we
define $\hat{a}[c\mapsto v](c)=v$ and $\hat{a}[c\mapsto
v](c^{\prime})=\hat{a}(c^{\prime})$ for $c\neq c^{\prime}$.

Let $\upsilon\subseteq\hat{\mathcal{T}_{U}}$ be in the following the set of
update terms and $\rho\subseteq\hat{\mathcal{T}_{P}}$ the predicate terms
appearing in the formula $\varphi$.

###### Definition 20

Let $\mathbb{I}\times\Pi=\\{i_{1},\dots i_{k}\\}$ be the set of inputs and
$\upsilon=\\{\llbracket
c_{1}\leftarrowtail\hat{\tau_{F1}}\rrbracket,\dots,\llbracket
c_{m}\leftarrowtail\hat{\tau_{Fm}}\rrbracket\\}$. Given computations
$\zeta_{\pi_{1}}\dots\zeta_{\pi_{n}}$, let
$\hat{\zeta}=\emptyset[\pi_{1},\sigma_{\pi_{1}}]\dots[\pi_{n},\sigma_{\pi_{n}}]$.
We define the adapted computation
$\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})}$.

$\displaystyle\hat{a}^{\mathit{tmp}_{1}}_{t}$
$\displaystyle:=\hat{\zeta}_{t-1}[\mathit{tmp}_{1}\mapsto\eta(\tau_{F1},\hat{\zeta}_{t-1})]$
$\displaystyle\hat{a}^{\mathit{tmp}_{j}}_{t}$
$\displaystyle:=\hat{a}^{\mathit{tmp}_{j-1}}[\mathit{tmp}_{j}\mapsto\eta(\tau_{Fj},\hat{\zeta}_{t-1})]~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\text{for
}1<j\leq m$ $\displaystyle\hat{a}^{\pi_{j}}_{t}$
$\displaystyle=(\hat{\zeta}_{t-1}[\pi_{1},\zeta_{\pi_{1}}]\dots[\pi_{j},\zeta_{\pi_{j}}])_{t}[i_{1}\mapsto\zeta_{t-1}(i_{1}),~{}\dots~{},i_{k}\mapsto\zeta_{t-1}(i_{k}),$
$\displaystyle~{}~{}~{}~{}\mathit{tmp}_{1}\mapsto\eta(\tau_{F1},\hat{\zeta}_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\tau_{Fm},\hat{\zeta}_{t-1})]$
$\displaystyle\hat{a}^{i_{1}}_{t}$
$\displaystyle:=\hat{a}_{t}^{\pi_{n}}[i_{1}\mapsto\hat{\zeta}_{t}(i_{1})]$
$\displaystyle\hat{a}^{i_{j}}_{t}$
$\displaystyle:=\hat{a}^{i_{j-1}}[i_{j}\mapsto\hat{\zeta}_{t}(i_{j})]~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\text{for
}1<j\leq k$
$\displaystyle\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})^{t}}$
$\displaystyle:=\hat{a}^{\mathit{tmp}_{1}}_{t}\dots\hat{a}^{\mathit{tmp}_{n}}_{t}~{}\hat{a}^{\pi_{1}}_{t}\dots\hat{a}^{\pi_{n}}_{t}~{}\hat{a}^{i_{1}}_{t}~{}\dots~{}\hat{a}^{i_{k}}_{t}~{}\hat{a}^{i_{k}}_{t}~{}\hat{a}^{i_{k}}_{t}$
$\displaystyle\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})}$
$\displaystyle:=\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})^{0}}~{}\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})^{1}}\dots$

Note that this is the only possibility to extend the computations
$\zeta_{\pi_{1}}\smalltriangleleft\sigma_{\pi_{1}},\dots,\zeta_{\pi_{n}}\smalltriangleleft\sigma_{\pi_{n}}$
to a computation that potentially matches $\mathit{combine}(\sigma,X)$ for any
$X$.

We can also define the left inverse of this operation: reducing a computation
that matches $\mathit{combine}(\sigma,X)$ to computations that match
$\sigma_{\pi_{1}},\dots,\sigma_{\pi_{n}}$ as follows.

###### Definition 21

Let $1\leq j\leq
n,\sigma\in\mathit{Stmt}^{\omega},X\in\mathcal{P}(\hat{\mathcal{T}_{P}}\cup\hat{\mathcal{T}_{U}})^{\omega}$
and $\hat{\zeta}\smalltriangleleft\mathit{combine}(\sigma,X)$. We define the
index of the computation step of $(\sigma_{\pi_{j}})_{t}$ in
$\mathit{combine}(\sigma,X)$

$\displaystyle\iota(t)$
$\displaystyle:=(|\mathbb{I}\times\Pi|+|\upsilon|+n+2)\cdot(t+1)-3$

We define the reduced computation $\zeta_{|\pi_{j}}$.

$\displaystyle\zeta_{|\pi_{j}}$
$\displaystyle:=(\zeta_{\iota(0)})_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}~{}(\zeta_{\iota(1)})_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}\dots$

where $\hat{a}_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}$ means restricting the
domain of the assignment to the cells and inputs labeled with $\pi_{j}$, thus
excluding the temporal variables $tmp_{1},tmp_{2}\dots$ and the variables from
other traces. Moreover, the cells and inputs are again renamed from
$c_{\pi_{j}}$ to $c$ or $i_{\pi_{j}}$ to $i$.

Note that if $\hat{\zeta}\smalltriangleleft\mathit{combine}(\sigma,X)$, we
also have that $\hat{\zeta}$ is the adapted computation of
$(\hat{\zeta}_{|\pi_{1}},\dots,\hat{\zeta}_{|\pi_{n}})$ as this is the only
computation that could match $\mathit{combine}(\sigma,X)$ and equals
$\zeta_{|\pi_{j}}$ when restricted to $\pi_{j}$.

###### Lemma 5

If $\hat{\zeta}\smalltriangleleft\mathit{combine}(\sigma,X)$ and
$\sigma=((\sigma_{\pi_{1}})_{\pi_{1}},\dots,(\sigma_{\pi_{n}})_{\pi_{n}})$,
then $\hat{\zeta}_{|\pi_{j}}\smalltriangleleft\sigma_{\pi_{j}}$ for every
$1\leq j\leq n$.

###### Proof

We show that $\forall
t\in\mathbb{N}.~{}\hat{\zeta}_{|\pi_{j}}\smalltriangleleft_{t}\sigma_{\pi_{j}}$.

Recall that $\hat{\zeta}$ is the adapted computation of
$(\hat{\zeta}_{|\pi_{1}},\dots,\hat{\zeta}_{|\pi_{n}})$ .

  * •

Case $\sigma_{t}=\mathit{assert}(\tau_{P})$
We know that
$\hat{\zeta}\smalltriangleleft_{\iota(t)-|\mathbb{I}\times\Pi|-(n-j)}\mathit{combine}(\sigma,X)$,
and thus

$\displaystyle\eta(\hat{\tau_{P}},\hat{\zeta}_{\iota(t)-|\mathbb{I}\times\Pi|-(n-j)-1})=true~{}~{}\wedge$
$\displaystyle\forall
c\in\mathbb{C}^{*}.~{}\hat{\zeta}_{\iota(t)-|\mathbb{I}\times\Pi|-(n-j)}(c)=\hat{\zeta}_{\iota(t)-|\mathbb{I}\times\Pi|(n-j)-1}(c)$

Moreover, $(\hat{\zeta}_{\iota(t)-|\mathbb{I}\times\Pi|-(n-j)-1})$ equals
$\hat{a}^{tmp_{m}}_{t}$ if $j=0$ and else $\hat{a}^{\pi_{j-1}}_{t}$, which
both equals $(\hat{\zeta}_{|\pi_{j}})_{t-1}$ when restricted to the inputs and
variables from $\pi_{j}$. $\tau_{P}$ does not contain variables from other
traces or temporary variables, thus
$\eta(\tau_{P},(\hat{\zeta}_{|\pi_{j}})_{t-1})$ is also true. It remains to
show that

$\displaystyle\forall
c\in\mathbb{C}.~{}((\hat{\zeta})_{\iota(t-1)})_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}(c)=((\hat{\zeta})_{\iota(t)})_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}(c)$

This is also true as the only cells changed in
$\hat{\zeta}_{\iota(t-1)}\dots\hat{\zeta}_{\iota(t)-|\mathbb{I}\times\Pi|-(n-j)-1}$
and in
$\hat{\zeta}_{\iota(t)-(n-j)-|\mathbb{I}\times\Pi|},\dots\hat{\zeta}_{\iota(t)}$
are cells from $\mathbb{C}^{*}\backslash\mathbb{C}$ or cells from other
traces.

  * •

The two remaining cases are analogous.

###### Lemma 6

If $\hat{\zeta}\smalltriangleleft combine(\sigma,X)$, then
$X=Seq(\emptyset[\pi_{1},\hat{\zeta}_{|\pi_{1}}]\dots[\pi_{n},\hat{\zeta}_{|\pi_{n}}])$

###### Proof

Set
$\hat{\zeta}^{\prime}=\emptyset[\pi_{1},\hat{\zeta}_{|\pi_{1}}]\dots[\pi_{n},\hat{\zeta}_{|\pi_{n}}]$.
We prove $\forall t.~{}X_{t}=Seq(\hat{\zeta}^{\prime})_{t}$. We know that
$\hat{\zeta}\smalltriangleleft_{\iota(t)+1}\mathit{combine}(\sigma,X)$. The
corresponding statement is $check\\_preds_{X_{t}}$. Set
$h=\left(\bigwedge_{\tau_{P}\in{X_{t}}}\hat{\tau_{P}}\wedge\bigwedge_{\hat{\tau_{P}}\in\rho\backslash{X_{t}}}\neg\tau_{P}\right)$.
This means that

$\displaystyle\eta(h,\hat{\zeta}_{\iota(t)+1})=true~{}~{}~{}\wedge\forall
c\in\mathbb{C}^{*}.~{}\zeta_{\iota(t)+1}(c)=\hat{\zeta}_{\iota(t)}(c)$

Recall that $\hat{\zeta}_{\iota(t)+1}$ is by Definition 20 equal to

$\displaystyle(\hat{\zeta}^{\prime}_{t-1}[\pi_{1},\hat{\zeta}^{\prime}_{\pi_{1}}]\dots[\pi_{j},\hat{\zeta}^{\prime}_{\pi_{n}}])_{t}~{}[\mathit{tmp}_{1}\mapsto\eta(\hat{\tau_{F1}},\hat{\zeta}^{\prime}_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\hat{\tau_{Fm}},\hat{\zeta}^{\prime}_{t-1})]$
$\displaystyle=\hat{\zeta}^{\prime}_{t}~{}[\mathit{tmp}_{1}\mapsto\eta(\hat{\tau_{F1}},\hat{\zeta}^{\prime}_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\hat{\tau_{Fm}},\hat{\zeta}^{\prime}_{t-1})]$

$h$ does not contain the temporal variables, so this implies that
$\eta(h,\hat{\zeta}^{\prime}_{t})=true$. Therefore, for all $\tau_{P}\in P$

$\displaystyle\tau_{P}\in Seq(\hat{\zeta}^{\prime})_{t}\Leftrightarrow
t,\hat{\zeta}^{\prime}\models\tau_{P}\Leftrightarrow\eta(\tau_{P},\zeta^{\prime}_{t})=true\Leftrightarrow\tau_{P}\in{X_{t}}$

The last equivalence holds by the definition of $h$.

For the update terms, we know that
$\zeta\smalltriangleleft_{\iota(t)+2}\mathit{combine}(\sigma,X)$. The
corresponding statement is $\mathit{check\\_updates}_{X_{t}}$. Set
$h=\left(\bigwedge_{\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in\upsilon}\begin{cases}c_{j}=\mathit{tmp}_{j}&\text{if
}\llbracket c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in X_{t}\\\
c_{j}\neq\mathit{tmp}_{j}&\text{else}\end{cases}\right)$ As before, we know
that $\eta(h,\hat{\zeta}^{\prime}_{t})=true$. Moreover, we know that for each
$j$,
$\hat{\zeta}_{\iota(t)+1}(\mathit{tmp}_{j})=\eta(\hat{\tau_{Fj}},\hat{\zeta}^{\prime}_{t-1})$
again by Definition 20 Therefore, for every $\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in\upsilon,$

$\displaystyle\llbracket c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in
Seq(\hat{\zeta}^{\prime})_{t}$ $\displaystyle\Leftrightarrow
t,\hat{\zeta}^{\prime}\models\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket$
$\displaystyle\Leftrightarrow\eta({\hat{\tau_{Fj}}},\hat{\zeta}^{\prime}_{t-1})=\eta(c_{j},\hat{\zeta}^{\prime}_{t})$
$\displaystyle\Leftrightarrow\eta(c_{j}=tmp_{j},\hat{\zeta}^{\prime}_{t})=true$
$\displaystyle\Leftrightarrow\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in X_{t}$

The last equivalence is again true by the definition of $h$.

###### Lemma 7

If
$\zeta_{\pi_{1}}\smalltriangleleft\sigma_{\pi_{1}}\wedge\dots\wedge\zeta_{\pi_{n}}\smalltriangleleft\sigma_{\pi_{n}}$,
then
$\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})}\smalltriangleleft\mathit{combine}(\sigma,Seq(\hat{\zeta}^{\prime}))$,
where
$\hat{\zeta}^{\prime}=\emptyset[\pi_{1},\zeta_{\pi_{1}}]\dots[\pi_{n},\zeta_{\pi_{n}}]$

###### Proof

Set $\hat{\zeta}=\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})}$. We have
to show that for all $t$,
$\hat{\zeta}\smalltriangleleft_{t}\mathit{combine}(\sigma,Seq(\hat{\zeta}^{\prime}))$.
This is clear for all time steps except for those of kind
$\mathit{check\\_preds}$ or $\mathit{check\\_updates}$ by the definition of
$\hat{\zeta}$.

First consider $\mathit{check\\_preds}$. We need to show that $\forall t$,
$\hat{\zeta}\smalltriangleleft_{\iota(t)+1}\mathit{combine}(\sigma,Seq(\hat{\zeta}^{\prime}))$.
This boils down to

$\displaystyle\eta\left(\left(\bigwedge_{\hat{\tau_{P}}\in{Seq(\hat{\zeta}^{\prime})_{t}}}\hat{\tau_{P}}\wedge\bigwedge_{\hat{\tau_{P}}\in\rho\backslash{Seq(\hat{\zeta}^{\prime})_{t}}}\neg\hat{\tau_{P}}\right),\hat{\zeta}_{\iota(t)+1}\right)=true$

Recall that $\hat{\zeta}_{\iota(t)+1}$ is by Definition 20 equal to

$\displaystyle(\hat{\zeta}^{\prime}_{t-1}[\pi_{1},\hat{\zeta}^{\prime}_{\pi_{1}}]\dots[\pi_{j},\hat{\zeta}^{\prime}_{\pi_{n}}])_{t}~{}[\mathit{tmp}_{1}\mapsto\eta(\hat{\tau_{F1}},\hat{\zeta}^{\prime}_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\hat{\tau_{Fm}},\hat{\zeta}_{t-1})]$
$\displaystyle=\hat{\zeta}^{\prime}_{t}~{}[\mathit{tmp}_{1}\mapsto\eta(\hat{\tau_{F1}},\hat{\zeta}^{\prime}_{t-1}),\dots,\mathit{tmp}_{m}\mapsto\eta(\hat{\tau_{Fm}},\hat{\zeta}_{t-1})]$

Thus, as the temporary variables are not used in $\hat{\tau_{P}}$, this is
equivalent to

$\displaystyle\forall\hat{\tau_{P}}\in\rho.~{}\hat{\tau_{P}}\in
Seq(\zeta^{\prime})_{t}\Leftrightarrow\eta((\hat{\tau_{P}}),\zeta^{\prime}_{t})=true$

This is true by the definition of $Seq(\zeta)_{t}$.

Now consider $\mathit{check\\_updates}$. We need to show that $\forall t$,
$\hat{\zeta}\smalltriangleleft_{\iota(t)+2}\mathit{combine}(\sigma,Seq(\hat{\zeta}^{\prime}))$.
This boils down to

$\displaystyle\eta\left(\left(\bigwedge_{\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in\upsilon}\begin{cases}c_{j}=\mathit{tmp}_{j}&\text{if
}\llbracket c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in
Seq(\hat{\zeta}^{\prime})_{t}\\\
c_{j}\neq\mathit{tmp}_{j}&\text{else}\end{cases}\right),\hat{\zeta}_{\iota(t)+2}\right)=true$

Which is again equivalent to

$\displaystyle\forall\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in\upsilon.~{}\eta(c_{j}=\mathit{tmp}_{j},\hat{\zeta}_{\iota(t)+2})=true\Leftrightarrow\llbracket
c_{j}\leftarrowtail\tau_{Fj}\rrbracket\in Seq(\hat{\zeta}^{\prime})_{t}$

We know that
$\hat{\zeta}_{\iota(t)+2}(\mathit{tmp}_{j})=\hat{\zeta}^{\prime}_{t-1}(\tau_{Fj})$.
Thus this is equivalent to

$\displaystyle\forall\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in\upsilon.~{}\eta(\hat{\tau_{Fj}},\hat{\zeta}^{\prime}_{t-1})=\hat{\zeta}^{\prime}_{t}(c)\Leftrightarrow\llbracket
c_{j}\leftarrowtail\hat{\tau_{Fj}}\rrbracket\in Seq(\hat{\zeta}^{\prime})_{t}$

Which is again true by the definition of $Seq(\hat{\zeta}^{\prime})_{t}$.

Now, we have all the lemmas needed to prove Theorem 5.1

###### Proof

(Theorem 5.1)
$\Rightarrow$ Assume that $P^{n}\otimes A_{\neg\varphi}$ has a feasible trace.
Then, this is a trace $\mathit{combine}(\sigma,X)$ for some
$\sigma\in\mathcal{L}(P^{n})$ and $X\in\mathcal{L}(A_{\neg\varphi})$. We know
that
$\sigma_{t}=({(\sigma_{\pi_{1}})_{\pi_{1}}}_{t};\dots;{(\sigma_{\pi_{n}})_{\pi_{n}}}_{t})$.
Moreover, $\hat{\zeta}\smalltriangleleft\mathit{combine}(\sigma,X)$ for some
$\hat{\zeta}\in\hat{\mathsf{A}}^{\omega}$. By Lemma 5, we know that
$\hat{\zeta}_{|\pi_{1}}\smalltriangleleft\sigma_{\pi_{1}}\wedge\dots\wedge\hat{\zeta}_{|\pi_{n}}\smalltriangleleft\sigma_{\pi_{n}}$.
Set
$\hat{\zeta}^{\prime}=\emptyset[\pi_{1},\hat{\zeta}_{|\pi_{1}}]\dots[\pi_{n},\hat{\zeta}_{|\pi_{n}}]$.
By Lemma 6, we know that $X=Seq(\hat{\zeta}^{\prime})$. By the correctness of
$A_{\psi}$ this means that $Seq(\hat{\zeta}^{\prime})\models_{LTL}\neg\varphi$
which by Lemma 1 means that $\hat{\zeta}^{\prime}\models\neg\varphi$. Thus,
$\hat{\zeta}_{|\pi_{1}}\dots\hat{\zeta}_{|\pi_{n}}$ are feasible
counterexample traces proving that
$\forall\pi_{1}.~{}\dots\forall\pi_{n}.~{}\psi$ does not hold.

$\Leftarrow$ Assume that $P$ does not satisfy $\varphi$. Then, there are trace
$\sigma_{\pi_{1}},\dots\sigma_{\pi_{n}}\in\mathcal{L}(P)$ and computations
$\zeta_{\pi_{1}},\dots\zeta_{\pi_{n}}$ such that
$\zeta_{\pi_{1}}\smalltriangleleft\sigma_{\pi_{1}}\wedge\dots\wedge\zeta_{\pi_{n}}\smalltriangleleft\sigma_{\pi_{n}}$
and
$\hat{\zeta}^{\prime}=\emptyset[\pi_{1},\zeta_{\pi_{1}}]\dots[\pi_{n},\zeta_{\pi_{n}}]\models\neg\varphi$.
This means by Lemma 1 that
$Seq(\hat{\zeta}^{\prime})\models_{LTL}\neg\varphi$, so
$Seq(\hat{\zeta}^{\prime})$ is accepted by $A_{\neg\varphi}$. Set
$\sigma_{t}=({(\sigma_{\pi_{1}})_{\pi_{1}}}_{t};\dots;~{}{(\sigma_{\pi_{n}})_{\pi_{n}}}_{t})$
and $\sigma=\sigma_{0}\sigma_{1}\dots$. Then,
$\mathit{combine}(\sigma,Seq(\zeta))$ is a trace of $P\otimes
A_{\neg\varphi}$. By Lemma 7,
$\widetilde{(\zeta_{\pi_{1}},\dots,\zeta_{\pi_{n}})}\smalltriangleleft\mathit{combine}(\sigma,Seq(\zeta^{\prime}))$,
so this is also a feasible trace.

###  0.A.6 Proof of Theorem 5.4

We now prove Theorem 5.4. To do that, we need the following lemma: recall that
for a program execution $\sigma_{\pi}$, $(\sigma_{\pi})_{\pi}$ means renaming
every cell $c$ in $\sigma_{\pi}$ to $c_{\pi}$ and every input $i$ to
$i_{\pi}$.

###### Lemma 8

Let $\sigma\in\mathit{Stmt}^{\omega}$ be feasible and
$\sigma_{t}=(((\sigma_{\pi_{1}})_{\pi_{1}})_{t},\dots,((\sigma_{\pi_{n}})_{\pi_{n}})_{t})$
for some $\sigma_{\pi_{1}},\dots\sigma_{\pi_{n}}$. Then
$\sigma_{\pi_{1}},\dots,\sigma_{\pi_{n}}$ are also all feasible.

###### Proof

As $\sigma$ is feasible, we know that $\hat{\zeta}\smalltriangleleft\sigma$
for some $\hat{\zeta}$. For all $1\leq j\leq n$, we define $\zeta_{\pi_{j}}$
by

$\displaystyle(\zeta_{\pi_{j}})_{t}$ $\displaystyle=(\hat{\zeta}_{t\cdot
n+j-1})_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}$
$\displaystyle\zeta_{\pi_{j}}$
$\displaystyle=(\zeta_{\pi_{j}})_{0}~{}(\zeta_{\pi_{j}})_{1}\dots$

where $\hat{a}_{|(\mathbb{I}\cup\mathbb{C})_{\pi_{j}}}$ as before means
restricting the domain of the assignment to the cells and inputs labeled with
$\pi_{j}$, thus excluding the variables from other traces. Moreover, the cells
and inputs are again renamed from $c_{\pi_{j}}$ to $c$ or $i_{\pi_{j}}$ to
$i$. $t\cdot m+j-1$ is the index of $(\sigma_{\pi_{j}})_{t}$ in $\sigma$.

We show that for all time points $t$,
$\zeta_{\pi_{j}}\smalltriangleleft_{t}\sigma_{\pi_{j}}$

  * •

Case $(\zeta_{\pi_{j}})_{t}=\mathit{assert}(\tau_{P})$
We know that $\hat{\zeta}\smalltriangleleft_{t\cdot m+j-1}\sigma$ and thus

$\displaystyle\eta(\hat{\tau_{P}},\hat{\zeta}_{t\cdot
m+j-1})=true\wedge\forall c\in\mathbb{C}\times\Pi.~{}\hat{\zeta}_{t\cdot
m+j-1}(c)=\hat{\zeta}_{t\cdot m+j-2}.$

Moreover $\eta(\tau_{P},(\zeta_{\pi_{j}})_{t})$ is also true as $\tau_{P}$
does not contain variables from other traces. It remains to show that

$\displaystyle\forall
c\in\mathbb{C}.~{}((\zeta_{\pi_{j}})_{t})(c)=(\zeta_{\pi_{j}})_{t-1}(c)$

This is also true as the only cells changed in $\hat{\zeta}_{(t-1)\cdot
m+j-1},\dots\hat{\zeta}_{t\cdot m+j-2}$ are cells from other traces.

  * •

The remaining two cases are analogous.

We now prove Theorem 5.4

###### Proof

Assume that $P^{m}\backslash(P^{n}\otimes
A_{\psi})_{k,C(k^{\prime})}^{\forall}$ has a feasible trace $\sigma$ with
$\hat{\zeta}\smalltriangleleft\sigma$. By Lemma 8, this means that