11institutetext: CISPA Helmholtz Center for Information Security, Saarbrücken,
Germany 11email<EMAIL_ADDRESS>
22institutetext: Microsoft Research, Cambridge, UK
22email<EMAIL_ADDRESS>
# Reactive Synthesis of
Smart Contract Control Flows

Bernd Finkbeiner 11 Jana Hofmann 22 Florian Kohn 11 Noemi Passing 11

###### Abstract

Smart contracts are small but highly error-prone programs that implement
agreements between multiple parties. We present a reactive synthesis approach
for the automatic construction of smart contract state machines. Towards this
end, we extend temporal stream logic (TSL) with universally quantified
parameters over infinite domains. Parameterized TSL is a convenient logic to
specify the temporal control flow, i.e., the correct order of transactions, as
well as the data flow of the contract’s fields. We develop a two-step approach
that 1) synthesizes a finite representation of the – in general – infinite-
state system and 2) splits the system into a compact hierarchical architecture
that enables efficient handling of the state machine in Solidity. We implement
the approach in our tool SCSynt, which leverages efficient symbolic algorithms
based on the observation that smart contract specifications naturally fall
into the safety fragment. As a result, SCSynt synthesizes correct-by-design
Solidity code from various specifications within seconds.

###### Keywords:

Reactive Synthesis Smart Contracts Temporal Stream Logic.

##  1 Introduction

Smart contracts are small programs that implement digital contracts between
multiple parties. They are deployed on the blockchain and thereby remove the
need for a trusted third party that enforces a correct execution of the
contract. Recent history, however, has witnessed numerous bugs in smart
contracts, some of which led to substantial monetary losses. One critical
aspect is the implicit state machine of a contract: to justify the removal of
a trusted third party – a major selling point for smart contracts – all
parties must trust that the contract indeed enforces the agreed order of
transactions.

Formal methods play a significant role in the efforts to improve the
trustworthiness of smart contracts. Indeed, the _code is law_ paradigm is
shifting towards a _specification is law_ paradigm
[DBLP:journals/corr/abs-2205-07529]. Formal verification has been successfully
applied to prove the correctness of the implicit state machine of smart
contracts, for example, by verifying the contract against temporal logic
specifications [DBLP:conf/sp/PermenevDTDV20, DBLP:conf/sp/StephensFMLD21,
nehai2018model] or a given state machine [DBLP:conf/vstte/0001LCPDBNF19].
Other approaches model the control flow with state machines and construct
Solidity code from it [zupan2020secure, DBLP:conf/fc/MavridouL18,
DBLP:journals/insk/CiccioCDGLLMPTW19, DBLP:journals/spe/Lopez-PintadoGD19].
Synthesis, i.e., the automatic construction of Solidity code _directly_ from a
temporal specification, has hardly been studied so far (except for a first
step [DBLP:journals/corr/abs-1906-02906], see related work paragraph). This is
despite the fact that the benefits of synthesis are especially applicable to
smart contracts. Many contracts extend standardized classes like the ERC20
token standard with new functionality. Synthesis as a property-oriented
approach enables an incremental development process: specifications can be
easily extended with additional conjuncts describing new features. The
implications on the state machine are handled by the synthesis algorithm.

In this paper, we study the synthesis of smart contracts from temporal stream
logic (TSL), which we equip with universally quantified parameters. TSL
extends linear-time temporal logic (LTL) with cells that hold data from an
infinite domain. Additionally, it uses uninterpreted functions and predicates.
These features enable us to reason about the order of transactions as well as
the data flow of the contract’s fields. To distinguish method calls from
different callers, we extend the logic with universally quantified parameters.
For example, the following parameterized TSL formula expresses that every
voter can only vote once and that a field numVotes is increased with every
vote.

⬇

$\forall$m. $\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(vote(m)
$\rightarrow$ $\llbracket$numVotes $\leftarrowtail$ numVotes $+$ 1$\rrbracket$
$\land$ $\operatorname{\leavevmode\hbox to6.66pt{\vbox
to6.66pt{\pgfpicture\makeatletter\hbox{\hskip 3.33249pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@moveto{3.09999pt}{2.325pt}\pgfsys@curveto{3.09999pt}{4.0371pt}{1.7121pt}{5.42499pt}{0.0pt}{5.42499pt}\pgfsys@curveto{-1.7121pt}{5.42499pt}{-3.09999pt}{4.0371pt}{-3.09999pt}{2.325pt}\pgfsys@curveto{-3.09999pt}{0.6129pt}{-1.7121pt}{-0.775pt}{0.0pt}{-0.775pt}\pgfsys@curveto{1.7121pt}{-0.775pt}{3.09999pt}{0.6129pt}{3.09999pt}{2.325pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.325pt}\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}}}\operatorname{\leavevmode\hbox
to6.28pt{\vbox to6.28pt{\pgfpicture\makeatletter\hbox{\hskip
0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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$vote(m))

Due to the universal quantification over an infinite domain, the above formula
describes an infinite-state system. This poses the challenges of 1)
synthesizing a finite representation of the system that 2) can be translated
into a Solidity contract that keeps the gas consumption at a moderate level.

We proceed in two steps. First, we observe that smart contract specifications
fall into the safety fragment, which enables us to use the simpler past-time
fragment of TSL. Unfortunately, we show that the realizability problem of
pastTSL is already undecidable, even without parameters. For unparameterized
pastTSL formulas, however, we can still employ a sound reduction to LTL,
following [FinkbeinerKPS19].

In a second step, we lift the synthesis to parameterized pastTSL. We present a
sound algorithm that splits the infinite-state machine into a hierarchical
structure of smaller, distributed finite-state machines. This architecture
minimizes the number of transactions needed to keep the system up to date at
runtime.

We implement the toolchain in our tool SCSynt, which, due to the past-time
fragment, leverages efficient symbolic algorithms. We evaluate SCSynt on ten
different smart contract specifications, and obtain an average synthesis time
of two seconds. Our largest specification is based on Avolab’s NFT auction
[NFTReference] and produces a state machine with 12 states in 12 seconds. To
summarize, we

  * •

show how to specify smart contract control flows in pastTSL with and without
parameters,

  * •

prove undecidability of the general realizability problem of pastTSL,

  * •

define pastTSL with universally quantified parameters and show how to
synthesize infinite-state machines with an efficient representation in
Solidity,

  * •

present SCSynt, the first tool that synthesizes smart contracts from a
temporal specification that reasons about the transaction order, method access
rights, and the fields’ data flow.

#### Related Work.

Formal approaches to smart contracts range from the automatic construction of
contracts from state machines [DBLP:conf/fc/MavridouL18, MavridouLSD19], over
the verification against temporal logics [DBLP:conf/sp/PermenevDTDV20,
DBLP:conf/sp/StephensFMLD21, nehai2018model] and state machines
[DBLP:conf/vstte/0001LCPDBNF19, DBLP:journals/corr/abs-1812-08829], to
deductive verification approaches [dharanikota2021celestial,
DBLP:conf/ndss/KalraGDS18]. Closest to our work is a synthesis approach based
on LTL specifications [DBLP:journals/corr/abs-1906-02906]. The approach does
not reason about the contract’s data, neither about the current value of the
fields, nor about parameters like the method’s caller. To quote the authors of
[DBLP:journals/corr/abs-1906-02906]: the main challenge in the synthesis of
smart contracts is “how to strike a balance between simplicity and
expressivity […] to allow effective synthesis of practical smart contracts”.
TSL has been successfully applied to synthesize the control flow of FPGAs
[DBLP:journals/corr/abs-2101-07232] and functional reactive programs
[DBLP:conf/haskell/Finkbeiner0PS19]. To include domain-specific reasoning, TSL
has been extended with theories [FinkbeinerHP22] and SMT solvers
[RoderickTSLTheories]. A recent approach combines TSL reactive synthesis with
SyGus to synthesize implementations for TSL’s uninterpreted functions
[cispa3674]. Parameterized synthesis has so far focused on distributed
architectures parameterized in the number of components [JacobsB14, Party,
KhalimovJB13, MarkgrafHLNN20]. Orthogonal to this work, these approaches rely
on a reduction to bounded isomorphic synthesis [JacobsB14, Party,
KhalimovJB13] or apply a learning-based approach [MarkgrafHLNN20].

#### Overview.

We first provide some brief preliminaries on state machines, reactive
synthesis, and TSL. In Section 3, we demonstrate how to specify smart
contracts using pure pastTSL and prove the undecidability of its realizability
problem. Next, in Section 4, we introduce parameterized pastTSL and
demonstrate its features with the specification of an ERC20 contract. We
proceed with the synthesis algorithm for parameterized specifications in
Section 5. Finally, in Sections 6 and 7, we present the implementation and
evaluation of SCSynt.

##  2 Preliminaries

We assume familiarity with linear-time temporal logic (LTL). A definition with
past-time temporal operators can be found in [recursiveEvaluation, pastLTL].
We only assume basic knowledge about smart contracts; for an introduction we
refer to [Ethereum].

###  2.1 State Machines and Reactive Synthesis

We give a very brief introduction to Mealy machines, safety properties and
reactive synthesis. A more detailed version of these preliminaries is given in
Appendix 0.A. In this work, we interpret smart contracts as reactive systems
represented by _Mealy state machines_ [Mealy55]. A Mealy machine is a tuple
$(S,s_{0},\delta)$ of states $S$, initial state $s_{0}$, and transition
relation $\delta\subseteq S\times I\cup O\times S$. We work with
specifications that are _safety properties_ (see, [KupfermanV99,
DBLP:journals/tse/Lamport77]). Given an LTL safety formula $\varphi$, we can
represent its safety region with a Mealy machine, meaning that a trace $t$
satisfies $\varphi$ iff it is a trace of the Mealy machine.

$q_{1}$$q_{2}$$q_{3}$$\neg a|b$$\neg a|\neg b$$a|(b\lor\neg b)$$\neg a|\neg
b$$a|\neg b$$\neg a|\neg b$ Figure 1: Exemplary winning region. $|$ separates
inputs and outputs.

For a safety specification, the _reactive synthesis_ problem is to determine
the _winning region_ , i.e., the maximal subset of its safety region such that
for every state and input combination, there is a transition into said subset.
For specifications that consist of assumptions and guarantees, we only depict
the transitions of a winning region whose inputs are allowed by the
assumption. As an example, consider the specification with input $a$, output
$b$, assumption $\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\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}}}(a\rightarrow\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{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}}}a)$, and guarantee
$\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\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}}}((b\rightarrow\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{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}}}b)\land(b\rightarrow\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{2.58333pt}\pgfsys@lineto{4.95137pt}{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}}}\neg a))$. The
winning region for this example is depicted in Figure 1.

###  2.2 Past-time Temporal Stream Logic

PastTSL is the past-time variant of TSL [FinkbeinerKPS19], which extends LTL
with cells that can hold data from a possibly infinite domain. To abstract
from concrete data, TSL includes uninterpreted functions and predicates.
_Function terms $\tau_{f}\in\mathcal{T}_{F}$_ are recursively defined by

$\tau_{f}\Coloneqq\texttt{s}~{}\mid~{}f~{}\tau^{1}_{f}\ldots~{}\tau^{n}_{f}$

where s is either a cell ${{\texttt{c}}}\in\mathbb{C}$ or an input
$i\in\mathbb{I}$, and $f\in\Sigma_{F}$ is a function symbol. Constants are
0-ary function symbols. _Predicate terms $\tau_{p}\in\mathcal{T}_{P}$_ are
obtained by applying a predicate symbol $p\in\Sigma_{P}$ with
$\Sigma_{P}\subseteq\Sigma_{F}$ to a tuple of function terms. PastTSL formulas
are built according to the following grammar:

$\varphi,\psi\Coloneqq\neg\varphi\,\mid\,\varphi\land\psi\,\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{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\,\mid\,\varphi\operatorname{\mathcal{S}}\psi\,\mid\,\tau_{p}\,\mid\,\llbracket{{\texttt{c}}}\leftarrowtail\tau_{f}\rrbracket$

An _update term_
$\llbracket{{\texttt{c}}}\leftarrowtail\tau_{f}\rrbracket\in\mathcal{T}_{U}$
denotes that cell c is overwritten with $\tau_{f}$. The temporal operators are
called “Yesterday” $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{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}}}$ and “Since”
$\operatorname{\mathcal{S}}$. Inputs, function symbols, and predicate symbols
a purely syntactic objects. To assign meaning to them, let $\mathcal{V}$ be
the set of values with $\mathbb{B}\subseteq\mathcal{V}$. We denote by
$\mathcal{I}:\mathbb{I}\to\mathcal{V}$ the evaluation of inputs. An
_assignment function_ ${\langle\cdot\rangle}:\Sigma_{F}\rightarrow\mathcal{F}$
assigns function symbols to functions
$\mathcal{F}=\bigcup_{n\in\mathbb{N}}\mathcal{V}^{n}\rightarrow\mathcal{V}$.

The type $\mathcal{C}=\mathbb{C}\to\mathcal{T}_{U}$ describes an update of all
cells. For every cell ${{\texttt{c}}}\in\mathbb{C}$, let
$\mathit{init}_{{{\texttt{c}}}}$ its initial value. The evaluation function
$\eta_{{\langle\cdot\rangle}}:\mathcal{C}^{\omega}\times\mathcal{I}^{\omega}\times\mathbb{N}\times\mathcal{T}_{F}\rightarrow\mathcal{V}$
evaluates a function term at point in time $t$ with respect to an _input
stream_ $\iota\in\mathcal{I}^{\omega}$ and a _computation_
$\varsigma\in\mathcal{C}^{\omega}$:

$\displaystyle\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t,{{\texttt{s}}})\coloneqq\begin{cases}\iota~{}t~{}{{\texttt{s}}}&\text{if
}{{\texttt{s}}}\in\mathbb{I}\\\ \mathit{init}_{{{\texttt{s}}}}&\text{if
}{{\texttt{s}}}\in\mathbb{C}\land t=0\\\
\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t-1,\varsigma~{}(t-1)~{}{{\texttt{s}}})&\text{if
}{{\texttt{s}}}\in\mathbb{C}\land t>0\end{cases}$
$\displaystyle\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t,f~{}\tau_{0}\dots\tau_{m-1})\coloneqq\langle
f\rangle~{}\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t,\tau_{0})~{}\dots~{}\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t,\tau_{m-1})$

Note that $\iota~{}t~{}{{\texttt{s}}}$ denotes the value of s at position $t$
according to $\iota$. Likewise, $\varsigma~{}t~{}{{\texttt{s}}}$ is the
function term that $\varsigma$ assigns to s at position $t$. For the semantics
of pastTSL, we concentrate on the cases that differ from the standard, LTL-
like semantics. The full semantics is provided in Section 0.A.2.

$\displaystyle\varsigma,\iota,t\models_{{\langle\cdot\rangle}}\llbracket{{\texttt{v}}}\leftarrowtail\tau\rrbracket~{}$
iff $\displaystyle~{}\varsigma~{}t~{}{{\texttt{v}}}\equiv\tau$
$\displaystyle\varsigma,\iota,t\models_{{\langle\cdot\rangle}}p~{}\tau_{0}\dots\tau_{m}~{}$
iff
$\displaystyle~{}\eta_{{\langle\cdot\rangle}}(\varsigma,\iota,t,p~{}\tau_{0}\dots\tau_{m-1})$

We use $\equiv$ to syntactically compare two terms. We derive three additional
operators: $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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
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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{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}}}\neg\varphi$,
$\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{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:=\mathit{true}\operatorname{\mathcal{S}}\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{2.58333pt}\pgfsys@lineto{4.95137pt}{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:=\lnot\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{2.58333pt}\pgfsys@lineto{5.5972pt}{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}}}\lnot\varphi$. The
difference between $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{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}}}$ and “Weak
Yesterday” $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}$ is that
$\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.72221pt}{2.58333pt}\pgfsys@lineto{1.72221pt}{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}}}$ evaluates to
$\mathit{false}$ in the first step, $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}$ to $\mathit{true}$.
We use pastTSL formulas to describe safety properties. Therefore, we define
that computation $\varsigma$ and an input stream $\iota$ satisfy a pastTSL
formula $\varphi$, written
$\varsigma,\iota\models_{{\langle\cdot\rangle}}\varphi$, if $\forall
t\in\mathbb{N}\mathpunct{.}\varsigma,\iota,t\models_{{\langle\cdot\rangle}}\varphi$.

The realizability problem of a pastTSL formula $\varphi$ asks whether there
exists a strategy which reacts to predicate evaluations with cell updates
according to $\varphi$. Formally, a strategy is a function
$\sigma:(2^{\mathcal{T}_{P}})^{+}\rightarrow\mathcal{C}$. For
$\iota\in\mathcal{I}^{\omega}$, we write $\sigma(\iota)$ for the computation
$\varsigma=\sigma(\iota[0])~{}\sigma(\iota[0..1])~{}\sigma(\iota[0..2])\ldots$
A strategy induces an infinite _strategy tree_ that branches according to the
predicate evaluations and whose nodes are labeled with the cell updates chosen
by the system.

######  Definition 1 ([FinkbeinerKPS19]).

A pastTSL formula $\varphi$ is _realizable_ if, and only if, there exists a
strategy $\sigma:(2^{\mathcal{T}_{P}})^{+}\rightarrow\mathcal{C}$ such that
for every input stream $\iota\in\mathcal{I}^{\omega}$ and every assignment
function ${\langle\cdot\rangle}:\Sigma_{F}\rightarrow\mathcal{F}$ it holds
that $\sigma(\iota),\iota\models_{{\langle\cdot\rangle}}\varphi$.

##  3 Synthesis from Pure PastTSL Specifications

We first demonstrate the use of pastTSL for the specification of smart
contracts with the example of a small voting contract. Second, we show that
even though past-time variants of temporal logics usually lead to
significantly easier algorithms [KupfermanV99], the pastTSL realizability
problem is undecidable in general.

#### Form of our Specifications.

Our specifications describe the temporal control flow of the contract’s method
calls and the data flow of its fields. We distinguish between _requirements_
$\varphi_{R}$, _obligations_ $\varphi_{O}$, and _assumptions_ $\varphi_{A}$.
Requirements enforce the right order of method calls with correct arguments.
Obligations describe the data flow in the fields of the contract. Assumptions
formulate properties of uninterpreted predicates that are needed for the
synthesis to succeed. Each type of specification can be given as invariant
$\varphi^{\mathit{inv}}$ or as initial formula $\varphi^{\mathit{init}}$.
Together, they form the following pastTSL formula, which we, according to the
definition of pastTSL, require to hold globally:

$(\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}\mathit{false}\rightarrow\varphi^{\mathit{init}}_{A}\land\varphi^{\mathit{init}}_{R})\land(\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{2.58333pt}\pgfsys@lineto{4.95137pt}{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^{\mathit{inv}}_{A}\land\varphi^{\mathit{inv}}_{R}))\rightarrow(\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}\mathit{false}\rightarrow\varphi^{\mathit{init}}_{O})\land\varphi^{\mathit{inv}}_{O}$

We use $\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\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@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.72221pt}{2.36806pt}\pgfsys@lineto{-1.39905pt}{2.77202pt}\pgfsys@curveto{-1.10196pt}{3.14337pt}{-0.5885pt}{3.17181pt}{-0.25223pt}{2.83554pt}\pgfsys@lineto{0.25223pt}{2.3311pt}\pgfsys@curveto{0.5885pt}{1.99483pt}{1.10196pt}{2.02327pt}{1.39905pt}{2.39462pt}\pgfsys@lineto{1.72221pt}{2.7986pt}\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}}}\mathit{false}$ to
refer to the first position of a trace. In the following, we indicate
invariants with a preceding $\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\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}}}$ operator to improve
readability.

###  3.1 Example: Voting Contract

We specify a small voting contract with three methods: vote, close, and
reveal. The fields of the contract are described with TSL’s cells, here we use
a single cell voters. In the context of smart contracts, we use the terms
cells and fields interchangeably. Additionally, our specification uses an
input sender, which holds the current caller of the method, and a constant
owner(), which is the static owner of the contract. The requirements
$\varphi_{R}$ are a conjunct of the following formulas.

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$((close
$\rightarrow$ $\operatorname{\leavevmode\hbox to6.66pt{\vbox
to6.66pt{\pgfpicture\makeatletter\hbox{\hskip 3.33249pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@moveto{3.09999pt}{2.325pt}\pgfsys@curveto{3.09999pt}{4.0371pt}{1.7121pt}{5.42499pt}{0.0pt}{5.42499pt}\pgfsys@curveto{-1.7121pt}{5.42499pt}{-3.09999pt}{4.0371pt}{-3.09999pt}{2.325pt}\pgfsys@curveto{-3.09999pt}{0.6129pt}{-1.7121pt}{-0.775pt}{0.0pt}{-0.775pt}\pgfsys@curveto{1.7121pt}{-0.775pt}{3.09999pt}{0.6129pt}{3.09999pt}{2.325pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.54999pt}{2.13124pt}\pgfsys@lineto{-1.25912pt}{2.49483pt}\pgfsys@curveto{-0.99174pt}{2.82904pt}{-0.52965pt}{2.85464pt}{-0.227pt}{2.552pt}\pgfsys@lineto{0.227pt}{2.09798pt}\pgfsys@curveto{0.52965pt}{1.79533pt}{0.99174pt}{1.82094pt}{1.25912pt}{2.15515pt}\pgfsys@lineto{1.54999pt}{2.51874pt}\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}}}$
$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.35625pt}{2.325pt}\pgfsys@lineto{4.45622pt}{2.325pt}\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$close)
$\land$ (reveal $\rightarrow$ $\operatorname{\leavevmode\hbox to7.83pt{\vbox
to7.83pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.58875pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@lineto{3.68124pt}{6.00623pt}\pgfsys@lineto{7.36247pt}{2.325pt}\pgfsys@lineto{3.68124pt}{-1.35625pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.93748pt}{2.325pt}\pgfsys@lineto{5.03748pt}{2.325pt}\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}}}$ close))

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(close $\rightarrow$
sender $=$ owner() $\land$ time $>$ cTime())

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(vote $\rightarrow$
$\neg$(sender $\in$ voters) $\land$ $\neg$(time $>$ cTime()))

Technically, close is syntactic sugar for a predicate term
isClose(methodinput). In our tool (see Section 6), we automatically add that
at most one method is called in each step. sender refers to the caller of the
method. The first invariant describes the control flow of the contract, the
other two express conditions that must hold for a call. E.g., method close can
only be called by the owner and after a threshold cTime() was passed. Lastly,
as obligations $\varphi_{O}$, we state that the field voters is updated when
vote is called and left unchanged otherwise:

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(vote $\rightarrow$
$\llbracket$voters $\leftarrowtail$ add(sender, voters)$\rrbracket$)

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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$vote
$\rightarrow$ $\llbracket$voters $\leftarrowtail$ voters$\rrbracket$)

We also need a typical consistency assumption on the time input:

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$($\operatorname{\leavevmode\hbox
to6.66pt{\vbox to6.66pt{\pgfpicture\makeatletter\hbox{\hskip
3.33249pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@moveto{3.09999pt}{2.325pt}\pgfsys@curveto{3.09999pt}{4.0371pt}{1.7121pt}{5.42499pt}{0.0pt}{5.42499pt}\pgfsys@curveto{-1.7121pt}{5.42499pt}{-3.09999pt}{4.0371pt}{-3.09999pt}{2.325pt}\pgfsys@curveto{-3.09999pt}{0.6129pt}{-1.7121pt}{-0.775pt}{0.0pt}{-0.775pt}\pgfsys@curveto{1.7121pt}{-0.775pt}{3.09999pt}{0.6129pt}{3.09999pt}{2.325pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{-1.54999pt}{2.325pt}\pgfsys@lineto{1.54999pt}{2.325pt}\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}}}$(time $>$ cTime())
$\rightarrow$ time $>$ cTime())

For a useful contract, we would probably also add fields to count the votes
for each respective candidate. We skip this part in this toy example.

#### On Safety Properties.

For smart contracts, safety specifications seem to lie in a sweet spot between
expressiveness and synthesis performance (see Section 7). In our experience,
this choice did not feel restrictive, as many contracts enforce that no party
can betray the other with a malicious sequence of transactions.

###  3.2 PastTSL Undecidability

We establish undecidability of pastTSL realizability by a reduction from the
universal halting problem of lossy counter machines
[DBLP:journals/tcs/Mayr03]. We employ a version of lossiness where a counter
can suddenly become zero if it is tested for zero [DBLP:journals/tcs/Mayr03].
A definition of $n$-counter machines is provided in Section 0.B.1.

######  Theorem 3.1 ().

The pastTSL realizability problem is undecidable.

We use the undecidable problem whether a $4$-counter machine with lossiness
halts from every initial configuration [DBLP:journals/tcs/Mayr03]. The main
idea is to use two cells $c^{\mathit{inc}}_{x}$ and $c^{\mathit{dec}}_{x}$ for
each counter $x$. Expression $f(c^{\mathit{inc}}_{x})$ increases $x$ and
$f(c^{\mathit{dec}}_{x})$ decreases it. To test a counter for zero, we use
$\psi^{0}_{x}:=p(c^{\mathit{inc}}_{x})\leftrightarrow
p(c^{\mathit{dec}}_{x})$. If $x$ really is zero, then $\psi^{0}_{x}$ _must_
evaluate to true according to the semantics of pastTSL. If not, $\psi^{0}_{x}$
_may_ evaluate to true, which corresponds to lossy behavior. We use the
temporal operators of pastTSL to encode that the machine never reaches a
halting state. The full proof is given in Section 0.B.1.

#### PastTSL Synthesis via PastLTL Approximation

Even if the pastTSL synthesis problem is undecidable, we can employ a
reduction from TSL to LTL proposed in [FinkbeinerKPS19] to synthesize a state
machine. Given a TSL formula $\varphi$, we define

$\psi_{\text{pastLTL\@}}\coloneqq\mathit{syntacticConversion}(\varphi)\land\mathit{cellUpdates}(\varphi)$

where $\mathit{syntacticConversion}(\varphi)$ replaces all predicate and
update terms of $\varphi$ with unique atomic propositions, e.g., $a_{p\\_x}$
for $p({{\texttt{x}}})$ and $a_{x\\_\mathit{to}\\_f\\_x}$ for
$\llbracket{{\texttt{x}}}\leftarrowtail f({{\texttt{x}}})\rrbracket$. Formula
$\mathit{cellUpdates}(\varphi)$ ensures that every cell is updated with
exactly one function term in each step. If $\varphi$ is a pastTSL formula,
then $\psi_{\text{pastLTL\@}}$ is a pastLTL formula.

The reduction is sound but not complete, i.e., the TSL formula might be
realizable even if the LTL formula is not. This is because the LTL formula
does not enforce consistent predicate evaluations on cells that logically must
contain the same value. As an example, after an update
$\llbracket{{\texttt{x}}}\leftarrowtail{{\texttt{y}}}\rrbracket$, all
predicates must evaluate to the same value on x and y according to the TSL
semantics. This is not enforced in the LTL formula, where setting $a_{p\\_x}$
to $\mathit{true}$ and $a_{p\\_y}$ to $\mathit{false}$ constitutes a valid
input. In the case of spurious unrealizability, [FinkbeinerKPS19] describes
how to refine the LTL formula to exclude the spurious input valuations.
Interestingly, for our smart contract specifications, we never encountered
spurious unrealizability. In practice, the approximation seems to work quite
well.

For the voting example of Section 3.1, the state machine is depicted in Figure
2. We automatically translate this state machine into Solidity code (c.f.
Section 6), which by design enforces a correct order of method calls and data
flow in the contract.

$q_{1}$$q_{2}$ vote $\land$ $\neg$ (sender $\in$ voters) $\land$ $\neg$ (time
> cTime()) $\mid$
$\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\leftarrowtail\texttt{add(sender,
{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters})}\rrbracket$
close $\land$ sender = owner() $\land$ time > cTime() $\mid$
$\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\rrbracket$
reveal $\land$ time > cTime() $\mid$
$\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\rrbracket$
Figure 2: Winning region of the voting specification.

##  4 Parameterized PastTSL

In this section, we introduce parameterized pastTSL for the specification of
smart contract temporal control flows. We first illustrate the logic by means
of two examples: an extension of the voting specification presented in Section
3.1 and an ERC20 token contract. We then formally define parameterized TSL
and, for approximations, parameterized LTL.

###  4.1 Parameterized Contract Specifications

#### Parameterized Voting Contract.

Parameters enable us to distinguish between different calls to the same
method. They may refer to the caller of the method or to one of the method’s
arguments. We write vote(m) for a call to method vote with parameter m; it is
syntactic sugar for isVote(methodinput, m). In this example, m refers to the
caller of the method (this information is added for the translation to
Solidity, see Section 6). Compared with the specification in Section 3.1, we
do not have to use a field that stores the voters in order to make sure that
everybody only votes once. Instead, we simply state:

⬇

$\forall$m. $\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(vote(m)
$\rightarrow$ $\operatorname{\leavevmode\hbox to6.66pt{\vbox
to6.66pt{\pgfpicture\makeatletter\hbox{\hskip 3.33249pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@moveto{3.09999pt}{2.325pt}\pgfsys@curveto{3.09999pt}{4.0371pt}{1.7121pt}{5.42499pt}{0.0pt}{5.42499pt}\pgfsys@curveto{-1.7121pt}{5.42499pt}{-3.09999pt}{4.0371pt}{-3.09999pt}{2.325pt}\pgfsys@curveto{-3.09999pt}{0.6129pt}{-1.7121pt}{-0.775pt}{0.0pt}{-0.775pt}\pgfsys@curveto{1.7121pt}{-0.775pt}{3.09999pt}{0.6129pt}{3.09999pt}{2.325pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.325pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{{}}{} {}{} {}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{-1.54999pt}{2.13124pt}\pgfsys@lineto{-1.25912pt}{2.49483pt}\pgfsys@curveto{-0.99174pt}{2.82904pt}{-0.52965pt}{2.85464pt}{-0.227pt}{2.552pt}\pgfsys@lineto{0.227pt}{2.09798pt}\pgfsys@curveto{0.52965pt}{1.79533pt}{0.99174pt}{1.82094pt}{1.25912pt}{2.15515pt}\pgfsys@lineto{1.54999pt}{2.51874pt}\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}}}\operatorname{\leavevmode\hbox
to6.28pt{\vbox to6.28pt{\pgfpicture\makeatletter\hbox{\hskip
0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.35625pt}{2.325pt}\pgfsys@lineto{4.45622pt}{2.325pt}\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$vote(m))

In the following, we do not explicitly add the universal quantification as all
parameters are always universally quantified.

#### ERC Token Contract.

As a second example, we illustrate how specifications with parameters can be
used to specify an ERC20 token system. We follow the Open Zeppelin
documentation [ERC20Spec] but also add additional functionality. An ERC20
token system provides a platform to transfer tokens between different
accounts. The core contract consists of methods transfer, transferFrom, and
approve. We do not model getters like totalSupply or balanceOf as they are not
relevant for the temporal behavior of the contract. From a synthesis point-of-
view, the challenge is that there is not only a global control flow but also
one for each pair of accounts interacting with the contract. We therefore use
two parameters m and n, where m refers to the address from which tokens are
subtracted and parameter n, whenever different from m, to the contract that
initiates the transfer. Parameterized fields correspond to mappings.

We only present some key aspects of the specification, the full spec can be
found in Section 0.C.1. First, if we want to transfer from m’s account, there
needs to be sufficient funds available:

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(transfer(m) $\lor$
transferFrom(m,n) $\rightarrow$ suffFunds(m, arg@amount))

Above, the label arg@ indicates that amount is the current method’s argument.
If n wants to transfer from m’s account, the requested amount must have been
approved. We use a mapping approved(m,n) to record the amount of tokens m
allows n to spend in their name.

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(transferFrom(m,n)
$\rightarrow$ approved(m,n) $\geq$ arg@amount

$\land$ $\llbracket$approved(m,n) $\leftarrowtail$
approved(m,n)-arg@amount$\rrbracket$)

The Open Zeppelin ERC20 contract offers various extensions of the core
contract, one of which is the ability to pause all transfers. We additionally
add methods localPause(m) and localUnpause(m). While pause stops _all_
transfers, localPause(m) can be called by m to stop transfers from m’s account
only. We specify local pausing as follows. Global pausing is specified
similarly.

⬇

$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\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}}}$(transferFrom(m,n)
$\lor$ transfer(m) $\lor$ approve(m,n) $\rightarrow$ (($\neg$localPause(m))
$\operatorname{\mathcal{S}}$ localUnpause(m)) $\lor$
$\operatorname{\leavevmode\hbox to6.28pt{\vbox
to6.28pt{\pgfpicture\makeatletter\hbox{\hskip 0.2325pt\lower-1.00749pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.465pt}\pgfsys@invoke{
}\pgfsys@roundjoin\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-0.775pt}\pgfsys@lineto{0.0pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{5.03748pt}\pgfsys@lineto{5.81248pt}{-0.775pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.34875pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{1.35625pt}{2.325pt}\pgfsys@lineto{4.45622pt}{2.325pt}\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$localPause(m))

Note that the correct addition and subtraction of tokens upon transfer must
currently still be implemented by hand. We discuss this limitation in Section
5.5.

As parameters are universally quantified, the specification describes a state
machine for each instantiation of the parameters. This state machine is
depicted in Figure 3.

$s_{1}$$s_{2}$$s_{3}$$s_{4}$localPause(m)pauselocalUnpause(m)unpausepauseunpauseapprove(m,n)
$\lor$ (transfer(m) $\land$ suffFunds(m,a)) $\lor$ (transferFrom(m,n) $\land$
suffFunds(m,a) $\land$ approved(m,n) $\geq$ a) Figure 3: Synthesized state
machine of the ERC20 token system with local pause function. Predicates that
are not relevant for the transition and all field updates are omitted for
readability. We also write a instead of arg@amount.

The different instances are not independent, though. The contract can be in
different states for different instantiations of m and n. But, if pause is
called, all instances must move to a state where no transfer is possible.

###  4.2 Parameterized LTL and TSL

We introduce parameterized TSL and parameterized LTL together with some
notation we make use of in the next section.

#### Parameterized TSL

Technically, parameterized TSL is TSL with quantification over infinitely many
constants and cells. Let $P$ be a set of parameters and $\mathbb{C}_{P}$ a set
of parameterized cells, where each cell is of the form
${{\texttt{c}}}(p_{1},\ldots,p_{m})$ with $p_{1},\ldots,p_{m}\in P$. A
parameterized TSL formula is a formula $\forall p_{1},\ldots,\forall
p_{n}\mathpunct{.}\psi$, where $\psi$ is a TSL formula with cells from
$\mathbb{C}_{P}$ and which allows parameters from $P$ as base terms in
function terms and predicate terms. We require that the formula is closed,
i.e., every parameter occurring in $\psi$ is bound in the quantifier prefix.

Parameterized TSL formulas are evaluated with respect to a domain $\mathbb{P}$
for the parameters. To keep the definition of the semantics simple, we assume
that $\mathbb{P}$ is a subset of the set of constants. We use
$\mu:P\rightarrow\mathbb{P}$ to denote a function that instantiates all
parameters. For each $\mu$, we assume that
${{\texttt{c}}}(\mu(p_{1}),\ldots,\mu(p_{m}))\in\mathbb{C}$, i.e., the
instantiation of a parameterized cell refers to a normal cell. Given a
parameterized TSL formula $\forall p_{1},\ldots,\forall
p_{n}\mathpunct{.}\psi$, let $\psi[\mu]$ be the TSL formula obtained by
replacing all parameters in $\psi$ according to $\mu$. Given a computation
$\varsigma$ and an input stream $\iota$, we define
$\varsigma,\iota\models\forall p_{1},\ldots,\forall p_{n}\mathpunct{.}\psi$
iff $\forall\mu:P\to\mathbb{P}\mathpunct{.}\varsigma,\iota\models\psi[\mu]$.

#### Parameterized LTL

Parameterized LTL has been studied in the settings parameterized verification
[DBLP:journals/ipl/AptK86] and parameterized synthesis [JacobsB14]. We define
it analogously to parameterized TSL. A parameterized LTL formula is a closed
formula $\forall p_{1},\ldots,p_{n}\mathpunct{.}\psi$ such that
$p_{1},\ldots,p_{n}\in P$ and $\psi$ is an LTL formula over atomic
propositions $\mathit{AP}$, each of the form $a(p_{1},\ldots,p_{m})$. We
usually denote the sequence $p_{1},\ldots,p_{m}$ with some $P_{i}$, for which
we also use set notation. We assume that every proposition occurs with only
one sequence of parameters, i.e., there are no
$a(P_{i}),a(P_{j})\in\mathit{AP}$ with $P_{i}\neq P_{j}$. If $a$ is not
parameterized, then $P_{i}=\emptyset$. Given $P_{i}=(p_{1},\ldots,p_{m})$ and
$\mu:P\rightarrow\mathbb{P}$, $P_{i}[\mu]$ denotes
$(\mu(p_{1}),\ldots,\mu(p_{m}))$. For $a(P_{i})\in\mathit{AP}$ we write,
slightly abusing notation, $a\in\mathit{AP}$ and $a[\mu]$ for $a(P_{i}[\mu])$.
Let $\mathit{AP}_{\mathbb{P}}=\\{a[\mu]\mid
a\in\mathit{AP},\mu:P\rightarrow\mathbb{P}\\}$. For each
$\alpha\in\mathit{AP}_{\mathbb{P}}$, there is exactly one $a$ such that
$a[\mu]=\alpha$ for some $\mu$. A trace $t$ over $\mathit{AP}_{\mathbb{P}}$
satisfies a parameterized LTL formula $\forall
p_{1},\ldots,p_{n}\mathpunct{.}\psi$ if for all $\mu$, it holds that
$t\models\psi[\mu]$.

We can approximate parameterized TSL with parameterized LTL. We translate TSL
predicate and update terms to LTL input and output propositions as described
in Section 3.2 but keep all parameters a term contains as parameters of the
proposition. For example, a(m) $>$ b(n) is translated to some parameterized
proposition $\mathit{a\\_greater\\_b}(m,n)$.

##  5 Synthesis from Parameterized PastTSL

The synthesis of a smart contract from a pastTSL specification comes with
several challenges. Our aim is to translate the state machine to Solidity
code, so we need to make sure that the state machine is finitely
representable. Furthermore, as each Solidity computation costs gas, we need to
minimize the number transactions needed to update the transition system at
runtime. We first formulate synthesis problem formally and describe our
approach in a nutshell, before we proceed with the algorithm and finally prove
its correctness.

###  5.1 Problem Definition

Let a parameterized pastLTL formula $\varphi=\forall
p_{1},\ldots,p_{n}\mathpunct{.}\psi$ over $\mathit{AP}=I\cup O$ be given,
which is the approximation of a parameterized pastTSL formula. For
$A\subseteq\mathit{AP}$, we write $A_{|O}$ instead of $A\cap O$. We denote the
set of atomic propositions that correspond to some method call f($P_{i}$) by
$I_{\mathit{call}}\subseteq I$ and the set of output propositions that denote
self-updates like
$\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}\rrbracket$
by $O_{\mathit{self}}\subseteq O$.

######  Definition 2.

Let $\mathbb{P}$ be a parameter domain. An infinite-state machine
$\mathcal{M}$ over $2^{\mathit{AP}_{\mathbb{P}}}$ _implements a smart
contract_ if (i) for each transition $(s,A,s^{\prime})\in\delta$, there is
exactly one $\alpha\in A$ with
$\alpha=\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}[\mu]$
for some $\mu$ and
$\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
I_{\mathit{call}}$ and (ii) in every state $s\in S$, for every instance $\mu$,
and all inputs $A_{I}\subseteq I$, there exists a transition
$(s,A,s^{\prime})\in\delta$ such that $\\{a[\mu]\mid a\in A_{I}\\}\subseteq
A$.

The definition requires that in each state, every instance must have the
possibility to make progress. An instance is given by an instantiation $\mu$
of the parameters. In each transition, on the other hand, the state machine
processes a method call for exactly one instance of the parameters. This does
not mean that only one instance makes progress per transition. For example, if
localPause(m) is called with $\mu(\texttt{m})=1$ in the ERC20 token system
from Section 4.1, this affects all instances $\mu^{\prime}$ with
$\mu^{\prime}(\texttt{m})=1$. To project on steps relevant for an instance
$\mu$, we project the traces of $\mathcal{M}$ to steps that either include a
method call to $\mu$ or a non-self-update of one of $\mu$’s fields. For
$A\subseteq\mathit{AP}_{\mathbb{P}}$, we define $A_{\mu}$ as $\\{\alpha\in
A\mid\exists a\in\mathit{AP}\mathpunct{.}\alpha=a[\mu]\\}$. Given
$t\in\mathit{traces}(\mathcal{M})$, let
$t^{\prime}=(t[0])_{\mu}(t[1])_{\mu}\ldots$. Now, we define $t_{\mu}$ to be
the trace obtained from $t^{\prime}$ by deleting all positions $i$ such that
$(t[i]_{\mu})_{|O}\subseteq O_{\mathit{self}}$ and
$\neg\exists\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
I_{\mathit{call}}\mathpunct{.}\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}[\mu]\in
t^{\prime}[i]$. Note that $t_{\mu}$ might be a finite trace even if $t$ is
infinite. Since $t_{\mu}$ only deletes steps from $t$ that do not change the
value of the cells, $t_{\mu}$ still constitutes a sound computation regarding
the original pastTSL formula. We define
$\mathit{traces}_{\mu}(\mathcal{M})=\\{t_{\mu}\mid
t\in\mathit{traces}(\mathcal{M})\\}$. Similarly,
$\mathit{finTraces}_{\mu}(\mathcal{M})=\\{t_{\mu}\mid
t\in\mathit{finTraces}(\mathcal{M})\\}$. We use $\mathit{traces}(\mathcal{M})$
and $\mathit{finTraces}(\mathcal{M})$ for the (in)finite traces of a state
machine, see Section 0.A.1.

######  Definition 3.

A state machine implementing a smart contract _satisfies a pastLTL formula_
$\varphi=\forall p_{1}\mathpunct{.},\ldots,\forall p_{n}\mathpunct{.}\psi$ if
for all instances $\mu$ and traces
$t_{\mu}\in\mathit{traces}_{\mu}(\mathcal{M})$, we have
$t_{\mu}\models\psi[\mu]$.

###  5.2 Approach in a Nutshell

$q_{1}$$q_{2}$$K\\!=\\!\\{s_{1},s_{2}\\}$$K\\!=\\!\\{s_{3},s_{4}\\}$
$(\texttt{in\\_}s_{1}\lor\texttt{in\\_}s_{2})$ $\land$ pause unpause $\land$
$(\texttt{in\\_}s_{3}\lor\texttt{in\\_}s_{4})$

(a) System for $\emptyset$.

$q_{1}$$q_{2}$$K\\!=\\!\\{s_{1},s_{3}\\}$$K\\!=\\!\\{s_{2},s_{4}\\}$
$\texttt{in\\_}s_{1}$ $\land$ localPause(m) localUnpause(m) $\land$
$\texttt{in\\_}s_{2}$ transfer(m) $\land$ $\texttt{in\\_}s_{1}$

(b) System for $\\{\texttt{m}\\}$.

$q_{1}$$K\\!=\\!\\{s_{1},s_{2},s_{3},s_{4}\\}$ $\texttt{in\\_}s_{1}$ $\land$
(approve(m,n) $\lor$ transferFrom(m,n))

(c) System for $\\{\texttt{m},\texttt{n}\\}$.

Figure 4: State machines for all non-empty parameter sets. For readability, we
omit the value predicates and field updates.

In a nutshell, we proceed as follows. First, we interpret the specification as
being unquantified, i.e., we treat parameters as being part of the
proposition’s name. The synthesized finite-state machine describes the
behavior of a single instance. The different instances depend on each other;
therefore, it is not possible to just keep a duplicate of the state machine
for every instance: if localPause(m) is called for $\texttt{m}=\texttt{1}$,
this needs to be recorded in all state machines for instances that share the
value of m. We would have to iterate over all state machines of so-far
observed instances, which would be way too costly in Solidity.

To obtain a more feasible solution, we describe an algorithm to split the
synthesized state machine into multiple machines, one for each subset of
parameters. Together, these machines represent the full system. For the ERC20
example, we obtain the three systems depicted in Figure 4. Each node is
labeled with a “knowledge” set $K$. If we follow a run of the original system
in all subsystems, the knowledge states denote which state the original system
might be in. We also add guards to the transitions, where
$\texttt{in\\_}s_{1}$ means that the subsystem can only take the transition if
it knows for sure that the full system is currently in state $s_{1}$. The
systems share their knowledge about the state of the original system in a
hierarchical structure. A subsystem for parameters $P_{i}$ may share its
knowledge only with systems for parameters $P_{j}\supseteq P_{i}$. We define
an independence check that is successful if every subsystem comes at every
state to a definite conclusion whether a transition can be taken.

In the following, we first describe the splitting algorithm together with two
technical requirements on the synthesized finite-state machine and the
independence criterion. For the correctness argument, we define how the
distributed knowledge about the current state of the system can be put
together to construct a realizing infinite-state machine. Finally, we argue
that the approach is sound, i.e., if all criteria are met, then the infinite-
state machine implements a smart contract that satisfies the parameterized
formula.

###  5.3 Splitting Algorithm

Let $\varphi=\forall p_{1}\ldots\forall p_{n}\mathpunct{.}\psi$ and let
$\mathcal{W}=(S_{\mathcal{W}},s^{0}_{\mathcal{W}},\delta_{\mathcal{W}})$ be
the finite-state machine over $\mathit{AP}$ that represents the winning region
of $\psi$. We define two requirements on $\mathcal{W}$, which can be checked
easily by inspecting all its transitions. First, we require that calls to a
method parameterized with parameter sequence $P_{i}$ only lead to field
updates parameterized with the same parameter sequence.

######  Requirement 1 (Local Updates).

For every transition $(s,A,s^{\prime})\in\delta_{\mathcal{W}}$, if
$\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}o}\texttt{($P_{i}$)}\in
A_{|O}$ and
$\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}o}\texttt{($P_{i}$)}\notin
O_{\mathit{self}}$, then there is a method call proposition
$\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
A$.

Second, whether a method can be called at a given state must not depend on
predicates with parameters that are not included in the current method call.

######  Requirement 2 (Independence of Irrelevant Predicates).

For every $(s,A,s^{\prime})\in\delta_{\mathcal{W}}$, if
$\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
A$, then for every $a(P_{j})\in I$ with $P_{j}\not\subseteq P_{i}$ and
$a(P_{j})\notin I_{\mathit{call}}$, there is a transition
$(s,A^{\prime},s^{\prime})$ with $a(P_{j})\in A$ iff $a(P_{j})\notin
A^{\prime}$ and $A_{|O}=A^{\prime}_{|O}$.

If $\mathcal{W}$ satisfies the above requirements, we split the state machine
into multiple state machines, one for every subset $P_{i}$ of parameters. Each
$\mathcal{W}_{P_{i}}$ projects $\mathcal{W}$ to the method calls with
parameters $P_{i}$. We label each state of $\mathcal{W}_{P_{i}}$ with the
state’s knowledge regarding the global state of the contract. The algorithm to
construct $\mathcal{W}_{P_{i}}$ combines several standard automata-theoretic
concepts:

  1. 1.

Introduce a new guard proposition $\texttt{in\\_}s$ for every state $s\in
S_{\mathcal{W}}$ of $\mathcal{W}$. For every transition
$(s,A,s^{\prime})\in\delta_{\mathcal{W}}$, replace $A$ with
$A\cup\\{\texttt{in\\_}s\\}$.

  2. 2.

Label all transitions $(s,A,s^{\prime})\in\delta_{\mathcal{W}}$ for which
there is no
$\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
A$ with $\epsilon$. The result is a nondeterministic safety automaton with
$\epsilon$-edges.

  3. 3.

$\mathcal{W}_{P_{i}}$ is obtained by determinizing the safety automaton using
the standard subset construction. This removes all $\epsilon$ transitions.
During the construction, we label each state with the subset of
$S_{\mathcal{W}}$ it represents, these are the knowledge sets.

We use $S_{i}$ for the states of $\mathcal{W}_{P_{i}}$, $\delta_{i}$ for its
transition relation, and $K_{i}:S_{i}\rightarrow 2^{S_{\mathcal{W}}}$ for the
knowledge sets. Note that every transition in $\mathcal{W}$ is labeled with
exactly one method call proposition and is therefore present in exactly one
$\mathcal{W}_{P_{i}}$. The following two propositions follow from the
correctness of the subset construction for the determinization of finite
automata. The first proposition states that the outgoing transitions of a
state $s_{i}\in\mathcal{W}_{P_{i}}$ are exactly the outgoing transitions of
all states $s\in K_{i}(s_{i})$.

######  Proposition 1.

For every state $s_{i}\in S_{i}$, if $s\in K_{i}(s_{i})$, then for all
$s^{\prime}\in S$ and $A\subseteq\mathit{AP}$,
$(s,A,s^{\prime})\in\delta_{\mathcal{W}}$ iff
$(s_{i},A\cup\\{\texttt{in\\_}s\\},s^{\prime}_{i})\in\delta_{i}$ for some
$s_{i}^{\prime}\in S_{i}$.

The second one states that the knowledge labels in $\mathcal{W}_{P_{i}}$ are
consistent with the transitions of $\mathcal{W}$.

######  Proposition 2.

Let $(s,A,s^{\prime})\in\delta_{\mathcal{W}}$ with
$\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}f}\texttt{($P_{i}$)}\in
A$. Then, for every state $s_{i}\in S_{i}$ with $s\in K_{i}(s_{i})$, and every
transition $(s_{i},A\cup\\{\texttt{in\\_}s\\},s^{\prime}_{i})\in\delta_{i}$,
it holds that $s^{\prime}\in K_{i}(s^{\prime}_{i})$. Furthermore, for every
$s_{j}$ of $\mathcal{W}_{P_{j}}$ with $i\neq j$, if $s\in K_{j}(s_{j})$, then
$s^{\prime}\in K_{j}(s_{j})$.

#### Check for Independence

We now define the check if transitions in $\mathcal{W}_{P_{i}}$ can be taken
independently of the current state of all $\mathcal{W}_{P_{j}}$ with
$P_{j}\not\subseteq P_{i}$. If the check is positive, we can implement the
system efficiently in Solidity: when a method f($P_{i}$) is called, we only
need to make progress in system $\mathcal{W}_{P_{i}}$ and whether the
transition can be taken only depends on parameters $P_{i}$.

Let $s_{i}$ and $s_{i}^{\prime}$ be states in $\mathcal{W}_{P_{i}}$ and
$A\subseteq\mathit{AP}$. Let
$G_{(s_{i},A,s_{i}^{\prime})}=\\{s\mid(s_{i},A\cup\\{\texttt{in\\_}s\\},s^{\prime}_{i})\in\delta_{i}\\}$
be the set of all guard propositions that occur on transitions from $s_{i}$ to
$s^{\prime}_{i}$ with $A$. Let $P_{j_{1}},\ldots P_{j_{l}}$ be the maximum set
of parameter subsets such that $P_{j_{k}}\subseteq P_{i}$ for $1\leq k\leq l$.
A transition $(s_{i},A,s^{\prime}_{i})$ is _independent_ if for all states
$s_{j_{1}},\ldots,s_{j_{l}}$ with $s_{j_{k}}\in S_{j_{k}}$ either

  1. (i)

$K_{i}(s_{i})\cap\bigcap_{1\leq k\leq l}{K_{j_{k}}(s_{j_{k}})}\subseteq
G_{(s_{i},A,s_{i}^{\prime})}$ or

  2. (ii)

$(K_{i}(s_{i})\cap\bigcap_{1\leq k\leq l}{K_{j_{k}}(s_{j_{k}})})\cap
G_{(s_{i},A,s_{i}^{\prime})}=\emptyset$.

The check combines the knowledge of $\mathcal{W}_{P_{i}}$ in state $s_{i}$
with the knowledge of each combination of states from
$\mathcal{W}_{P_{j_{1}}},\ldots,\mathcal{W}_{P_{j_{l}}}$. For each potential
combination, it must be possible to determine whether transition
$(s_{i},A,s_{i}^{\prime})$ can be taken. If the first condition is satisfied,
then the combined knowledge leads to the definite conclusion that
$\mathcal{W}$ is currently in a state where an $A$-transition can be taken. If
the second condition is satisfied, if definitely cannot be taken. If none of
the two is satisfied, then the combined knowledge of $P_{i}$ and all
$P_{j_{k}}$ is not sufficient to reach a definite answer. Note that some state
combinations $s_{i},s_{j_{1}},\ldots,s_{j_{l}}$ might be impossible to reach.
But then, we have that $K_{i}(s_{i})\cap\bigcap_{1\leq k\leq
l}{K_{j_{k}}(s_{j_{k}})}=\emptyset$ and the second condition is satisfied. The
check is successful if all transitions $(s_{i},A,s^{\prime}_{i})$ in all
$\delta_{i}$ are independent.

###  5.4 Correctness

If the above check is successful, all $\mathcal{W}_{P_{i}}$ together represent
an infinite-state machine $\mathcal{M}$ that implements a smart contract. We
construct $\mathcal{M}$ as follows. A state in $\mathcal{M}$ is a collection
of $n=|2^{P}|$ functions $f_{1},\ldots,f_{n}$, where
$f_{i}:\mathbb{P}^{m}\rightarrow S_{i}$ if
$P_{i}=(p_{i_{1}},\ldots,p_{i_{m}})$. Each $f_{i}$ indicates in which state of
$\mathcal{W}_{P_{i}}$ instance $\mu$ currently is. The initial state is the
collection of functions that all map to the initial states of their respective
$\mathcal{W}_{P_{i}}$. For every state $s=(f_{1},\ldots,f_{n})$ of
$\mathcal{M}$, every $P_{i}\subseteq P$, and every instance $\mu$, we add a
transition where $P_{i}[\mu]$ makes progress and all other instances stay
idle. Let $f_{i}(P_{i}[\mu])=s_{i}$, $s_{i}^{\prime}\in S_{i}$,
$A\subseteq\mathit{AP}$, and
$G_{(s_{i},A,s_{i}^{\prime})}=\\{s\mid(s_{i},A\cup\\{\texttt{in\\_}s\\},s_{i}^{\prime})\in\delta_{i}\\}$.
Let $P_{j_{1}},\ldots P_{j_{l}}$ be all subsets of $P_{i}$. If
$K_{i}(s_{i})\cap\bigcap_{1\leq k\leq
l}{K_{j_{k}}(f_{j_{k}}(P_{j_{k}}[\mu]))}\subseteq
G_{(s_{i},A,s_{i}^{\prime})}$, we add the transition
$(s,A^{\prime},s^{\prime})$ to $\mathcal{M}$, where $A^{\prime}$ and
$s^{\prime}$ are defined as follows.

$\displaystyle A^{\prime}$ $\displaystyle=\\{a[\mu]\mid a\in
A\\}\cup\\{o[\mu^{\prime}]\mid o\in O_{\mathit{self}},o[\mu^{\prime}]\neq
o[\mu]\\}$ $\displaystyle s^{\prime}$
$\displaystyle=(f_{1},\ldots,f_{i}[P_{i}[\mu]\mapsto
s_{i}^{\prime}],\ldots,f_{n})$

The label $A^{\prime}$ sets all propositions of instance $\mu$ as in $A$ and
sets all other input propositions to $\mathit{false}$. Of all other outputs
propositions, it only sets those denoting self-updates to $\mathit{true}$.

We observe that, as $\mathcal{W}$ describes a collection of strategies for
$\psi$, $\mathcal{M}$ describes a smart contract as defined in Definition 2.
It remains to prove that the traces of $\mathcal{M}$ satisfy $\varphi$
according to Definition 3. Most of the work is done in the following lemma. We
define $\mathcal{W}_{\mu}$ as the state machine that replaces the transition
labels of $\mathcal{W}$ with their instantiations according to $\mu$, i.e., if
$(s,A,s^{\prime})\in\mathcal{W}$, then
$(s,A[\mu],s^{\prime})\in\mathcal{W}_{\mu}$. We provide a proof of the lemma
in Section 0.B.2.

######  Lemma 1 ().

For every instance $\mu$,
$\mathit{traces}_{\mu}(\mathcal{M})\cup\mathit{finTraces}_{\mu}(\mathcal{M})=\mathit{traces}(\mathcal{W}_{\mu})\cup\mathit{finTraces}(\mathcal{W}_{\mu})$.

Not every infinite run of $\mathcal{M}$ corresponds to an infinite run in
$\mathcal{W}_{\mu}$ for every $\mu$. Therefore, the above lemma only holds for
the union of finite and infinite traces. However, as we work with past-time
logics, a trace satisfies a formula iff all its prefixes satisfy the formula.
Thus, $\mathcal{M}$ satisfies a pastLTL formula $\psi$ iff for every
$t\in\mathit{traces}(\mathcal{M})\cup\mathit{finTraces}(\mathcal{M})$, it
holds that $t\models\psi$. From the above lemma we therefore directly obtain
the desired correctness result for $\mathcal{M}$.

######  Theorem 5.1.

Let $\varphi=\forall p_{1},\ldots p_{m}\mathpunct{.}\psi$ be a parameterized
pastLTL formula obtained by approximating a parameterized pastTSL formula
$\rho$. If $\mathcal{W}\models\psi$, $\mathcal{W}$ satisfies Requirements 1
and 2, and can be split into $\mathcal{W}_{P_{1}},\ldots,\mathcal{W}_{P_{n}}$
such that the check for independence is successful, then
$\mathcal{M}\models\varphi$.

Since all parameters are universally quantified, it follows from the soundness
of the LTL approximation of TSL formulas [FinkbeinerKPS19] that the infinite-
state machine $\mathcal{M}$ then also satisfies the original pastTSL formula
$\rho$.

###  5.5 Extension to Existential Quantifiers

Currently, our approach cannot handle existential quantifiers. In the example
of the ERC20 contract, this forbids us to use a field funds(m) to store the
balance of all users of the contract. If we were to try, we could use an
additional parameter r for the recipient of the tokens and state the
following.

$\displaystyle\forall\texttt{m},\texttt{n},\texttt{r}\mathpunct{.}$
$\displaystyle\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\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}}}(\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}transferFrom}\texttt{(m,n,r)}\lor\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}transfer}\texttt{(m,r)}$
$\displaystyle\quad\to\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(m)}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(m)}-\texttt{arg@amount}\rrbracket$
$\displaystyle\qquad\land\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(r)}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(r)}+\texttt{arg@amount}\rrbracket)$

However, for completeness, we would have to specify that the funds field does
not spuriously increase, which would require existential quantifiers.

$\displaystyle\forall\texttt{r}\mathpunct{.}$
$\displaystyle\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\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}}}(\llbracket\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(r)}\leftarrowtail\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}funds}\texttt{(r)}+\texttt{arg@amount}\rrbracket$
$\displaystyle\quad\to\exists\texttt{m}\mathpunct{.}\exists\texttt{n}\mathpunct{.}\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}transferFrom}\texttt{(m,n,r)}\lor\texttt{\color[rgb]{0.109375,0.28515625,0.53125}\definecolor[named]{pgfstrokecolor}{rgb}{0.109375,0.28515625,0.53125}transfer}\texttt{(m,r)})$

A similar limitation stems from 1, which requires that a field parameterized
with set $P_{i}$ can only be updated by a method which is also parameterized
with $P_{i}$. As for existential quantifiers, we would otherwise not be able
to distinguish spurious updates from intended updates of fields. While it
might be challenging to extend the approach with arbitrary existential
quantification, it should be possible for future work to include existential
quantification that prevents spurious updates. One could, for example, define
some sort of “lazy synthesis”, which only does a non-self-update when
necessary.

##  6 Implementation

Figure 5: Workflow of our smart contract control flow synthesis.

We implemented our approach in a toolchain consisting of several steps. First,
we translate the pastTSL specification into a pastLTL formula using TSLtools
[tsltools], which we adapted to handle past-time operators. We then synthesize
a state machine using BDD-based symbolic synthesis. To make our lives easier,
we implemented a simple analysis to detect free choices and deadlocks, which
both indicate potential specification errors. If the specification contains
parameters, we split up the resulting state machine as described in Section 5.
Lastly, the state machines are translated to Solidity code. The toolchain is
implemented in our tool SCSynt consisting of approximately 3000 lines of
Python code (excluding TSLtools). From a user perspective, we obtain the
workflow depicted in Figure 5.

#### Synthesis from PastLTL.

The first part of our toolchain implements a symbolic synthesis algorithm for
pastLTL. As such, it can also be employed outside the context of smart
contract synthesis. We are not aware of any other tool that implements pastLTL
synthesis. We first build the safety automaton of the specification using a
representation as BDDs. For pastLTL, a symbolic approach is especially
efficient due to the long-known fact that for evaluating a pastLTL formula at
time point $i$, it is sufficient to know the value of all subformulas at point
$i-1$ [recursive_evaluation]. Afterwards, we symbolically extract the winning
region from the safety region with a classic fixpoint attractor construction.
Finally, we minimize the resulting state machine using an explicit
implementation of Hopcroft’s minimization algorithm [hopcroft1971n].

#### State Machine Analysis.

We analyze the winning region for free choices and potential deadlocks, which
both usually indicate specification errors. A free choice is a state which,
for the same input, has multiple outgoing transitions into the winning region.
If there are free choices and the developer has no preference which one is
chosen, SCSynt nondeterministically commits to one option. For the deadlock
detection, we require the user to label _determined predicate terms_. We call
a predicate determined if either 1) it becomes a constant at some time or 2)
only method calls can change its value. An example of class 1 are predicates
over the time, e.g., $\texttt{time}>\texttt{cTime()}$: if it is
$\mathit{true}$ at some point, it will never be $\mathit{false}$ again. A
class 2 example would be a predicate that counts whether the number stored in
a field has passed a fixed threshold. A predicate like
$\texttt{sender}\in\texttt{\color[rgb]{0.63671875,0.26953125,0.0859375}\definecolor[named]{pgfstrokecolor}{rgb}{0.63671875,0.26953125,0.0859375}voters}$,
on the other hand, is not determined as the evaluation changes with the input
sender. SCSynt automatically detects if, at some point, there is an evaluation
of the determined predicate terms that is allowed by the assumptions but for
which there is no valid transition. It then warns of a potential deadlock.

#### Translation to Solidity.

Finally, SCSynt translates the state machines into Solidity code. The
developer needs to provide the implementation of all predicates and functions,
as they are uninterpreted (which makes the synthesis feasible after all). Some
of the most common functions and predicates (equality, addition, etc) are
automatically replaced by SCSynt. The signatures of all methods, functions,
predicates, constants, fields, and parameters need to be provided as well. As
an example, we attach the signatures of the parameterized voting contract from
Section 4.1 in Section 0.D.1. For each method of the contract, we create a
function that contains the state machine logic for that particular method. For
parameterized specifications, the contract is augmented with a mapping
recording the knowledge of states (c.f. Section 5.3). The parameters of a
method are included as arguments or, according to the signature, replaced with
a fixed interpretation (e.g, if m is always msg.sender). Following
[DBLP:conf/fc/MavridouL18], we also add automatic protection against
reentrancy attacks by setting a Boolean flag if a method is currently
executing. For the interested reader, we provide the Solidity code for the
method vote from Section 3.1 in Section 0.D.2. In Section 0.D.3, there is also
a general schema of our translation.

##  7 Evaluation

To evaluate SCSynt, we specified and synthesized ten different smart
contracts. We report on the running time of the synthesis procedure itself and
the translation to Solidity code. We also compare our automatically generated
Solidity code to handwritten reference implementations in terms of size and
average gas consumption. Since the reference contracts do not provide any
formal guarantees, we also conduct a comparison of different versions of the
same contract, each automatically generated by tools that provide some form of
formal guarantees.

#### Running Time.

We synthesized typical smart contracts with a non-trivial temporal control
flow. Of the ten specifications, four use specifications with parameters. A
detailed description of all benchmarks is provided in Section 0.E.1. We
analyzed all contracts in terms of the size of the specification and of the
synthesized state machine. All experiments were run on a 2020 Macbook with an
Apple M1 chip, 16GB RAM, running MacOS. The results are shown in Table 1.

Table 1: Sizes of the specifications and state machines as well as the average running time of SCSynt. #Conj. is the number of conjuncts, #Nodes is the number of nodes of the AST. If the spec has parameters, the state machine size is the sum of the states/transitions of the split state machines. The synthesis and translation times are the respective average on 10 runs of the same benchmark. | Specification | State Machine | Avg. Time (s)
---|---|---|---
Contract |  #Conj. |  #Nodes |  #States |  #Trans. |  Synth. |  Transl.
Asset Transfer |  36 |  216 |  8 |  14 |  5.9996 |  0.0053
Blinded Auction |  19 |  218 |  5 |  8 |  1.5446 |  0.0026
Coin Toss |  27 |  154 |  5 |  7 |  1.6180 |  0.0029
Crowd Funding |  17 |  100 |  4 |  8 |  0.2178 |  0.0026
ERC20 |  15 |  140 |  9 |  5 |  0.4812 |  0.0033
ERC20 Extended |  19 |  244 |  10 |  7 |  1.9608 |  0.0040
NFT Auction |  30 |  325 |  12 |  15 |  12.1853 |  0.0080
Simple Auction |  15 |  83 |  4 |  7 |  0.1362 |  0.0026
Ticket System |  13 |  97 |  4 |  6 |  0.1812 |  0.0028
Voting |  17 |  98 |  6 |  5 |  0.1478 |  0.0023

The evaluation shows that our toolchain is efficient: the translation of the
state machine into Solidity code is nearly instantaneous. For most contracts,
SCSynt synthesizes a state machine in less than two seconds. To show that the
approach scales to larger, real-life contracts, we included the NFT auction, a
parameterized specification for a contract actively maintained by Avolabs. Its
reference implementation has over 1400 lines of code. We specified the
contract according to the README provided on the GitHub of Avolabs
[NFTReference].

#### Comparison to Handwritten Contracts.

We compare the Solidity code generated by SCSynt to handwritten
implementations for the same contracts found in the literature but without
formal guarantees. For a fair comparison, we extend our code with the
implementation of the contract beyond the specified temporal control flow. A
detailed table with the results is given in Section 0.E.2. Overall, the
automatically generated code has an overhead of 62% in terms of code length
(including automatic reentrancy protection). An exception is the NFT auction,
where SCSynt’s code is 35% shorter. This is mostly due to code duplication at
various locations in the handwritten contract which is needed to structure the
code and make it readable. This is not necessary if the code is correct by
construction. It seems that SCSynt has an advantage in terms of code length
for more complicated and thus generally longer smart contracts.

We measured the gas consumption using the Truffle Suite [truffle]. Our
synthesized code consumes 40% more gas than the handwritten, non-verified
code. Without SCSynt’s automatic prevention of reentrancy attacks, there is
only a 25% overhead. We see that the average gas overhead is 50.6% for
parameterized specification as compared to 34.5% for non-parameterized
contracts. This is because the implementation of the hierarchical systems and
the sharing of knowledge needs some machinery like additional enums and
mappings.

#### Comparison to Other Approaches with Formal Guarantees.

It is to be expected that automatically generated code is not as efficient as
handwritten one. We therefore evaluate our code with respect to two comparable
formal approaches that also automatically generate Solidity code. The first
approach synthesizes a state machine from LTL specifications and translates
the result to Solidity code [DBLP:journals/corr/abs-1906-02906]. The approach
does not include any reasoning about the data flow in the fields or the
arguments of a method. The second approach, the VeriSolid framework
[DBLP:conf/fc/MavridouL18, MavridouLSD19], generates Solidity code from a
handwritten state machine.

The only benchmark available for all three approaches is the blinded auction
contract. We make sure that the code is comparable by 1) adding a missing
guard on the time requirements to [DBLP:journals/corr/abs-1906-02906]’ code,
which was present in the specification but not in the Solidity code, 2)
removing additional requirements that make sure only the owner can call
certain methods from SCSynt’s code and 3) removing reentrancy protection in
SCSynt’s and VeriSolid’s code.

The generated contract of the LTL synthesis approach is 42% longer than
SCSynt’s implementation and consumes 17% more gas. VeriSolid duplicates a
method if it can be invoked in several states. Therefore, their code is
slightly longer than ours (14%) and consumes 4% more gas. Their reentrancy
protection is more efficient though: when enabled, SCSynt’s code is 12% longer
and consumes 5% more gas. This is a possibility for future optimizations in
SCSynt.

##  8 Conclusion

We have described the synthesis of Solidity code from specifications given in
pastTSL equipped with universally quantified parameters. Our approach is the
first one that facilitates a comprehensive specification of the implicit state
machine of a smart contract, including the data flow of the contract’s fields
and guards on the method’s arguments. While we have shown that pastTSL
realizability without parameters is undecidable in general, solutions can be
obtained via a sound reduction to LTL. For parameterized specifications, we
have developed a representation of the described infinite-state system that
enables a Solidity implementation with a moderate overhead in the gas
consumption. Our tool SCSynt implements the synthesis toolchain, including an
analysis of the state machine regarding potential specification errors.

For future work, we aim to extend our approach to specifications given in
pastTSL with alternating parameter quantifiers. There are also several
exciting possibilities to combine our work with other synthesis and
verification techniques. One avenue is to automatically prove necessary
assumptions in deductive verification tools [dharanikota2021celestial],
especially for assumptions that state invariants maintained by method calls
(e.g., “calling close does not increase the number of votes”). Another
possibility is to synthesize function and predicate implementations in the
spirit of [cispa3674]. Finally, we would like to generalize our work to a
broader class of programs. We have developed this approach specifically for
smart contracts but parameterized TSL, past-time synthesis, and our splitting
technique should be applicable to other use cases as well.

## References

  * [1] Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A.W.: Specification is law: Safe creation and upgrade of ethereum smart contracts. CoRR abs/2205.07529 (2022). https://doi.org/10.48550/arXiv.2205.07529, https://doi.org/10.48550/arXiv.2205.07529
  * [2] Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986). https://doi.org/10.1016/0020-0190(86)90071-2, https://doi.org/10.1016/0020-0190(86)90071-2
  * [3] Avolabs: NFT auction reference contract. https://github.com/avolabs-io/nft-auction (2022), accessed: 2022-07-05
  * [4] Azure: Asset transfer sample from the azure blockchain workbench. https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/asset-transfer (2021), accessed: 2022-07-05
  * [5] Azure: Asset transfer reference contract. https://github.com/Azure-Samples/blockchain/blob/master/blockchain-workbench/application-and-smart-contract-samples/asset-transfer/ethereum/AssetTransfer.sol (2022), accessed: 2022-07-05
  * [6] Bansal, S., Vardi, M.Y.: Safety and co-safety comparator automata for discounted-sum inclusion. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 60–78. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_4, https://doi.org/10.1007/978-3-030-25540-4_4
  * [7] Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (June 2022), https://publications.cispa.saarland/3674/
  * [8] Ciccio, C.D., Cecconi, A., Dumas, M., García-Bañuelos, L., López-Pintado, O., Lu, Q., Mendling, J., Ponomarev, A., Tran, A.B., Weber, I.: Blockchain support for collaborative business processes. Inform. Spektrum 42(3), 182–190 (2019). https://doi.org/10.1007/s00287-019-01178-x, https://doi.org/10.1007/s00287-019-01178-x
  * [9] Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3312, pp. 245–259. Springer (2004). https://doi.org/10.1007/978-3-540-30494-4_18, https://doi.org/10.1007/978-3-540-30494-4_18
  * [10] Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., Lal, A.: Celestial: A smart contracts verification framework. In: Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design (FMCAD 2021). pp. 133–142 (2021)
  * [11] Ehlers, R., Finkbeiner, B.: Reactive safety. In: D’Agostino, G., Torre, S.L. (eds.) Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2011, Minori, Italy, 15-17th June 2011\. EPTCS, vol. 54, pp. 178–191 (2011). https://doi.org/10.4204/EPTCS.54.13, https://doi.org/10.4204/EPTCS.54.13
  * [12] Ethereum: Introduction to ethereum. https://ethereum.org/en/developers/docs/intro-to-ethereum/ (2021), accessed: 2022-07-05
  * [13] Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. In: Bouyer, P., Schröder, L. (eds.) 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. Lecture Notes in Computer Science, vol. 13242, pp. 325–346. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_17, https://doi.org/10.1007/978-3-030-99253-8_17
  * [14] Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Synthesizing functional reactive programs. In: Eisenberg, R.A. (ed.) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019. pp. 162–175. ACM (2019). https://doi.org/10.1145/3331545.3342601, https://doi.org/10.1145/3331545.3342601
  * [15] Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal Stream Logic: Synthesis Beyond the Bools. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 609–629. Springer (2019). https://doi.org/10.1007/978-3-030-25540-4_35
  * [16] Fourswords: Simple auction reference contract. https://fourswords.io/docs/smartcontracts/solidity-guide/solidity-examples/ (2022), accessed: 2022-07-05
  * [17] Fourswords: Voting reference contract. https://fourswords.io/docs/smartcontracts/solidity-guide/solidity-examples/ (2022), accessed: 2022-07-05
  * [18] Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Syntroids: Synthesizing a game for fpgas using temporal logic specifications. CoRR abs/2101.07232 (2021), https://arxiv.org/abs/2101.07232
  * [19] Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2280, pp. 342–356. Springer (2002). https://doi.org/10.1007/3-540-46002-0_24, https://doi.org/10.1007/3-540-46002-0_24
  * [20] Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Katoen, J., Stevens, P. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2280, pp. 342–356. Springer (2002). https://doi.org/10.1007/3-540-46002-0_24, https://doi.org/10.1007/3-540-46002-0_24
  * [21] Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of machines and computations, pp. 189–196. Elsevier (1971)
  * [22] Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10(1) (2014). https://doi.org/10.2168/LMCS-10(1:12)2014, https://doi.org/10.2168/LMCS-10(1:12)2014