of 67
Formalizing synthesis in TLA
+
Ioannis Filippidis and Richard M. Murray
Control and Dynamical Systems
California Institute of Technology
f
ifilippi,murray
g
@caltech.edu
December 23, 2016
Abstract
This report proposes a TLA
+
de nition for the problem of constructing
a strategy that implements a temporal property. It is based on a note by
Lamport [1] that outlines a formalization of realizability in TLA. The
modi ed de nition proposed here is expressed axiomatically in TLA
+
.
Specifying what function is acceptable as a strategy requires care, so that
a function with empty domain be avoided, while ensuring that the strategy
will not need to have a domain too large to be a set.
We prove that initial conditions should appear in assumptions only,
unless an initial predicate is added to the de nition of a realization. We
show that a speci cation should include an assumption about a set of
initial values to ensure that realizability does not become unprovable. We
discuss what form of open-system properties expressed with the \while-
plus" operator
+
▷
are realizable.
We formalize the notions of interleaving and disjoint-state behaviors,
based on de nitions given by Lamport and Abadi, and consider the no-
tion of interleaving for an open-system property. We give examples of
expressing different forms of games in TLA
+
using the proposed de ni-
tion, including games with partial information.
Contents
1 Motivation
3
2 Functions as strategies
3
3 Speci cations that functions can implement
4
3.1 Initial conditions . . . . . . . . . . . . . . . . . . . . . . . . . . .
4
3.2 From where should a strategy matter? . . . . . . . . . . . . . . .
6
3.2.1 Interpretation vs model . . . . . . . . . . . . . . . . . . .
7
3.2.2 Recursively structured interpretation . . . . . . . . . . . .
8
1
3.2.3 TLA
+
function axioms . . . . . . . . . . . . . . . . . . . .
11
3.2.4 When realizability is unprovable . . . . . . . . . . . . . .
11
3.3 Placing initial conditions . . . . . . . . . . . . . . . . . . . . . . .
14
4 De ning realizability and synthesis
17
4.1 Sharing variables . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
4.2 Realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
17
4.3 Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
21
5 Who changed each variable
22
5.1 Behaviors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22
5.1.1 Interleaving . . . . . . . . . . . . . . . . . . . . . . . . . .
22
5.1.2 Shared or disjoint state . . . . . . . . . . . . . . . . . . .
23
5.1.3 Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . .
24
5.2 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
25
5.2.1 Interleaving . . . . . . . . . . . . . . . . . . . . . . . . . .
25
5.2.2 Shared or disjoint state . . . . . . . . . . . . . . . . . . .
25
5.2.3 Open-system speci cations . . . . . . . . . . . . . . . . .
25
5.2.4 Stepwise type precondition needed inside G . . . . . . . .
26
5.3 Synchronous games with full information . . . . . . . . . . . . . .
27
6 Discussion
28
6.1 Specifying a type invariant is not restrictive . . . . . . . . . . . .
28
6.2 Variants for de ning realizability . . . . . . . . . . . . . . . . . .
29
6.3 Interpretations and models . . . . . . . . . . . . . . . . . . . . .
30
7 Conclusion
31
A Proofs
32
B Auxiliary results
56
C Lamport's de nition of realizability
65
2
1 Motivation
A TLA
+
formula
φ
describes some behaviors
1
. Constructing an implementation
is a separate concern. In TLA
+
, implementation is implication between two
properties
)
φ
. Synthesis is the construction of an implementation
that
we can run on a computer. A computer only knows how to execute some concrete
steps, so the synthesized property
should be expressed in terms of these steps.
In order to de ne synthesis, we must describe what our computer can do, for
example what variables it can change. A speci cation for the synthesis problem
describes precisely what it means to control a variable. Formalizing the notion
of variable controllability was one motivation for what follows.
Another reason was the observation that, in the literature on games, a strat-
egy is sometimes allowed to be a
partial
function. The intention is that a smaller
domain may suffice to de ne a winning strategy. However, such a de nition can
leave unspeci ed what happens outside the strategy's domain
2
. If plays outside
the strategy's domain are declared as impossible due to typeness considerations,
then a function with empty domain would qualify as a winning strategy
3
. The
de nition of synthesis formalized below in TLA
+
aims to avoid such ambiguity,
a symptom of using a typed logic [5, 6, 7].
2 Functions as strategies
We want to de ne the solution of a game in TLA
+
. Several other de nitions of
this problem exist in the literature. Based on the de nition outlined in [1], we
give a TLA
+
de nition that is general enough to serve for more than one kind
of game, including games of partial information.
We have to choose what quali es as a strategy. Is an operator a strategy?
A strategy reads the current state and writes (part of) the next state. So, a
strategy operator must take arguments. To express realizability, we will want
to quantify over system strategies. TLA
+
is a rst-order logic, so we cannot
quantify over unary operators [8, p.318], [5, p.508]. In order to quantify over
strategies, a strategy should be a set. We want to use a strategy as a mapping.
There are several alternative ways for de ning sets that can serve the purpose
of mappings [6, p.4]. We prefer to let a strategy be a function
f
, similarly to
[1, 9, 10]. This requirement can be expressed axiomatically in TLA
+
with the
predicate
IsAFunction
(
f
)
∆
=
f
= [
x
2
domain
f
7!
f
[
x
]]
[8, p.303]. This is convenient, because it does not mention a set of candidate
strategies, and leads to a simpler de nition of synthesis below. This predicate
1
Any formula describes a collection of behaviors too large to be a set (a proper class).
2
A partial function
f
can lead the game outside its domain, arti cially terminating it.
3
Non-axiomatic de nitions of synthesis that avoid this have been given using partial func-
tions [2, p.46], [3, p.367], [4, p.915]. They are informal, and more complex, because trivial
solutions need to be expressly excluded.
3
can be written equivalently as
IsAFunction
(
f
) =
9
S
:
^
S
=
domain
f
^
f
= [
x
2
S
7!
f
[
x
]]
:
We are about to
construct
a function
f
suitable for our purpose, and so choose
domain
f
. This choice raises the question of what speci cations admit a func-
tion as strategy.
3 Speci cations that functions can implement
3.1 Initial conditions
Somewhat simpli ed, function
f
reads the variables
x
;
h
and controls the next
value of
x
,
De nition 1 (Simple realization)
Let
(
x
;
h
;
f
)
∆
=
2
[
x
′
=
f
[
⟨
x
;
h
⟩
] ]
⟨
x
;
h
⟩
:
The objective of this control law is to implement the property
φ
(
x
;
h
) that
mentions only the variables
x
and
h
, and does not mention the constant
f
.
Proving that
f
implements the property
φ
(
x
;
h
) (roughly) means proving that
j
=
(
x
;
h
;
f
)
)
φ
(
x
;
h
)
:
Above, we decided that a strategy should be a function
f
, so we want
j
=
^
IsAFunction
(
f
)
^
(
x
;
h
;
f
)
)
φ
(
x
;
h
)
:
Any property
φ
implies an initial (state) predicate
Init
(
x
;
h
), even if it is trivial
(
true
). We will show that for
to implement
φ
:
1.
should contain a (non-trivial) initial predicate, or
2.
no initial state should violate
φ
.
For any initial value
u
of
x
, we will construct a behavior that satis es
but
violates
φ
. The proofs are in Appendix A. The proof style is described in [11].
The operator
999
999
expresses temporal existential quanti cation [8,
x
8.8, p.109].
Proposition 2
Assume
:
1.
constants
u
;
f (rigid variables)
2.
variable
h ( exible variable)
Prove
:
999
999
x
:
^
x
=
u
^
2
[
x
′
=
f
[
⟨
x
;
h
⟩
]]
⟨
x
;
h
⟩
4
In words, for any behavior
4
there exists some stutter-equivalent
x
-variant be-
havior that satis es (
x
=
u
)
^
2
[
x
′
=
f
[
⟨
x
;
h
⟩
]]
⟨
x
;
h
⟩
:
The proof is written at
the meta-level, in Zermelo-Fraenkel (ZF) set theory [12]. For this reason, we
translate the statement to ZF, using de nitions from [8, p.316], and
(1)
8
behavior

:
F
∆
=
: 9
behavior

:
:
F
=
8

:
IsABehavior
(

)
)
F
Proposition 3
Assume
:
1.
constants
u
;
f
2.
variables
h
;
x
Prove
:
8
behavior

:
9
behavior

:
^


x

^

j
=
^
x
=
u
^
2
[
x
′
=
f
[
⟨
x
;
h
⟩
]]
⟨
x
;
h
⟩
Proof
: on page 34.
[Proposition 3]
Proof sketch
: Given any behavior

and TLA
+
constant
u
,
pick a behavior

with
5

[
n
2
Nat
]
≜
if
n
= 0
then
[

[0]
except
!
J
x
K
=

[0]
J
u
K
]
else
[

[
n
]
except
!
J
x
K
=

[
n
1]
J
f
[
⟨
x
;
h
⟩
]
K
]
By construction, all steps
6
of

satisfy the action
x
′
=
f
[
⟨
x
;
h
⟩
], and initially
x
=
u
. This construction is possible because
f
and
⟨
x
;
h
⟩
are sets, and TLA
+
an
untyped logic, so the expression
f
[
⟨
x
;
h
⟩
] is syntactically well-formed [8, p.71].
In an untyped logic, every syntactically well-formed expression is interpreted as
some set [8, p.67]. So, the expression
f
[
⟨
x
;
h
⟩
] has some set as meaning.
Next, we show that if some initial states violate
φ
then no function
f
can
implement
φ
with
.
Lemma 4
Assume
:
1.
state
Init
(
x
;
h
)
2.
temporal
φ
(
x
;
h
)
3.
No variable symbols other than x
;
h occur in
φ
(
x
;
h
)
4.
as de ned in De nition 1
5.
φ
(
x
;
h
)
)
Init
(
x
;
h
)
6.
9
u
;
r
:
Init
(
u
;
r
)

false
Prove
:
8
f
:
999
999
x
;
h
:
(
x
;
h
;
f
)
^ :
φ
(
x
;
h
)
.
4
In Proposition 2, the proof goal is equivalent to its universal closure [13, p.5].
5
Using TLA
+
notation also for ZF, ! refers to the function being de ned. The variable
interpretation
state
J
u
K
is de ned in [8, p.311].
6
A
step
of a behavior is de ned in [8, p.16].
5
Realization
(
x;h;f
)
φ
(
x;h
)
Init
(
x;h
)
initial states that
violate
φ
any state
can be initial
from any initial state
there exists some behavior
that satis es

⟨
x;h
⟩
=
⟨
u;r
⟩
Figure 1: If some initial state violates
φ
, and no initial predicate
I
is included
in the realization
, then
φ
is unrealizable.
Proof
: on page 36.
[Lemma 4]
Proof sketch
: We can pick initial values
u
;
r
such that
(
⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
)
)
(
Init
(
x
;
h
)

false
)
By contrapositive of
assumption
5
:
Init
(
x
;
h
)
) :
φ
(
x
;
h
)
So
(2)
(
⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
)
) :
φ
(
x
;
h
)
By Proposition 2, which holds
888
888
h
(universal closure)
(3)
999
999
x
;
h
:
^ ⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
^
(
x
;
h
;
f
)
By Eqs. (2) and (3), for any
f
999
999
x
;
h
:
^
(
x
;
h
;
f
)
^ ⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
)
999
999
x
;
h
:
(
x
;
h
;
f
)
^ :
φ
(
x
;
h
)
:
3.2 From where should a strategy matter?
Suppose that behaviors that assign arbitrary values to
x
;
h
can violate the prop-
erty
φ
(
x
;
h
). No function
f
in the property
(
x
;
h
;
f
) can provably implement
6
φ
(
x
;
h
) in this case, because
domain
f
must be a set. This suggests that
φ
should include an assumption of the form
⟨
x
;
h
⟩ 2
S
about the initial condi-
tion. We will prove that otherwise realizability can be impossible to prove. The
proof relies on the freedom that exists in how function application,
f
[
x
], is inter-
preted when
x
=
2
domain
f
. TLA
+
is untyped, so
f
[
x
] is some set. The axioms
of TLA
+
leave unspeci ed what set
f
[
x
] is for
x
=
2
domain
f
.
3.2.1 Interpretation vs model
An interpretation is a way to assign meaning to expressions of a language. One
way to assign meaning is to take an expression in the object language (here
TLA
+
), and map it to an expression in the metalanguage (here ZF) [8, p.292].
A model is an interpretation in which all the theorems of a formal theory are
interpreted as statements that are theorems of the metatheory.
We base our de nition of interpretation for rst-order TLA
+
on the liter-
ature. Vanzetto de nes a translation of TLA
+
to input for SMT solvers [14].
Merz formalizes TLA
+
in the Isabelle theorem prover [15], for TLAPS (the TLA
proof system), including functions [16]. Models of rst-order TLA

are de ned
in [17, pp.80{86]. Lamport refers to Leisenring's study [18] of the operator
choose
. Leisenring de nes models for ZF
"
7
[18, p.18], but not for modal logic.
A semantics for TLA
+
can be given by pairing a model as de ned by Leisenring
with a behavior

, similarly to [14, 17, 19, 20]. Following Lamport, we use
TLA
+
syntax for ZF itself [8, p.292], including function syntax. For example,
the de nition of behaviors as functions with domain
Nat
[8, p.315].
By interpretation of TLA
+
in ZF we mean an operator
I
(
;
) and a set

such that

IsABehavior
(

), and

the mapping
I
(
;
) de nes the meaning
I
(
e
;
s
) of each basic state function
e
in each state
s
. Let
8
s
J
e
K
I
∆
=
I
(
e
;
s
)
Constant expressions have the same meaning in each state, so we can omit
s
and write
J
e
K
I
.
The role of a behavior

is to map each index
n
2
Nat
and variables
9
to values
in each index
n
2
Nat
. We will denote that a temporal formula
F
is interpreted
as true in the metatheory as [17]
I
;
j
=
F
7
ZF abbreviates Zermelo-Fraenkel set theory. ZF
"
denotes ZF extended with the operator
choose
. The operator
choose
is Hilbert's
"
operator [18], [21, p.9]. We use ZF
"
, so we omit
"
and write ZF.
7
A
basic state function
is a particular form of TLA
+
expression. The TLA
+
syntax de nes
countably many expressions. The
meaning
of a basic state function is a mapping from
all
states, so an operator, but not a function [8, p.311].
8
The expression
s
J
e
K
I
extends the notation
s
J
e
K
of [8, p.311]. A similar notation is
s
J
x
K
I
;
in [17, p.81].
7
The assignment of values to constants (rigid variables) is speci ed by
I
. We
could de ne a separate operator
Const
I
, but we will use
I
for that purpose too,
in the recursive interpretation de ned later. The other observation is that we
will writte
Flatten
(
:::;
I
) and recurse to
ApplyFunc
I
when
I
is given to the
operator
Flatten
, and to
ApplyFunc
R
when
R
is given to
Flatten
.
A
model
of TLA
+
is an interpretation in which each theorem is interpreted as
a statement provable in the metatheory. We use an operator
IsAModel
(
I
(
;
)
;
)
to signify this, by writing the predicate
IsAModel
(
I
;
).
3.2.2 Recursively structured interpretation
Structured interpretations
In the proofs, we assume for some interpre-
tation
I
A
;
that
IsAModel
(
I
A
;
), and modify the rst-order interpretation
operator
I
A
to
I
B
so that both:
1.
the resulting interpretation
I
B
;
has some desired properties
10
, and
2.
IsAModel
(
I
B
;
).
It can be difficult to de ne
I
B
in terms of
I
A
so as to achieve both of these
goals. An example of what can go wrong is given in Section 6.3. The difficulty
lies in that
I
A
takes entire TLA
+
expressions as arguments. We have to change
not only the interpretation of those symbols that we are primarily interested
in, but also all other expressions that contain those symbols, to ensure that all
axioms and proof rules are true in
I
B
too.
The standard way of de ning a rst-order interpretation
I
is inductively [8,
Ch.16]. This is the case in the literature cited earlier. TLA
+
is a modal logic, so
the interpretation
I
;
of a temporal formula is de ned in terms of actions over
steps [8, p.315], of actions in terms of state predicates over states [8, p.313], and
of constant expressions [8, pp.311]. The interpretation
I
is de ned inductively
using the operators:

Tokenize
(
e
) for a TLA
+
expression
e
is a tuple of strings (tokens).

Flatten
(
seq
;
s
;
I
(
;
)) takes a sequence of tokens and interprets it in ZF.

ApplyFunc
I
(
u
;
v
), an operator that takes the interpretation
u
of an ex-
pression
e
1
, the interpretation
v
of another expression
e
2
, and gives the
interpretation of the expression \
e
1
[
e
2
]".

MakeFunction
(
S
) for a set
S
of 2-tuples returns a function.

DomainOf
(
a
) interprets function domain syntax.
9
There are variables and constants in TLA
+
. Sometimes, constants are called \rigid vari-
ables" [8, p.110], and the variables \ exible variables". A behavior

assigns values only to
exible variables. The values of constants are de ned by the rst-order interpretation
I
.
10
Modifying one model to obtain another is a method widely used for proving relative
consistency results. The method of forcing [22] is one approach for constructing new models.
We do not use forcing, because we modify the interpretation of functions without changing
the domain of discourse.
8
We describe these operators using a combination of de nitions and examples
Tokenize
(
str
)
∆
=
choose
seq
2
Seq
(
string
) :
^
seq
2
TLAPlusGrammar
:
Module
^
str
=
Concatenate
(
seq
)
with
Concatenate
de ned as we usually understand it,
Seq
from the standard
Sequences
module [8, Fig.18.1, p.341], and
TLAPlusGrammar
[8, p.278]
11
.
Rigid quanti cation is de ned in [8, pp.88, 109] as

j
= (
8
r
:
F
)
∆
=
8
r
: (

j
=
F
)
The modi cation of constant symbols in the rst-order interpretation is not
mentioned, and the same symbol
r
occurs in object language (TLA
+
) as in
the metalanguage (ZF). We need to keep track of these details, so we base our
de nition on
12
[14, p.31]
(4)
I
;
j
=
8
r
:
φ
∆
=
8
u
:
let
I
j
r
≜
u
(
seq
;
s
)
∆
=
if
seq
=
⟨
\
r
"
⟩
then
u
else
I
(
seq
;
s
)
in
I
j
r
≜
u
;
j
=
φ:
Function constructors are interpreted as
Flatten
(
Tokenize
(\[
x
2
e
1
7!
e
2
]")
;
s
;
I
) =
MakeFunction
(
f
⟨
r
;
Flatten
(
Tokenize
(\
e
2
")
;
s
;
I
j
x
≜
r
)
⟩
:
r
2
Flatten
(
Tokenize
(\
e
1
")
;
s
;
I
)
g
)
So, a function is determined by the values of
e
2
for
x
ranging over values in
e
1
,
but not outside. Function domain syntax is interpreted as
Flatten
(
Tokenize
(\
domain
e
")
;
s
;
I
) =
DomainOf
(
Flatten
(
Tokenize
(\
e
")
;
s
;
I
))
Function application is interpreted as
Flatten
(
Tokenize
(\
e
1
[
e
2
]")
;
s
;
I
) =
ApplyFunc
I
(
Flatten
(
Tokenize
(\
e
1
")
;
s
;
I
)
;
Flatten
(
Tokenize
(\
e
2
")
;
s
;
I
)
)
:
11
If no such
seq
exists, then
Tokenize
(
str
) is some unknown value, but we don't care,
because this happens only when, by de nition of
TLAPlusGrammar
,
str
is
not
a syntactically
correct TLA
+
module. Strictly speaking, not all syntactically acceptable module strings have
meaning [8, Chapters 16, 17], but we can ignore those cases, because the result for those
strings is irrelevant to our study of TLA
+
.
12
In particular, the de nition of
truth
M
(
8
x
:
φ
) there. There is a typo in the subscript,
where
I
and
v

(
x
7!
d
) need to be swapped.
9
With the de nition sketched above, we can reduce the meaning of any TLA
+
formula to the meaning of variables and constants [8, p.310] in ZF.
The tokenizer in action
The operator
Tokenize
takes a string
str
(a nite
sequence of characters), and chooses
seq
, a sequence of strings (each of them a
token) that belongs to the TLA
+
grammar, so that concatenating the strings
in
seq
yields
str
. For example,
Tokenize
(\
p
2
q
") =
⟨
\
p
"
;
\
2
"
;
\
q
"
⟩
:
The string \
p
2
q
" has been split into the sequence
⟨
\
p
"
;
\
2
"
;
\
q
"
⟩
, where
each of \
p
"
;
\
2
"
;
\
q
" is a string. This agrees with our perception of what a
tokenizer program is doing.
The operator
Flatten
interprets the tokenizer's result in state
s
as follows
Flatten
(
Tokenize
(\
p
2
q
"
;
s
;
I
) =
Flatten
(
⟨
\
p
"
;
\
2
"
;
\
q
"
⟩
;
s
;
I
)
=
Flatten
(
⟨
\
p
"
⟩
;
s
;
I
)
2
Flatten
(
⟨
\
q
"
⟩
;
s
;
I
)
Is there such an interpretation?
We outlined an inductive de nition of
interpretation. The operator
Flatten
can be de ned in more detail as in [14]. We
are not going to give an exhaustive de nition, neither prove relative consistency
of TLA
+
with respect to ZF. The parser and translator code in TLAPS and
TLC
13
is evidence that it is possible to de ne these operators.
By Godel's second incompleteness theorem, if TLA
+
is consistent, then
TLA
+
cannot prove it is consistent. By Godel's completeness theorem, if TLA
+
is consistent, then it has a model with a set as domain of discourse [23, Sec.5.2].
We are going to assume that a relative interpretation [24, Def. I.16.11, p.99]
of TLA
+
in ZF is available, and modify it to obtain another relative interpre-
tation that satis es a desired property. Assuming that the starting relative
interpretation proves relative consistency [24, Cor. I.16.14, p.101], relative con-
sistency follows for the second interpretation. We need to refer to behaviors, so
we cannot work directly within TLA
+
to prove relative consistency by interpret-
ing the second TLA
+
theory in terms of the starting one. Instead, our proof
could be viewed as a relative interpretation of the ZF underlying the second
TLA
+
theory within the ZF underlying the starting TLA
+
theory.
Note that relative interpretation via relativization relies on class-sized mod-
els, and care is then required that the interpretation be de ned in the metathe-
ory, due to Tarski's theorem on the unde nability of truth [24, p.84].
Another way to view the proofs is in terms of set-sized models. Assuming
that a model with set as domain of discourse exists, we construct another model
with the same domain, but different interpretation for functions. The assump-
tion that a set-sized model exists is equivalent to assuming that ZF is consistent
[23, Sec.5.2].
13
TLC is a model checker for TLA
+
.
10
3.2.3 TLA
+
function axioms
We summarize the de nitions and axiom schemata of TLA
+
that describe func-
tions. The symbol
e
stands for any TLA
+
expression.
IsAFunction
(
f
)
∆
=
f
= [
x
2
domain
f
7!
f
[
x
]]
8
f
;
g
: (
^
IsAFunction
(
f
)
^
IsAFunction
(
g
) )
)
(
f
=
g
)
 ^
domain
f
=
domain
g
^ 8
x
2
domain
f
:
f
[
x
] =
g
[
x
]
(
domain
[
x
2
S
7!
e
]) =
S
8
y
2
S
: [
x
2
S
7!
e
][
y
] =
let
x
∆
=
y
in
e
IsAFunction
([
x
2
S
7!
e
])
8
f
: (
f
2
[
S
!
T
])
 ^
IsAFunction
(
f
)
^
S
=
domain
f
^ 8
x
2
S
:
f
[
x
]
2
T
[
f
except
![
d
] =
e
]
∆
= [
y
2
domain
f
7!
if
y
=
d
then
let
@
∆
=
f
[
d
]
in
e
else
f
[
y
]]
This summary is given only for convenience. For details, consult [8, 25, 16].
It should be emphasized that TLA
+
functions are interpreted \shallowly" by
the operators
ApplyFunction
and
MakeFunction
. These de ne TLA
+
functions
separately from ZF functions. We could have followed a \deeper" approach, but
it would have only made the proofs less readable.
3.2.4 When realizability is unprovable
Modifying the value of constant symbols does not affect the truthness of axioms
and proof rules in a model of TLA
+
that is an interpretation with the recur-
sive structure outlined above. Care is needed when modifying the operator
ApplyFunc
to ensure that function axioms be preserved. We use the following
claim, whose proof is sketched, but omitted.
Proposition 5 (Independence from function application outside domain)
Assume
:
1.
IsAModel
(
J
;
)
2.
J has the recursive structure outlined above.
3.
R is an interpretation obtained from J by replacing the operator
ApplyFunc
J
with an operator ApplyFunc
R
4.
8
u
;
v
:
_
v
=
2
DomainOf
(
u
)
_
ApplyFunc
R
(
u
;
v
) =
ApplyFunc
J
(
u
;
v
)
Prove
:
IsAModel
(
R
;
)
11
Proof sketch
: on page 36.
Another way to describe the above change is based on how TLAPS translates
TLA
+
to SMT, which can be written as
ApplyFunc
(
u
;
v
) =
if
v
2
DomainOf
(
u
)
then
a
(
u
;
v
)
else
!
(
u
;
v
)
;
where the operator
!
remains uninterpreted [14, Eq.(4.12),
x
4.4.2, p.78]. What
we do amounts to modifying only
!
.
Lemma 6 (Unprovability of realizability)
Assume
:
1.
TLA
+
is sound.
2.
zf new
J
(
;
)
;
3.
J
;
is an interpretation with the recursive structure described ear-
lier.
4.
IsAModel
(
J
;
)
5.
temporal
φ
(
x
;
h
)
6.
The symbols f
;
m do not occur in the expression
φ
(
x
;
h
)
.
7.
No
14
function syntax occurs in the expression
φ
(
x
;
h
)
(function
application, constructors, and related constructs).
8.
(
x
;
h
;
f
)
∆
=
999
999
m
:
2
[
x
′
=
f
[
⟨
x
;
h
;
m
⟩
]
⟨
x
;
h
;
m
⟩
9.
CanLoseOutside
∆
=
8
S
:
999
999
x
;
h
:
^ :
φ
(
x
;
h
)
^
2
(
⟨
x
;
h
⟩
=
2
S
)
10.
j
=
CanLoseOutside
11.
G
∆
=
9
f
:
^
IsAFunction
(
f
)
^
888
888
x
;
h
:
(
x
;
h
;
f
)
)
φ
(
x
;
h
)
:
Prove
:
⊬
G
Proof
: on page 37.
In words, prove that (arbitrary
14
memory) realizability of
φ
cannot be proved,
unless, for any behavior that violates
φ
, eventually
⟨
x
;
h
⟩ 2
S
.
In other words, outside its domain,
f
plays arbitrarily. The behavior sat-
is es
, but may violate
φ
, and we cannot prove that it doesn't. We have
shown that
f
should matter only for behaviors that eventually enter some set
S
,
3
(
⟨
x
;
h
⟩ 2
S
). It follows that any provably realizable speci cation
φ
should
satisfy
:
(
8
S
:
999
999
x
;
h
:
:
φ
(
x
;
h
)
^
2
(
⟨
x
;
h
⟩
=
2
S
)

9
S
:
888
888
x
;
h
:
2
(
⟨
x
;
h
⟩
=
2
S
)
)
φ
(
x
;
h
)
The above case is one alternative. The other alternative is
:
2
(
⟨
x
;
h
⟩
=
2
S
)

3
(
⟨
x
;
h
⟩ 2
S
)
 _
2
(
⟨
x
;
h
⟩ 2
S
)
_ ^
3
(
⟨
x
;
h
⟩ 2
S
)
^
3
(
⟨
x
;
h
⟩
=
2
S
)
13
This assumption can be relaxed to: under the moderate interpretation of Boolean opera-
tors, the meaning of
φ
is independent of function values that correspond to arguments outside
their domain. However, this will complicate the proof, without adding to our purpose.
14
This is a strong statement. Neither niteness, nor even type invariance of
m
is required.
12
For speci cations that contain enough type invariants, there is some set
S
such
that a behavior

j
=
3
(
⟨
x
;
h
⟩
=
2
S
) has a nite pre x that either satis es or
violates the speci cation (depending on whether the environment or system
violated their type invariant rst).
For the same reasons as above, we shouldn't expect any function to be
provably winning depending on the initial pre x of a behavior (behavior states
before the earliest state that satis es
⟨
x
;
h
⟩ 2
S
). So, we will regard the previous
result as support that if
φ
is provably realizable, then behaviors that start from
outside
S
should satisfy
φ
, independently of
f
. In other words, outside
S
,
the initial condition should determine whether a behavior is winning or losing.
Formally,
(5)
j
=
9
S
:
8
u
;
r
=
2
S
:
9
w
2
boolean
:
888
888
x
;
h
: (
⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
)
)
(
w
=
φ
)
:
So,
domain
f

S
suffices to consider all candidate winning strategies.
For example, if
φ
∆
= (
y
2
S
y
^
:::
)
+
▷
(
x
2
S
x
^
:::
)
;
then

(
x
=
2
S
x
)
) :
φ
, and

(
x
2
S
x
)
^
(
y
=
2
S
y
)
)
φ
,
so for (
x
=
2
S
x
)
_
(
y
=
2
S
y
)
 ⟨
x
;
y
⟩
=
2
S
x

S
y
, strategy
f
does not matter. This
partitioning of initial conditions is shown schematically in Fig. 2. These are all
the possible cases, but not all should occur. Clearly, if
x
2
S
x
appears in (or is
implied by) the guarantee in
+
▷
, the speci cation is unrealizable. This case is
analyzed further in Section 5.2.4.
Notice that
x
=
2
S
x
is not a set of values for
x
, and (
x
2
S
x
)
^
(
y
=
2
S
y
) not
a set of values for
y
[8, p.66], [6, 7]. No function
f
can be designed to play in a
known way from so many initial conditions, because
domain
f
would have to
be too large to be a set. Nevertheless, we need only reason about
f
in those
behaviors that satisfy (
x
2
S
x
)
^
(
y
2
S
y
). Proving that
f
does not matter
from other initial conditions allows us to ignore those initial conditions when
designing
f
. Such a proof ensures that it suffices for
domain
f
to contain all
initial conditions from where
f
can affect the outcome, and aids in mechanization
of nding
f
(the other aid is the presence of type invariants, for similar reasons).
Focusing on a set of initial conditions is independent of whether any initial
states violate
φ
. By the above, we showed that an initial condition in the form
of set containment should appear as an assumption (or within the realization
).
This is necessary for any TLA
+
de nition of synthesis, due to our unprovability
result.
It also aids mechanization, but may not be enough for mechanization. Type
invariants are an extra aid for mechanization, which may be unnecessary for
certain types of
φ
, assuming suitable theorem-proving capabilities.
13
x
2
S
x
^
y
2
S
y
x
2
S
x
^
y =
2
S
y
x
2
S
x
^
y =
2
S
y
x =
2
S
x
:
φ
holds from here
φ
holds from here
φ
holds from here
f
matters from here
Figure 2: Initial conditions from where the strategy
f
matters. The collection
of values for
x
that satisfy the predicate
x =
2
S
x
is too large to be a set. Likewise
for
y =
2
S
y
. Unlike them, the values for
⟨
x;y
⟩
that satisfy the predicate
x
2
S
x
^
y
2
S
y
does
form a set. This allows for a function
f
to be
designed
for acting
within a set as its domain.
3.3 Placing initial conditions
If some initial conditions violate
φ
, i.e.,
9
u
;
r
: (
⟨
x
;
h
⟩
=
⟨
u
;
r
⟩
)
) :
φ
(
x
;
h
)
then we must include an initial condition
I
in the realization
, for example
I
(
x
;
h
)
^
2
[
x
′
=
f
[
⟨
x
;
h
;
m
⟩
]]
⟨
x
;
h
;
m
⟩
and select
I
so that
j
=
I
(
x
;
h
)
)
Init
(
x
;
h
) (Lemma 4). We decide to not include
an initial condition in
, to keep it simpler. So, no initial state should violate
φ
. (Otherwise, no matter how we play from a violating state, we have already
lost.)
Still, we must include an initial condition in the assumption of
φ
, because
otherwise no function can be
proved
to implement
φ
(Section 3.2).
We will see in Section 5.2.4 that the de nition
15
of
+
▷
, together with the
untyped nature or TLA
+
, require including a type precondition on environ-
ment variables in the guarantee (or de ning a slight variant of
+
▷
). This is
an additional reason for not adding an initial condition to
, because then the
initial condition would appear at two places (Of course, this doesn't apply to
the aforementioned variant of
+
▷
.)
Assume that we use the operator
+
▷
to de ne
φ
∆
=
A
+
▷
G
. By Propo-
sition 9,
φ
is vacuous if
A
is unsatis able. Assume
9
x
;
h
:
A
(
x
;
h
) (satis able
assumption). By Proposition 12, initial states that violate
Init
G
violate
φ
. So,
it must be
Init
G
∆
=
true
. The only remaining location to place the initial
condition assumption is
Init
A
.
Advantages of writing the synthesis problem and the speci cation
φ
in this
way are:
14

A synthesis problem is de ned by the controllability predicates

ik
, and
a single property
φ
, instead of two separate properties
I
and
φ
. This is
simpler. It also collects everything about temporal behavior within one
property,
φ
.

The initial condition for every variable appears in the assumption
A
, em-
phasizing that it is the environment's responsibility, not the component's.
In other words,
we
should start the component
f
from admissible initial
conditions, which is what we mean by including
I
in
. Putting
I
inside
A
, instead of inside the realization
, groups it with other assumptions,
all assumptions at one place.
Disadvantages:

Symmetry is lost. The property
φ
env
∆
=
G
+
▷
A
does not anymore
express a speci cation for constructing an environment component, un-
less we reverted to de ning synthesis for the environment using an initial
condition
I
inside
. What really happened is that, by using
I
, the asym-
metry was factored out as
I
, so asymmetry was shifted outside
φ
. This
alowed
φ
env
to be obtained by simply swapping
G
and
A
. In contrast,
with the property
φ
sys
∆
= (
I
^
A
)
+
▷
G
;
where no initial states violate
G
(for the reasons explained above), the
environment should be speci ed with the property
φ
env
∆
= (
I
^
G
)
+
▷
A
;
where no initial states violate
A
(for the same reasons).

We cannot synthesize strategies for closed-system properties. So,
φ
∆
=
G
is unrealizable. We must either write it as
I
+
▷
G
, or place an initial
condition
I
within the realization
.
15
some initial
state violates
φ
includes an
initial condition
true
unprovable whether realizable in case
true
false
false
only initial values
inside some set matter
true
false
maybe realizable
φ
unrealizable
by
(Lemma 4)
(Section 3.3)
arbitrary behaviors can violate
φ
(Lemma 6)
Figure 3: Summary of results about initial conditions.
Init
G
^ :
Init
A
Init
G
^
Init
A
f
matters from here
:
Init
G
φ
:
φ
φ
?
Figure 4: Role of initial conditions in an open-system property of the form
(
Init
A
^
A
)
+
▷
(
Init
G
^
G
).
16
4 De ning realizability and synthesis
4.1 Sharing variables
We follow an approach noted by Lamport [1], along the lines of work by Abadi
and Lamport [10]. This approach formulates the synthesis problem using, for
each variable
x
, an action

x
. If a step satis es the action

x
, then it is called
a

x
-step. Any change of variable
x
in a

x
-step is attributed to player
f
x
,
possibly among other players.
This action promises to
f
x
that each step either stutters
x
, or is a
:

x
-step,
or, if
f
x
so wants, then a

x
-step that changes
x
will eventually occur. In any

x
-step that changes
x
, function
f
x
controls
x
′
.
The action

x
tells the system that it can affect certain variables in certain
steps. Conversely, it lets environment variables unconstrained by system strate-
gies. Wild environment behavior is then to be rejected by the assumption in
φ
. The de nition of action

x
should be part of the open-system speci cation
module that de nes the system property
φ
.
4.2 Realizability
Realizability is a decision problem, and synthesis the associated search prob-
lem. We can de ne realizability in TLA
+
as in Fig. 5, based on Lamport's
de nition [1] (see also Appendix C). This de nition motivates the de nition of
Fig. 6, which is in canonical form and more general. The requirements for nite
domains ensure that
f
;
g
can be implemented in the real world.
With the de nition of Fig. 5, a given temporal formula
φ
is
realizable
with
the action

if we can prove the
THEOREM
Realizability
(
φ;
)!
IsRealizable
:
Note the action's meaning
_ :

_
x
′
=
f
[
v
]
^
m
′
=
g
[
v
]
_ ⟨
m
;
x
;
y
⟩
′
=
⟨
m
;
x
;
y
⟩
This formula says that

any change of
x
;
m
in a
:

-step is attributed to the environment (disjunct
:

),

changes of
x
and
m
in a

-step are attributed to
f
and
g
(disjunct
x
′
=
f
[
v
]
^
m
′
=
g
[
v
]), or

a stuttering step occurs (disjunct
⟨
m
;
x
;
y
⟩
′
=
⟨
m
;
x
;
y
⟩
).
The brevity of this de nition owes to the de nition of a function and the un-
typeness of TLA
+
. Variants are possible, by writing two safety and liveness
17
module
RealizabilityFirst
extends
FiniteSets
state

(
;
)
temporal
φ
(
;
)
IsAFunction
(
f
)
∆
=
f
= [
u
2
domain
f
7!
f
[
u
]]
module
Inner
variables
x
;
y
constants
f
;
g
;
m
0
OnlyAllowedChanges
∆
=
8
r
:
8⟨
m
;
p
;
q
⟩ 2
domain
f
[
domain
g
:
let
v
=
⟨
m
;
p
;
q
⟩
in
_ ⟨
f
[
v
]
;
g
[
v
]
⟩
=
⟨
p
;
q
⟩
_

(
v
;
⟨
r
;
f
[
v
]
;
g
[
v
]
⟩
)
Realization
(
m
)
∆
=
let
v
∆
=
⟨
m
;
x
;
y
⟩
A
∆
=
^
x
′
=
f
[
v
]
^
m
′
=
g
[
v
]
in
^
m
=
m
0
^
2
[

(
v
;
v
′
)
)
A
]
v
^
23
_ ⟨

(
v
;
v
′
)
⟩
v
_ ^
x
=
f
[
v
]
^
m
=
g
[
v
]
Realize
∆
=
^
IsAFunction
(
f
)
^
IsFiniteSet
(
domain
f
)
^
IsAFunction
(
g
)
^
IsFiniteSet
(
domain
g
)
^
OnlyAllowedChanges
^
(
999
999
m
:
Realization
(
m
)
)
)
φ
(
x
;
y
)
Inner
(
f
;
g
;
m
0
;
x
;
y
)
∆
=
instance
Inner
IsRealization
(
f
;
g
;
m
0
)
∆
=
888
888
x
;
y
:
Inner
(
f
;
g
;
m
0
;
x
;
y
)!
Realize
IsRealizable
∆
=
9
f
;
g
;
m
0
:
IsRealization
(
f
;
g
;
m
0
)
Figure 5: A module that de nes realizability by constraining the strategy
f
to
request only
⟨
m;x
⟩
-nonstuttering steps. The module
FiniteSets
can be found
in [8, Fig.18.2, p.341].
18
module
Realizability
extends
FiniteSets
state

(
;
)
temporal
φ
(
;
)
IsAFunction
(
f
)
∆
=
f
= [
u
2
domain
f
7!
f
[
u
]]
module
Inner
variables
x
;
y
constants
f
;
g
;
m
0
Realization
(
m
)
∆
=
let
v
∆
=
⟨
m
;
x
;
y
⟩
A
∆
=
^
x
′
=
f
[
v
]
^
m
′
=
g
[
v
]
in
^
m
=
m
0
^
2
[

(
v
;
v
′
)
)
A
]
v
^
WF
⟨
m
;
x
⟩
(

(
v
;
v
′
)
^
A
)
Realize
∆
=
^
IsAFunction
(
f
)
^
IsFiniteSet
(
domain
f
)
^
IsAFunction
(
g
)
^
IsFiniteSet
(
domain
g
)
^
(
999
999
m
:
Realization
(
m
)
)
)
φ
(
x
;
y
)
Inner
(
f
;
g
;
m
0
;
x
;
y
)
∆
=
instance
Inner
IsRealization
(
f
;
g
;
m
0
)
∆
=
888
888
x
;
y
:
Inner
(
f
;
g
;
m
0
;
x
;
y
)!
Realize
IsRealizable
∆
=
9
f
;
g
;
m
0
:
IsRealization
(
f
;
g
;
m
0
)
Figure 6: A module that de nes realizability.
19
pairs, one for variable
x
, and another for
m
. The memory can be shifted to the
property
φ
itself, in which case
m
would be mentioned within
φ
.
The liveness condition requires weakly fair scheduling
23
_ ⟨

⟩
v
_ ^
x
=
f
[
v
]
^
m
=
g
[
v
]

(
32
_
x
̸
=
f
[
v
]
_
m
̸
=
g
[
v
]
)
)
23
⟨

⟩
v
:
In words, if
f
or
g
continuously request to make a change, then eventually

^
(
v
′
̸
=
v
). By the safety conjunct, this implies eventually
⟨
x
′
;
m
′
⟩
=
⟨
f
[
v
]
;
g
[
v
]
⟩
:
Speci cally for games with full information
16
(where

=
:
unchanged
⟨
m
;
x
;
y
⟩
),
the negated fairness condition means that
f
;
g
want to change
x
;
m
, but a change
never happens
:
23
_ ⟨
true
⟩
v
_ ^
x
=
f
[
v
]
^
m
=
g
[
v
]

32
^
v
=
v
′
nothing changes
^ ⟨
x
;
m
⟩ ̸
=
⟨
f
[
v
]
;
g
[
v
]
⟩
request for change
Comments on the de nition

Why not write
⟨
x
;
m
⟩
′
=
f
[
v
], instead of using two functions
f
and
g
?
Because, a function
f
can falsify
⟨
x
;
m
⟩
′
=
f
[
v
] by simply taking values
that are tuples of different length. This leads to trivial realizability, as
proved in Proposition 15. Clearly, when we think of \implementation",
we do not mean this case.
A more complicated and less readable alternative is to add the constraint
8
v
2
domain
f
:
IsATuple
(
f
[
v
])
^
Len
(
f
[
v
]) = 2
:

Universal temporal quanti cation of
v
(
888
888
v
) cannot be avoided, because
then, by the linear nesting of quanti ers, for each behavior

, we could
pick a different function
f
.

Existential temporal quanti cation of
m
(
999
999
m
) cannot be avoided, because
variable
m
is an internal variable of the implementation, so if it occurs in
φ
, then it should not be constrained by a realization, except via
x
.

To de ne controllability, we need the action

.

To avoid unprovability of realizability we have to include a set containment
as initial condition in
φ
(Lemma 6).

To quantify over a mapping
f
, it must be a set, so a function (Section 2).
16
Asynchronous reduces to stutter invariance within the assumption's action.
20