Preorder-Constrained Simulations
for Program Refinement with Effects
Koko Muroya1[0000−0003−0454−6900] , Takahiro Sanada1[0000−0003−3409−6963] , andNatsuki Urabe2[0000−0002−1554−6618]
1
RIMS, Kyoto University, Kyoto, Japan{kmuroya,tsanada}@kurims.kyoto-u.ac.jp
2
National Institute of Informatics, Tokyo, Japanurabenatsuki@nii.ac.jp

Abstract. We propose a notion of preorder-constrained simulation. It
is parameterised by a preorder (“observation preorder”) on traces, sothat it can uniformly characterise quantitative notions of program refinement for different effects, such as exception, nondeterminism andI/O. Preorder-constrained simulation is additionally parameterised bya positive number (“look-ahead bound”), and forms a generative spectrum governed by the look-ahead bound. We analyse the complexityof determining preorder-constrained similarity, and show that preorderconstrained simulation can be enhanced by the so-called up-to technique.

1

Introduction

It is often important to have two programs behave the same in programming,for example, in code refactoring and compiler optimisation. Observational equivalence [26] is the standard notion that asserts the same observable behaviour
between two programs.
Among known proof techniques for observational equivalence are coinductive
techniques. These techniques reduce the problem of observational equivalence
to stepwise comparison based on operational semantics. An important example
is applicative bisimilarity [1]. It is tailored to the ordinary reduction semantics, syntactically constructing a binary relation that characterises observational
equivalence. Together with its extension known as environmental bisimilarity[21], applicative bisimilarity is applicable to a wide range of side effects, such as
general state [21], I/O [36] and continuation [38].
Other coinductive techniques that are for abstract machines have emerged
recently. Examples are what we shall call counting simulation [27], and improvement [4] which can be seen as an instance of counting simulation. Notably,counting simulation can not only assert the same behaviour between programs,
but also compare efficiency of two programs in terms of the number of execution
steps. Despite this strength, it is only known to work on “deterministic” effects
that yield at most one result per program.

2

K. Muroya et al.
(1, Q)-similarity
.1,Q

−→

(2, Q)-similarity.2,Q−→ · · · −→Q-trace inclusion
vQ

Fig. 1: A generative spectrum, parameterised by the observation preorder Q
observation preorder Q(1, Q)-simulation

Q-trace inclusion vQ==rem{τ }Q̇
Q̇ ∩ =rem{τ }∪Ωstandard simulation
weak simulation

finite trace inclusion
weak trace inclusion
refinement Q
err for exception
refinement Q
nd for nondeterminismndQ̇ ∩ =rem{τ }(new instances)refinement Q
io for I/O

Table 1: Instances of the two ends of the generative spectrum (see Sec. 4 fordetails)

It is desirable to obtain a coinductive proof technique for observational equivalence that is applicable to various effects and capable of quantitative comparison of efficiency. We have two kinds of techniques with different strengths: (1)applicative bisimilarity and environmental bisimilarity accommodating various
effects, and (2) counting simulation and improvement which are capable of quantitative comparison. Our goal here is to enhance the techniques (2) so that they
can accommodate a wider range of effects including nondeterminism.
One of the challenges of accommodating various effects is that a notion of observational equivalence, in particular that of observation, varies between effects.
For example, nondeterministic choice is regarded as internal and unobservable.
A program or(1, 1) with a binary nondeterministic choice operator or would be
identified with a program 1. The choice (with the same result) is ignored. On
the other hand, the choice that is made according to a 1-bit input is regarded
as external and observable. A program in(1, 1), which results in 1 regardless ofthe value of the 1-bit input, would not be identified with the program 1. The received input value (0 or 1) and the induced choice (between 1 and 1) is observed.
We need to be able to both ignore and observe effectful choices.
We propose a notion of preorder-constrained simulation that is applicable toeffects such as nondeterminism and I/O, in addition to the “deterministic” effects such as exception. It is notably parameterised by an observation preorder,
a preorder on traces (or words). By altering the observation preorder, we cancharacterise quantitative notions of observational refinement, which is the asymmetric version of observational equivalence, for both internal and ignored effects,
and external and observed effects.
Preorder-constrained simulations are additionally parameterised by a positive number dubbed look-ahead bound. It determines the degree of awareness ofbranching. By altering the look-ahead bound, one can obtain a spectrum illustrated in Fig. 1. The “limit” of the spectrum is a novel generalisation of trace
inclusion (i.e. Q-trace inclusion vQ ) that is also parameterised by the observation preorder. The spectrum is generative in the sense that it yields various

Preorder-Constrained Simulations for Program Refinement with Effects

3

concrete spectra by instantiating the observation preorder Q. Some instances
are shown in Tab. 1, whose details will be evident in Sec. 4.
We analyse the complexity of determining preorder-constrained similarity.M,Q in the finite setting, and show that the complexity is polynomial time.
The complexity analysis is via a game-theoretic characterisation of preorderconstrained simulation that is similar to buffered simulation game [17,16]. We
also show that preorder-constrained simulation can be enhanced by the so-called
up-to technique [32]. We discuss and identify sufficient conditions that make theup-to technique work, in terms of observation preorders.
Our contributions can be summarised as follows.
– (Sec. 4) The notion of preorder-constrained simulation, which is a new variant of simulation for characterising observational refinement between programs (Cor. 1). Preorder-constrained simulations enjoy soundness (Thm. 1)
with respect to a novel generalisation of trace inclusion, and also monotonicity (Cor. 2) that yields a generative spectrum (Fig. 1).
– (Sec. 5) A game-theoretic characterisation of preorder-constrained simulation, with complexity analysis. The games also form a generative spectrum(Fig. 12).
– (Sec. 6) Integration of the so-called up-to technique [32], in terms of observation preorders.
Proofs of statements marked by (†) are formalised in Agda, and available athttps://github.com/urabenatsuki/preorder-constr-sim-agda. Other proofs canbe found in App. C.

2

Preliminaries

Let N be the set of natural numbers, and N+ be the set of positive numbers. Fora set X, X ∗ denotes the set {x1 . . . xn | n ∈ N; x1 , . . . , xn ∈ X} of finite words
over X. We let ε denote the empty word, X + denote X ∗ \ {ε}, and |w| denotethe length of a finite word w ∈ X ∗ .
Given X 0 ⊆ X, the filtered equality =remX 0 on the set X ∗ is defined by
w =remX 0 w0 if w and w0 are the same except for symbols in X 0 . For example,aτ bσσc =rem{τ,σ} σabτ cτ =rem{τ,σ} abc.
A preorder Q ⊆ N × N is said to be s-closed if it is closed under summation,i.e. kQl ∧ k 0 Ql0 =⇒ (k + k 0 )Q(l + l0 ). For a set Σ, a preorder Q ⊆ Σ ∗ × Σ ∗ issaid to be c-closed if it is closed under concatenation, i.e. w1 Qw2 ∧ w10 Qw20 =⇒(w1 w10 )Q(w20 w20 ).
2.1

Nondeterministic Automata

A nondeterministic automaton (NA) is a quadruple A = (X, Σ, , F ) consistingof a set X called a state space, a set Σ called an alphabet, a transition relationa⊆ X × Σ × X and a set F ⊆ X of accepting states. We write xx0 whenw
0
0
x for w = a1 · · · an when there exist x0 . . . xn ∈ X +(x, a, x ) ∈ , and x

4

K. Muroya et al.

t ::= x | t t | λx.t | t[x ← t] | n | t + t | t × t | f (t, . . . , t)

(Terms TΩ )v ::= λx.t | n(Values)

L ::= h i | L[x ← t]

(Answer contexts)

E ::= h i | E t | Lhvi E | E[x ← t] | E + t | Lhvi + E | E × t | Lhvi × E(Evaluation contexts)

τLhλx.ti L0 hvi → Lht[x ← Lhvi]i

τEhxi[x ← Lhvi] → LhEhvi[x ← v]i`t→u• ∈ {+, ×}τLhni • L0 hmi → n • mfi

f (t0 , . . . , tar(f )−1 ) → ti

` ∈ {τ } ∪ Ω`Ehti → Ehuin

Lhni → X

Fig. 2: Reduction semantics as an NA AΩ = (TΩ ∪ {X}, {τ } ∪ N ∪ Ω, →, {X})asuch that x0 = x, xn = x0 and xi−1 i xi for each i ∈ {1, . . . , n}. In particular,εx. We write x 6 and say x is stuck, if there exist no x0 ∈ X and a ∈ Σxasuch that x
x0 . An NA is said to be branching-free if its transition relation⊆ X × Σ × X satisfies the following: for any x ∈ X, if there exist two pairsaa(a1 , x1 ), (a2 , x2 ) ∈ Σ × X such that x 1 x1 and x 2 x2 , then (a1 , x1 ) = (a2 , x2 ).
The (finite) language of an NA A is a function L∗A : X → Σ ∗ defined byw
L∗A (x) := {w ∈ Σ ∗ | ∃x0 ∈ F. xx0 }. In particular, ε ∈ L∗A (x) when x ∈ F .
∗We omit the subscript and write L (x) for L∗A (x) when no confusion is likely.
2.2

A Linear Substitution Calculus with Algebraic Effects

We recall algebraic effects [29] and present their reduction semantics as an NA.
Algebraic effects are specified by a signature Ω. It is a set of algebraic operations
f , each of which comes with an arity ar(f ) ∈ N. We write f : n when ar(f ) = n.
Example 1 (algebraic operations).
1. Ωerr = {err : 0} for raising an error.
2. Ωnd = {or : 2} for nondeterministic choice between two operands.
3. Ωio = {in : 2, out0 : 1, out1 : 1} for I/O with a single bit. We focus on asingle-bit I/O for simplicity. Evaluation of a term in(t0 , t1 ) proceeds withti if the input value is i, for each i ∈ {0, 1}. Evaluation of a term outi (t)outputs the value i ∈ {0, 1} and proceeds with t.
We use the (left-to-right) call-by-value linear substitution calculus (LSC) [5]equipped with algebraic effects Ω and arithmetic. The LSC has been used as acost model of various abstract machines for the λ-calculus [3]. The LSC exploits
explicit substitutions [x ← t] to disclose cost of the traditional β-reduction.
We present reduction semantics of the LSC, with a signature Ω, as an NA
defined by Fig. 2. Transitions are labelled in a similar way as the original reduction semantics for algebraic effects [29]; labels consist of τ representing silent

Preorder-Constrained Simulations for Program Refinement with Effects
X
14
14
τ
6+8
τ
6+2×4
τ
2×3+2×4

X
14
14
τ
2×7
τ
2 × (3 + 4)

X
1
1
or0
or1
or(1, 1)(a) AΩerr (2 × (3 + 4)) and AΩerr (2 ×
3 + 2 × 4)
3

X

4

τ

τ

3+0

3+1
in0
in1
3 + in(0, 1)
τ
1 + 2 + in(0, 1)

0

1
or0

0
or1
or(1, 0)(b)
AΩnd (or(1, 1))AΩnd (or(1, 0))
3

4

3

X

1

X

5

and

4

3

4

3+0
τ
1+2+0

3+1
τ
1+2+1

τ

τ

in0
in1
in(1 + 2 + 0, 1 + 2 + 1)(c) AΩio (1 + 2 + in(0, 1)) and AΩio (in(1 + 2 + 0, 1 + 2 + 1))

Fig. 3: Example pairs of NAstransitions, N representing result values, and a set Ω = {fi | f ∈ Ω, i ∈n{0, . . . , ar(f )−1}} labelling effect transitions. We add a return transition n
Xfrom each ground value to a sole accepting state X. This extra transition enables
us to observe an evaluation result as a transition label. For t ∈ TΩ , an NA AΩ (t)is the restriction of AΩ to the states that are reachable from t.
wn
A successful evaluation of a term t is given by a sequence t  Lhni → X ofsilent or effect transitions followed by a return transition. We refer to the word
wn as a trace of t, and to n as a result of the execution. By removing the silentτtransitions →, we obtain a word w0 from w. We refer to w0 as an effect trace oft. Note that the NA AΩerr is in fact branching-free.
Example 2 (pairs of NAs).
1. In Fig. 3a, 2 × (3 + 4) has a trace τ τ 14, and 2 × 3 + 2 × 4 has a trace τ τ τ 14.
2. In Fig. 3b, terms or(1, 1) and or(1, 0) have the same effect traces {or0 , or1 }.
3. In Fig. 3c, terms 1 + 2 + in(0, 1) and in(1 + 2 + 0, 1 + 2 + 1) have the same
results {3, 4} and the same effect traces {in0 , in1 }, but not the same traces.
We can now formalise program refinement, using NAs AΩ for the signaturesin Ex. 1. The notion is quantitative, in the sense that it is parameterised by alength preorder Q ⊆ N × N.
Definition 1 ((quantitative) refinement). Let Q be a preorder on N (dubbed
length preorder).

6

K. Muroya et al.
w0

w

0
0
1. For Ωerr , t Q
err u is defined by ∀w.(t  X =⇒ ∃w .u  X ∧ |w|Q|w |).
w

w0

w

w0

0
0
2. For Ωnd , t Q
nd u is defined by ∀w.(t  X =⇒ ∃w .u  X ∧ |w|Q|w | ∧0
w =rem{τ }∪Ω w ).
nd00
3. For Ωio , t Q
io u is defined by ∀w.(t  X =⇒ ∃w .u  X ∧ |w|Q|w | ∧w =rem{τ } w0 ).

The refinement t Q
err u focuses on successful termination, and additionally,
compares the numbers of steps using Q. It asserts that when evaluation of t
terminates in m steps, evaluation of u also terminates in n steps, and moreover,mQn. An example of Q is the total relation N × N. This yields the asymmetricversion of the basic notion of observational equivalence. Another example of Q
is the greater-than-equal relation ≥, with which refinement t ≥ u can assertthat u terminates in a fewer steps.
Def. 1(2) and Def. 1(3) use the filtered equality differently to deal with different observations made for nondeterministic choice and I/O. The refinementt nd u for nondeterministic choice asserts that when evaluation of t terminates, evaluation of u also terminates with the same result. The filtered equality
w =rem{τ }∪Ω w0 in Def. 1(2) ignores effect traces, and only ensures the coinnd
cidence of results. We note that Def. 1(2) corresponds to program refinement
for angelic nondeterminism [35]. In contrast, the refinement t io u for I/O asserts that when evaluation of t terminates, evaluation of u also terminates withthe same effect trace and result. The filtered equality w =rem{τ } w0 in Def. 1(3)observes effect traces.
The three pairs of NAs in Fig. 3 all exhibit refinement. We have 2×(3+4) ≤err=
2 × 3 + 2 × 4, or(1, 1) =nd or(1, 0), and 1 + 2 + in(0, 1) io in(1 + 2 + 0, 1 + 2 + 1).
We do not always have the opposite: i.e. or(1, 0) 6=nd or(1, 1).

3Counting Simulation and its Deficiencies

We recall the simulation notion that was introduced for an abstract machinefor programs with at most one result [27]. We call it counting simulation, albeit
with no connection to counter automata. It is parameterised by a preorder Q on
natural numbers, dubbed length preorder, to count and compare the number ofsteps. The original presentation [27, Def. 4.4.1] of the counting simulation is foran unlabelled transition system, and it is equipped with an up-to technique. We
here present its naive extension to NAs, but without any up-to technique.
In this section, we let Ai = (Xi , Σ, i , Fi ) (i ∈ {1, 2}) be two NAs with thesame alphabet, and Q ⊆ N × N be an s-closed preorder.
Definition 2 (counting simulations). A binary relation R ⊆ X1 ×X2 is a Qcounting simulation from A1 to A2 if, for any (x, y) ∈ R, the following C-Final
and C-Step hold.
C-Final If x ∈ F1 , then y ∈ F2 .

Preorder-Constrained Simulations for Program Refinement with Effects

x

R

x00
w
x0
a
R y
x

x00 R
w
y0
x0
0
a
R yw
x

(b) C-Step (1) where x00 6(c) C-Step (2) where |aw|Q|w0 |y(a) C-Final

7

Fig. 4: Conditions of Def. 2. Black parts are universally quantified, and magenta
parts are existentially quantified.
X
3
3
τ
3+0

4

4

τ
3+1
τ
3 + (0 + 1)

in0
in1
3 + in(0, 0 + 1)
τ
1 + 2 + in(0, 0 + 1)

X

3
3
τ
3+0
τ
1+2+0
in0

5
5
in1
in(1 + 2 + 0, 5)

Fig. 5: Unsoundness of counting simulationa

C-Step For each x0 ∈ X1 and a ∈ Σ such that x 1 x0 , either of the following
holds.
w/ F1 .
1. There exist x00 ∈ X1 and w ∈ Σ ∗ such that x0 1 x00 6 1 and x00 ∈w
00
2. There exist x00 ∈ X1 , y 0 ∈ X2 and w, w0 ∈ Σ ∗ , such that x0
1 x ,
y

w0

0
0
00
0
2 y , |aw|Q|w |, and x Ry .

Fig. 4 illustrates the conditions of Def. 2. The condition C-Final is standard.
The condition C-Step (1) deals with a stuck and non-accepting state x00 ∈ X1
(i.e. x00 6 and x00 6∈ F1 ). A term err() ∈ TΩerr is an example of such a statein AΩerr . Lastly, C-Step (2) is the key condition of Def. 2. It asserts that any
watransition x
x0 followed by some transitions x0
x00 in A1 can be simulated
w0

by some transitions yy 0 in A2 .
Thanks to C-Step, which compares not just single steps but numbers of steps,
counting simulation can witness quantitative refinement for exception.
Proposition 1 (correctness wrt. refinement). If R is a Q-counting simulation from AΩerr to AΩerr , then tRu =⇒ t Qtu
err u holds for any t, u ∈ TΩerr .
Example 3. For the pair of branching-free NAs in Fig. 3a, a relation Rdistr ={(2 × (3 + 4), 2 × 3 + 2 × 4), (X, X)} is a ≤-counting simulation. The length
preorder ≤ asserts that 2 × (3 + 4) has better efficiency. The relation Rdistrrepresents the distributive law, without relating any intermediate states.
Nevertheless, counting simulation cannot witness refinement for effects suchas nondeterminism and I/O. This is due to two challenges. The first challenge

8

K. Muroya et al.

is varying observation. While we ignore effect traces for nondeterminism, weobserve effect traces for I/O. However, counting simulation can neither ignore
nor observe effect traces correctly. It simply compares the lengths of traces using
the length preorder Q. The second challenge is branching. It is branching effects
that counting simulation becomes unsound for.
Example 4 (unsoundness for I/O). For the pair of NAs in Fig. 5, refinement does
not hold, i.e. 1 + 2 + in(0, 0 + 1) 6io in(1 + 2 + 0, 5), because right branches havetraces τ in1 τ τ 4 6=remτ in1 5. However, the relation {(1 + 2 + in(0, 0 + 1), in(1 +2 + 0, 5)), (X, X)} is an =-counting simulation. It only asserts that left branches
have “identical” traces (i.e. τ in0 τ 3 and in0 τ τ 3), and it does not inspect the rightbranches with distinct traces.
This unsoundness is because counting simulation does not necessarily inspect all
possibilities of branching. Technically, this is due to the existential quantificationw
x00 in C-Step (2).
on x0

4

Preorder-Constrained Simulation

4.1

Definition

We present our main contribution, the notion of preorder-constrained simulation.
It generalises counting simulation from branching-free NAs to general NAs, andhence characterises a notion of observational refinement for a wider class ofeffects (Cor. 1 below). The generalisation is technically two-fold, dealing withthe two challenges we discussed in Sec. 3.
Firstly, preorder-constrained simulation is parameterised by a c-closed preorder Q on traces Σ ∗ , dubbed observation preorder, instead of the length preorder Q ⊆ N × N that parameterises counting simulation. Using preorders likethe filtered equality =remX , preorder-constrained simulation can flexibly observeand compare traces, adapting to varying observations.
Example 5 (observation preorders). Note that the following preorders are all cclosed.
1. The equality = on words.
2. Each preorder Q ⊆ N × N that is s-closed induces a preorder Q̇ on words
such that wQ̇w0 ⇐⇒ |w|Q|w0 |, which is c-closed.
3. Each subset Σ 0 ⊆ Σ induces the preorder =remΣ0 ⊆ Σ ∗ × Σ ∗ of filteredequality.
4. The substring preorder ⊆sub , where w ⊆sub w0 means that w is a substringof w0 .
5. Assume Σ is the powerset 2AP of some set AP. Let ⊆∗ be a preorder where
a1 . . . ak ⊆∗ a01 . . . a0k0 means k = k 0 and ∀i. ai ⊆ a0i .
6. Let R be the set of real numbers, and • be a binary operation on R suchas summation + and multiplication ×. When Σ = R, let ≤• be a preorderwhere a1 . . . an ≤• a01 . . . a0n0 means a1 • · · · • an ≤ a01 • · · · • a0n0 . Its inverse≥• is also a preorder.

Preorder-Constrained Simulations for Program Refinement with Effects

9

xM
y0
x0
0
w
R yw
x
(a) Final M where |w| < M ∧ wQw0

w

R

y0
0
R yw
x

xk

(b) Step M where a1 · · · ak Qw0

Fig. 6: Conditions of Def. 3. Black parts are universally quantified, and magenta
parts are existentially quantified.
Secondly, preorder-constrained simulation limits the existential quantificaw
x00 in C-Step (2), to overcome the unsoundness duetion, namely that on x0
to incomplete inspection of branching. The idea is to put the existential quantification inside universal quantification, so that every branch gets inspected by
the resultant simulation notion.
Additionally, preorder-constrained simulation is parameterised by a positive
number M dubbed look-ahead bound. It determines the degree of awareness ofbranching; we leave the study of the look-ahead bound to Sec. 4.3. We let Ai =(Xi , Σ, i , Fi ) (i ∈ {1, 2}) be two NAs with the same alphabet, Q ⊆ N × N be
an s-closed preorder, and Q ⊆ Σ ∗ × Σ ∗ be a c-closed preorder.
Definition 3 ((M, Q)-simulations). For each M ∈ N+ , a binary relation R ⊆X1 × X2 is an M -bounded Q-constrained simulation ( (M, Q)-simulation in
short) from A1 to A2 if, for any (x, y) ∈ R, the following FinalM and StepM
hold.
Final M For each w = a1 . . . an ∈ Σ ∗ and x1 . . . xn ∈ X1∗ such that n < M ,aax 1 1 x1 · · · n 1 xn and xn ∈ F1 , there exist w0 ∈ Σ ∗ and y 0 ∈ X2 such thatw0

wQw0 , y 2 y 0 and y 0 ∈ F2 .
aa
Step M For each a1 . . . aM ∈ Σ M and x1 . . . xM ∈ X1M such that x 1 1 x1 · · · M 10∗0xM , there exist k ∈ {1, . . . , M }, w ∈ Σ and y ∈ X2 such that a1 · · · ak Qw0 ,
y

w0

2 y

0

and xk Ry 0 .

When an (M, Q)-simulation relates x and y, we say x is (M, Q)-similar to y
and write x .M,Q y. When R is an (M, Q)-simulation from A to A, we say it ison A.
Fig. 6 illustrates the conditions of Def. 3. The difference between Fig. 4c
and Fig. 6b is crucial to overcome the incomplete inspection of branching thatcounting simulation suffers from. In Fig. 6b, existential quantification is limited
to xk , which is an intermediate state of the sequence x
xM that is universallyquantified.
4.2

Soundness

Thanks to the observation preorder Q and the limited existential quantification,
preorder-constrained simulation can characterise notions of quantitative refine-10

K. Muroya et al.

ment Q for all the signatures Ω in Ex. 1. Namely, (M, Q)-simulations provide
a sufficient condition for refinement.
Corollary 1 (correctness of (M, Q)-simulations wrt. refinement).
1. For any M ∈ N+ and t, u ∈ TΩerr , t .M,Q̇ u =⇒ t Q
err u.
2. For any M ∈ N+ and t, u ∈ TΩnd , t .M,Q̇∩=remu =⇒ t Qnd u.
{τ }∪Ωnd

3. For any M ∈ N+ and t, u ∈ TΩio , t .M,Q̇∩=rem{τ }u =⇒ t Q
io u.

t
u

Example 6 (Fig. 3 revisited).
˙
1. For the NAs in Fig. 3a, {(2 × (3 + 4), 2 × 3 + 2 × 4), (14, 14)} is a (2, ≤)simulation. This simulation represents the distributive law.
2. For Fig. 3b, {(or(1, 1), or(1, 0)), (1, 1), (X, X)} is a (1, =∪=˙
rem{τ }∪Ωnd )-simulation.
3. For Fig. 3c, let t1 ≡ 1 + 2 + in(0, 1) and t2 ≡ in(1 + 2 + 0, 1 + 2 + 1). The
filtered equality =rem{τ } distinguishes traces of length 1 from t1 , t2 , namely:τ 6=rem{τ } ini (i ∈ {0, 1}). This leads to non-existence of any (1, =∩˙ =rem{τ } )simulation that includes the pair (t1 , t2 ). In contrast, the filtered equality canidentify traces of length 2 from t1 , t2 , namely: τ ini =rem{τ } ini τ (i ∈ {0, 1}).
This leads to existence of a (2, =∩˙ =rem{τ } )-simulation. It can be given by{(t1 , t2 ), (3 + 0, 3 + 0), (3 + 1, 3 + 1), (X, X)}.
Cor. 1 is a consequence of a soundness property of preorder-constrained simulations. Namely, (M, Q)-simulations are sound with respect to a novel generalisation (Def. 4 below) of trace inclusion that is also parameterised by theobservation preorder Q.
Definition 4 (Q-trace inclusion). We write x vQ y and say Q-trace inclusion holds between x and y, if the following holds: ∀w ∈ L∗A1 (x). ∃w0 ∈L∗A2 (y). wQw0 .
Theorem 1 ((†) soundness). Let M ∈ N+ . For any (x, y) ∈ X1 × X2 , it holds
that x .M,Q y =⇒ x vQ y.
The three refinement relations for specific NAs AΩerr , AΩnd and AΩio , definedin Sec. 2.2, are instances of the generalised trace inclusion. Cor. 1 follows fromThm. 1 above and Prop. 2 below.
Proposition 2 (refinement as trace inclusion).
1. For AΩerr , for any t, u ∈ TΩerr , t Q
err u ⇐⇒ t vQ̇ u.
2. For AΩnd , for any t, u ∈ TΩnd , t Q
nd u ⇐⇒ t vQ̇∩=rem
3. For AΩio , for any t, u ∈ TΩio , t Q
io u ⇐⇒ t vQ̇∩=remu.

{τ }∪Ωnd

u.

t
u

{τ }

The most basic instance of the Q-trace inclusion is when Q is the equality;
it coincides with the standard notion of (finite) trace inclusion. Another basic
instance is when Q is the filtered equality =rem{τ } ; it corresponds to the wellknown notion of weak trace inclusion.

Preorder-Constrained Simulations for Program Refinement with Effects
a

x2
a
x1
a
x

a

y2
a
y

(a) =-trace inclusion
b

x2
a
x

b

y2
b
y1
a
y

(c) ⊆sub -trace inclusion

x2
τ
x1
τ
x

a

{a} x2
{b}
x1
{a}
x

11

y2

a

τ
y

(b) =rem{τ } -trace inclusion{a, b}y2{a, b}

2x1

1y(d) ⊆∗ -trace inclusion

y2

x2

x

0

0
y1

3
y

1

(e) ≤+ -trace inclusion

Fig. 7: Pairs of NAs that exhibit Q-trace inclusion
Example 7 (Q-trace inclusions for various preorders). Fig. 7 shows examples of
Q-trace inclusions for some of the preorders from Ex. 5.
1. In Fig. 7a, we have L∗ (x) = aaa∗ = {an+2 |n ∈ N} and L∗ (y) = aa∗ ={an+1 |n ∈ N}, and therefore, L∗ (x) ⊆ L∗ (y). We have x v= y for theequality =.
2. In Fig. 7b, we have L∗ (x) = τ τ a∗ and L∗ (y) = τ a∗ . These two sets coincide
when we ignore τ . We therefore have x v=rem{τ } y for the filtered equality=rem{τ } .
3. In Fig. 7c, we have L∗ (x) = ab∗ and L∗ (y) = abb∗ . We hence have x v⊆sub ywhere ⊆sub is the substring preorder from Ex. 5(4).
4. In Fig. 7d, we have L∗ (x) = {a}{b}{a}∗ and L∗ (y) = {a, b}{a, b}∗ . We hence
have x v⊆∗ y where ⊆∗ is from Ex. 5(5).
5. In Fig. 7e, we have L∗ (x) = {1, 02} and L∗ (y) = {3, 10}. It holds that 1 ≤ 3
and 0 + 2 ≤ 3. We hence have x v≤+ y where ≤+ is from Ex. 5(6).

4.3

Basic Properties

Here we investigate the look-ahead bound M of preorder-constrained simulation.
As observed in Ex. 6 (3), the look-ahead bound determines the degree of awareness of branching; as M increases, (M, Q)-simulation can inspect and identify
further branches. Technically, preorder-constrained simulation has a monotonicity property with respect to M .
Lemma 1 ((†) monotonicity of Final and Step). Let M, N ∈ N+ such thatM ≤ N.
1. FinalN =⇒ FinalM
3. StepM ∧ FinalM =⇒ FinalN
M
N
2. Step =⇒ Steptu
Corollary 2 (monotonicity). Let M, N ∈ N+ such that M ≤ N . Each (M, Q)simulation from A1 to A2 is also an (N, Q)-simulation from A1 to A2 .

12

K. Muroya et al.
x0M +1

xM +1
b

x02

x2
b

x1
a
x0

c

y20
c
y10

y2
b
y1
a

y0

(a) For M = 1

a

xM
a
..
.
a
x1
a
x0

c

yM +1
b
yM
a
..
.
a
y1
a

y0

0
yM
+1
c
0
yM
a
..
.
a
y10
a

(b) For arbitrary M

Fig. 8: Pairs of NAs that distinguish (M, =)-similarity and (M + 1, =)-similarity
When the observation preorder Q is the equality =, this monotonicity isstrict; in other words, strict inclusion .M,= ( .M +1,= holds. There exists apair of NAs that does not have an (M, =)-simulation but has an (M + 1, =)-simulation. Fig. 8 shows such pairs; one for M = 1, and the other for an
arbitrary M . For Fig. 8a, we have a (2, =)-simulation {(x0 , y0 ), (x1 , y1 ), (x1 , y10 ),(x2 , y2 ), (x02 , y20 )}. Similarly, for Fig. 8a, we have a (M +1, =)-simulation {(x0 , y0 ),00), (xM +1 , yM +1 ), (x0M +1 , yM
(xM , yM ), (xM , yM+1 )}.
The monotonicity is in contrast to that of nested simulations [12] which arealso parameterised by a positive number. As M increases, (M, Q)-simulations
become larger (as a relation), while M -nested simulations become smaller. WhenM = 1 (and Q is the equality), (1, =)-simulation coincides with the standard
simulation, and hence with 1-nested simulation.
Cor. 2 validates the spectrum of preorder-constrained similarities in Fig. 1,
which is governed by the look-ahead bound. Its “limit” can be given by the notionof Q-trace inclusion, thanks to the soundness property (Thm. 1).
The spectrum in Fig. 1 is generative because, by instantiating the observation
preorder Q, we can obtain various concrete spectra, as shown in Tab. 1. For
instance, when Q is the equality = or the filtered equality =rem{τ } , the spectrum
refines a part of (the asymmetric version of) van Glabbeek’s spectrum [13,14].
The other spectra of Tab. 1 are more of our interest here, which yield simulation
notions that characterise program refinement.
Finally, while (M, Q)-simulations are closed under union, they are not closed
under the standard composition of relations.
Lemma 2 ((†) basic properties). Let M ∈ N+ , and I be an arbitrary set.
S
1. Given a family {Ri }i∈I of (M, Q)-simulations, i∈I Ri is an (M, Q)-simulation.
2. The (M, Q)-similarity .M,Q is the largest (M, Q)-simulation.
Example 8 (no closedness under composition).

Preorder-Constrained Simulations for Program Refinement with Effects
x31

x32

x33

x34

τ

τ

τ
x22
τ

τ

x21
τ

x1

y21

y22

y23

y24

τ

τ

τ
y12
τ

τ

y11
τ

τ
x

y

z11

z12
z13
τ τ
τ
τ
z

13

z14

Fig. 9: A counterexample of closedness under composition
x2
b
x1
a
x

y1
a
y

z

(a) (2, =)-simulations

x2
c
x1
a
x

y2
c
y1
b
y

z1
d
z

(b) (2, Qe )-simulations

Fig. 10: More counterexamples of closedness under composition
1. Let > = {τ }∗ ×{τ }∗ . For the three NAs in Fig. 9, {(x, y), (x21, y11), (x22, y12),(x31, y21), (x32, y22), (x33, y23), (x34, y24)} and {(y, z), (y21, z11), (y22, z12),(y23, z13), (y24, z14)} are (2, >)-simulations, but their composition {(x, z),(x31, z11), (x32, z12), (x33, z13), (x34, z14)} is not a (2, >)-simulation. The
composition is a (3, >)-simulation instead.
2. For the three NAs in Fig. 10a, {(x, y), (x1 , y1 )} and {(y, z)} are (2, =)simulations, but their composition {(x, z)} is not a (2, =)-simulation.
3. Let Qe be the reflexive and c-closed closure of {(a, bc), (b, d)}. For the three
NAs in Fig. 10b, {(x, y), (x1 , y2 )} and {(y, z), (y1 , z1 )} are (2, Qe )-simulations,but their composition {(x, z)} is not a (2, Qe )-simulation.

5

Game-Theoretic Characterisation

Preorder-constrained simulations can be characterised by two-player reachability
games. The game is parameterised by the observation preorder Q, the look-aheadbound M , and additionally a catch-up bound N . Both numerical bounds M, N
are now taken from N+ ∪ {∞}.
M,N,Q
M,N,Q
Definition 5 (GA). Let M, N ∈ N+ . A two-player game GA
between
1 ,A2
1 ,A2
Challenger and Simulator is defined by Fig. 11. Simulator wins if they reach thestate sim-win, Challenger has no possible move, or the play continues forever.
M,N,Q
In a game GA, Challenger is in charge of A1 , and Simulator is in charge
1 ,A2
of A2 . Most of the positions are of the form (w, x, y), where w ∈ Σ ∗ represents
a queue of labels that Challenger has inputted into A1 . The two numericalparameters M, N both constrain Simulator’s ability to make a move. The lookahead bound M limits the length of the queue w, and equivalently the number

14

K. Muroya et al.

Position

Player

Move

Guard
0

a

(wa, x , y) x 1 x0
(X, w, x, y) x ∈ F1
(w, x0 , y) |w| < M
Simulator∃w0 ∈ Σ ∗ .
(ε, x0 , y 0 )w0|w0 | < N ∧ y 2 y 0 ∧ wQw0
∃w0 ∈ Σ ∗ .∃y 0 ∈ F2 .
(X, w, x, y)
Simulator sim-win∗
w0∈ {X} × Σ × X1 × X2
|w0 | < N ∧ y 2 y 0 ∧ wQw0
(w, x, y)∈ Σ ∗ × X1 × X2
(w, x0 , y)∈ Σ ∗ × X1 × X2

Challenger

1
2
3
4
5

a

1 Challenger chooses x 1 x0 from the current state x and enqueues the label a.
2 Challenger is at an accepting state x ∈ F1 . Challenger forces Simulator to check
whether an accepting state is reachable from y ∈ X2 .
3 Simulator skips the turn. This move is always possible when M = ∞.
4 Simulator simulates Challenger’s moves in the queue w.
5 Simulator simulates Challenger’s moves in the queue w and reaches an accepting
state.
M,N,Q
Fig. 11: Two-player game GA
characterising (M -bounded) Q-constrained
1 ,A2
simulation.

of turns that Simulator can skip consecutively. The catch-up bound N limits thenumber of transitions Simulator can make in A2 to dequeue w.
M,N,Q
The games GA
satisfy two expected properties: monotonicity with re1 ,A2
spect to both M and N (Lem. 3 below), and correspondence with (M, Q)similarity (Prop. 3 below). These results validate a generative (two-dimensional)
spectrum of games and preorder-constrained simulations shown in Fig. 12.
Lemma 3 (monotonicity). Let M, M 0 ∈ N+ such that M ≤ M 0 , and let
N, N 0 ∈ N+ such that N ≤ N 0 . If Simulator is winning from a state (w, x, y) in
M,N,Q
M 0 ,N 0 ,Q
GA
, Simulator is also winning from the state in GA
.
t
u
1 ,A2
1 ,A2
Proposition 3 (correctness). Let M ∈ N+ . Simulator is winning from a stateM,∞,Q(ε, x, y) in GA, if and only if x .M,Q y.
t
u
1 ,A2
We conclude this section with complexity analysis of determining winning
M,N,Q
positions in GA, and hence of determining (M, Q)-similarity .M,Q .
1 ,A2
Proposition 4 (complexity). Assume that wQw0 can be checked in linear
time to the lengths of w and w0 . For M, N ∈ N+ , whether Simulator is winning
M,N,Q
from a state (ε, x, y) in GA
can be checked in O(|Σ|M +N × |X1 | × |X2 |2 )
1 ,A2
time.
Proof. For a set X and for k, l ∈ N such that k ≤ l, let X [k,l] denote the set{x1 x2 . . . xn | k ≤ n ≤ l; x1 , . . . , xn ∈ X}.
M,N,Q
We first approximate the complexity to construct the game GA, assuming
1 ,A2that the membership to F1 , F2 , 1 and 2 can be checked in constant time. The

Preorder-Constrained Simulations for Program Refinement with Effects

15.1,Q −→ .2,Q −→ · · · −→ Q-trace inclusion vQ
↑
..
.
↑

↑
..
.
↑

2,2,Q
1,2,Q
−→ · · · −→ Q-trace inclusion vQ
−→ GA
GA
1 ,A2
1 ,A2

↑

↑

2,1,Q
1,1,Q
−→ · · · −→
−→ GA
GA
1 ,A2
1 ,A2

Q-trace inclusion vQ

M,N,Q
Fig. 12: A generative spectrum of games GA
and similarities .M,Q
1 ,A2

number of positions of the game is O(|Σ|M × |X1 | × |X2 |), because Challenger’s
positions are elements of Σ [0,M −1] × X1 × X2 , and Simulator’s positions are
elements of Σ [0,M ] × X1 × X2 or {X} × Σ [0,M ] × X1 × X2 .
For each pair (p, q) of positions, we approximate the complexity to determine
if a move is possible from p to q, by case analysis on the possible moves (seeFig. 11).
a– Case 1 . It suffices to check x 1 x0 , which can be done in constant time.
– Case 2 . It suffices to check x ∈ F1 , which can be done in constant time.
– Case 3 . It suffices to check |w| < M , which can be done in constant time,
because M is a constant here.
– Case 4 . By the condition |w0 | < N , w0 can be chosen from Σ [0,N −1] . Checkw0

ing y 2 y 0 is O(N − 1) time and hence constant time, and checking wQw0
is also constant time, because both M and N are constants here. Overall,this move can be determined in O(|Σ|N ) time.
– Case 5 . This case is similar to the case 4 , with extra choice of y 0 fromF2 ⊆ X2 . This move can be determined in O(|Σ|N × |X2 |) time.
Once the game is constructed, its winning region (i.e. the positions fromwhich Simulator is winning) can be determined in O(|Σ|M × |X1 | × |X2 |) time
multiplied by O(|Σ|N × |X2 |) time, because the game is a reachability game.
M,N,Q
Consequently, whether Simulator is winning from a state (ε, x, y) in GA
can
1 ,A2
M +N
2
be checked in O(|Σ|× |X1 | × |X2 | ) time.
tu

6Preorder-Constrained Simulation Up-To

We here integrate the up-to technique [32] into preorder-constrained simulation.
The technique is widely used for enhancing (bi-)simulation notions. It allows
a smaller relation, which is not necessarily a simulation itself, to witness trace
inclusion. The up-to version of preorder-constrained simulation is additionallyparameterised by a pair of binary relations (R1 , R2 ) on state spaces. The following definition is obtained by simply replacing R in Def. 3 with R1 ; R; R2 , where; is the composition of binary relations.

16

K. Muroya et al.

x2
x

0

0

x12
x11

3

−1

−1

x2
y2 0

0

y1

−1

x1

0

0
0

x

y

y 0

Fig. 14: An unsound (1, ≥+ )-simulation
Fig. 13: A (1, ≥+ )-simulation up-to up-to
Definition 6 ((M, Q)-simulations up to (R1 , R2 )). Let R1 ⊆ X1 × X1 andR2 ⊆ X2 × X2 . For each M ∈ N+ , a binary relation R ⊆ X1 × X2 is an (M, Q)simulation up to (R1 , R2 ) from A1 to A2 if, for any (x, y) ∈ R, FinalM (seeDef. 3) and U-StepM below hold.
a

U-Step M For each w = a1 . . . aM ∈ Σ M and x1 . . . xM ∈ X1M such that x 1 1
aa
x1 2 1 · · · M 1 xM , there exist k ∈ {1, . . . , M }, w0 ∈ Σ ∗ and y 0 ∈ X2 suchthat a1 · · · ak Qw0 , y

w0

2 y

0

and xk (R1 ; R; R2 )y 0 .

The question now is when a preorder-constrained simulation up to (R1 , R2 )is sound with respect to Q-trace inclusion. The relations R1 and R2 cannot be
arbitrary, and they should be consistent to the Q-trace inclusion vQ . Formally,
they should satisfy R1 ⊆ vQ1 and R2 ⊆ vQ2 for some preorders Q1 , Q2 ⊆Σ ∗ × Σ ∗ such that (Q1 ; Q; Q2 ) ⊆ Q.
Example 9 ((M, ≥+ )-constrained simulation up to (v≥+ , v≥+ )). Recall the preorder ≥+ from Ex. 5(6). It is feasible to use a ≥+ -constrained simulation up to(v≥+ , v≥+ ). The first reason is that the consistence property is satisfied, thanks
to transitivity of the preorder ≥+ . The second reason is that the ≥+ -trace inclusion v≥+ between two states of the same NA can be checked efficiently witha graph algorithm. Specifically, for two states x, x0 of the same NA, x v≥+ x0
holds if the summation of weights on each path from x to x0 is non-negative.
Example 10 ((1, ≥+ )-simulation up-to). For a pair of NAs shown in Fig. 13,x v≥+ y holds, but there exists no (1, ≥+ )-simulation that relates x with y. In
contrast, a relation R = {(x, y), (x12 , y1 ), (x2 , y2 )} is a (1, ≥+ )-simulation up to(v≥+ , v≥+ ). The pair (x, y) satisfies the condition U-Step 1 of Def. 6, because wehave x11 v≥+ x12 R y1 v≥+ y1 . The up-to allows us to move U-Step1 towards
the accepting state x2 , that is, it allows us to deal with U-Step 1 of (x12 , y1 )instead of (x11 , y1 ).
However, the consistence property (Q1 ; Q; Q2 ) ⊆ Q is not enough to achievesoundness. A naive combination of the weak simulation notion, which coincides
with our similarity .1,=rem{τ } , and an up-to technique is known to be unsound,and requires special care [30,31]. The following counterexample is inspired by
the one for weak simulation from the literature [30,31].
Example 11 (unsound (1, ≥+ )-simulation up-to). For a pair of NAs shown in
Fig. 14, x v≥+ y does not hold, because no accepting state is reachable from y.

Preorder-Constrained Simulations for Program Refinement with Effects

17

However, a relation {(x, y)} is a (1, ≥+ )-simulation up to (v≥+ , v≥+ ). The pair(x, y) indeed satisfies U-Step 1 , because x1 v≥+ x R y v≥+ y. Here, the up-to
allows us to move U-Step1 away from the accepting state x2 : namely, it allows
us to deal with U-Step 1 of (x, y) instead of (x1 , y).
From the two examples above, we can extract an additional condition on thepreorders Q, Q1 , Q2 , namely on Q1 . We can observe that, while it is safe to move
U-Step M toward an accepting state (Ex. 10), it is unsafe to move it away froman accepting state (Ex. 11), for the sake of soundness. To prohibit the unsafe
move, the additional condition is required, namely wQ1 w0 =⇒ |w| ≥ |w0 |.
˙ induced by ≥ ⊆ N × N,
Examples of such Q1 are the equality =, the preorder ≥−1∗
the inverse (⊆sub ) , and ⊆ (see Ex. 5).
The condition is inspired by a soundness criterion for counting simulation
up-to [27, Def. 4.3.13]. A similar idea can be found in Pous’ work [30,31] on
weak simulation up-to.
Theorem 2 ((†) soundness). Let M ∈ N+ . Let R ⊆ X1 × X2 , R1 ⊆ vQ1 andR2 ⊆ vQ2 be binary relations, for preorders Q1 , Q2 ⊆ Σ ∗ × Σ ∗ such that (i)(Q1 ; Q; Q2 ) ⊆ Q and (ii) wQ1 w0 =⇒ |w| ≥ |w0 |. If R is an (M, Q)-simulation
up to (R1 , R2 ), it holds that xRy =⇒ x vQ y for any (x, y) ∈ X1 × X2 .
Example 12 (weak simulation up to “expansion/contraction”). Let Qe be a pre˙ The (1, Qe )-similarity .1,Qe is akin to expansion [34] andorder =rem{τ } ∩ ≥.
contraction [33] that have been used with an up-to technique. It is indeed valid
to have the weak simulation up to the similarity .1,Qe . More precisely, we canhave a (1, =rem{τ } )-simulation, which is the weak simulation, up to (.1,Qe , =).
The three preorders =rem{τ } , Qe and = satisfy the two conditions in Thm. 2;
˙ We
we have (Qe ; =rem{τ } ; =) ⊆ =rem{τ } , and the preorder Qe satisfies Qe ⊆ ≥.
also have .1,Qe ⊆ vQe by soundness (Thm. 1), and = ⊆ v= .

7

Related Work

M,N,Q
Our two-player game GA
is similar to buffered simulation game [17,16].
1 ,A2
While ours is for NAs with finite languages, the latter is for Büchi automata.
We contribute to coinductively defining the simulations and investigating thegenerative spectrum.
Quantitative simulation notions are known for weighted automata: many arefor probabilistic systems [24,19,15]; a general simulation notion for automata
weighted with semirings (e.g. R with + and ×, and R with max and + a.k.a.
tropical semiring) was introduced as a matrix over real numbers [37].
Preorder-constrained simulations are defined for NAs, but can be quantitative, in the sense that they can compare lengths of accepted runs (e.g. using
˙ Known (bi-)simulation notions such as expansion [34] and conthe preorder ≥).
traction [33] are also capable of such quantitative comparison. As mentioned in˙
Ex. 12, the (1, =rem{τ } ∩ ≥)-similarity
is akin to these (bi-)simulation notions
seen as simulation notions.

18

K. Muroya et al.

Prop. 4 suggests that we can reduce the problem of checking refinement
between programs to determining a winning region of the reachability game
M,N,Q
GA
. Algorithmic game semantics [2,20] is another approach to reduce pro1 ,A2gram refinement to solving games. A notable difference is that algorithmic gamesemantics restricts types of programs, while our approach would require a program t to induce a finite automaton AΩ (t).
Our work is not the first to characterise or refine the LT–BT spectrum using
a simulation notion or a game. It would be interesting to compare existing work,
e.g. [10,8], to ours in details. Ordered words are not a new research topic either,
but the literature seems to focus on decidability of their theory, e.g. [22,23].

8

Conclusion and Future Work

We proposed a notion of preorder-constrained simulation. Being parameterisedby the observation preorder on traces, it can uniformly characterise quantitative notions of observational refinement for different algebraic effects: exception,
nondeterminism and I/O. We demonstrated this using reduction semantics for
the LSC.
Being additionally parameterised by the look-ahead bound, preorder-constrained simulations form a generative spectrum. Its “limit” is given by a novel
generalisation of trace inclusion. The spectrum is generative in the sense that it
can be instantiated variously according to the observation preorder.
We additionally presented a characterisation of preorder-constrained simulation as a two-player reachability game, and showed that preorder-constrained
similarity can be determined in polynomial time in the finite setting. Finally, we
studied enhancement of preorder-constrained simulation, showing how to integrate an up-to technique, in terms of observation preorders.
One direction of future work is to extend the characterisation of program
refinement to probabilistic choice. This would require preorder-constrained simulation to work on weighted automata instead of NAs. One can try to accommodate probabilistic choice into the current work, using the preorder ≤+ ,but a naive approach does not work. It results in a false refinement such as
or0.5 (1, 1) v≤+ or0.5 (0, 1), where or0.5 is an operation that chooses either argument with probability 0.5. It would also be interesting to connect preorderconstrained simulation to a generic metatheory of algebraic effects [18,35].
Another future work is to develop a methodology to constructing a preorderconstrained simulation. For the automaton AΩ induced by a signature Ω, it
would be particularly important to construct a preorder-constrained simulationthat is closed under term construction. Such a simulation would characterise contextual refinement, which asserts refinement between two terms in an arbitrary
context. Counting simulation was originally used in this way [27].
Acknowledgments. We are grateful to Ichiro Hasuo and Shigeru Chiba for insightfulcomments. The first and second authors are supported by JST, ACT-X Grant No.
JPMJAX190U, Japan, and JSPS, KAKENHI Project No. 22K17850, Japan. The third

Preorder-Constrained Simulations for Program Refinement with Effects

19

author is supported by JST ERATO HASUO Metamathematics for Systems Design
Project (No. JPMJER1603).

References
1. Abramsky, S.: The lazy lambda-calculus, p. 65–117. Addison Wesley (1990)
2. Abramsky, S.: Algorithmic Game Semantics, NATO Science Series, vol. 62,
pp. 21–47. Springer Netherlands, Dordrecht (2002). https://doi.org/10.1007/
978-94-010-0413-8_2, https://_doi.org/10.1007/978-94-010-0413-8_2
3. Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: ICFP
2014. pp. 363–376. ACM (2014). https://doi.org/10.1145/2628136.2628154
4. Accattoli, B., Dal Lago, U., Vanoni, G.: The machinery of interaction. In: PPDP
’20: 22nd International Symposium on Principles and Practice of Declarative
Programming, Bologna, Italy, 9-10 September, 2020. pp. 4:1–4:15. ACM (2020),
https://doi.org/10.1145/3414080.3414108
5. Accattoli, B., Kesner, D.: The structural lambda-calculus. In: CSL 2010. vol. 6247,
pp. 381–395. Springer (2010). https://doi.org/10.1007/978-3-642-15205-4_30
6. Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)
7. Banerjee, A., Pal, B., Das, S., Kumar, A., Dasgupta, P.: Test generation games
from formal specifications. In: Sentovich, E. (ed.) Proceedings of the 43rd Design
Automation Conference, DAC 2006, San Francisco, CA, USA, July 24-28, 2006.
pp. 827–832. ACM (2006), https://doi.org/10.1145/1146909.1147120
8. Bisping, B., Jansen, D.N., Nestmann, U.: Deciding all behavioral equivalences at
once: A game for linear-time-branching-time spectroscopy. Log. Methods Comput.
Sci. 18(3) (2022), https://doi.org/10.46298/lmcs-18(3:19)2022
9. Cormie-Bowins, E., van Breugel, F.: Measuring progress of probabilistic LTLmodel checking. In: Wiklicky, H., Massink, M. (eds.) Proceedings 10th Workshop
on Quantitative Aspects of Programming Languages and Systems, QAPL 2012,
Tallinn, Estonia, 31 March and 1 April 2012. EPTCS, vol. 85, pp. 33–47 (2012),
https://doi.org/10.4204/EPTCS.85.3
10. de Frutos-Escrig, D., Gregorio-Rodríguez, C., Palomino, M., Romero-Hernández,
D.: Unifying the linear time-branching time spectrum of process semantics. Log.
Methods Comput. Sci. 9(2) (2013), https://doi.org/10.2168/LMCS-9(2:11)2013
11. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic
on finite traces. In: Rossi, F. (ed.) IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 39, 2013. pp. 854–860. IJCAI/AAAI (2013), http://www.aaai.org/ocs/index.php/
IJCAI/IJCAI13/paper/view/6997
12. de Frutos-Escrig, D., Gregorio-Rodríguez, C.: Constrained simulations, nested simulation semantics and counting bisimulations. In: Pimentel, E. (ed.) Proceedings of the Seventh Spanish Conference on Programming and Computer Languages, PROLE 2007, Zaragoza, Spain, September 12-14, 2007. Electronic Notes
in Theoretical Computer Science, vol. 206, pp. 41–58. Elsevier (2007), https://doi.org/10.1016/j.entcs.2008.03.074
13. van Glabbeek, R.J.: The linear time-branching time spectrum (extended abstract).
In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR ’90, Theories of Concurrency:
Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990,
Proceedings. Lecture Notes in Computer Science, vol. 458, pp. 278–297. Springer(1990), https://doi.org/10.1007/BFb0039066

20

K. Muroya et al.

14. van Glabbeek, R.J.: The linear time - branching time spectrum II. In: Best, E. (ed.)
CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim,
Germany, August 23-26, 1993, Proceedings. Lecture Notes in Computer Science,
vol. 715, pp. 66–81. Springer (1993), https://doi.org/10.1007/3-540-57208-2_6
15. Hughes, J., Jacobs, B.: Simulations in coalgebra. Theor. Comput. Sci. 327(1-2),
71–108 (2004), https://doi.org/10.1016/j.tcs.2004.07.022
16. Hutagalung, M.: Buffered Simulation for Büchi Automata. Ph.D. thesis, University of Kassel, Germany (2019), https://kobra.uni-kassel.de/bitstream/handle/
123456789/11329/DissertationMilkaHutagalung.pdf?sequence=7&isAllowed=y
17. Hutagalung, M., Lange, M., Lozes, É.: Buffered simulation games for büchi automata. In: Ésik, Z., Fülöp, Z. (eds.) Proceedings 14th International Conference on
Automata and Formal Languages, AFL 2014, Szeged, Hungary, May 27-29, 2014.
EPTCS, vol. 151, pp. 286–300 (2014), https://doi.org/10.4204/EPTCS.151.20
18. Johann, P., Simpson, A., Voigtländer, J.: A generic operational metatheory foralgebraic effects. In: Proceedings of the 25th Annual IEEE Symposium on Logic in
Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom. pp.
209–218. IEEE Computer Society (2010), https://doi.org/10.1109/LICS.2010.29
19. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes.
In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science(LICS ’91), Amsterdam, The Netherlands, July 15-18, 1991. pp. 266–277. IEEE
Computer Society (1991), https://doi.org/10.1109/LICS.1991.151651
20. Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic
probabilistic game semantics - playing games with automata. Formal Methods
Syst. Des. 43(2), 285–312 (2013), https://doi.org/10.1007/s10703-012-0173-1
21. Koutavas, V., Levy, P.B., Sumii, E.: From applicative to environmental bisimulation. In: Mislove, M.W., Ouaknine, J. (eds.) Twenty-seventh Conference on the
Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh,
PA, USA, May 25-28, 2011. Electronic Notes in Theoretical Computer Science,
vol. 276, pp. 215–235. Elsevier (2011), https://doi.org/10.1016/j.entcs.2011.09.023
22. Kuske, D.: Theories of orders on the set of words. RAIRO Theor. Informatics Appl.
40(1), 53–74 (2006), https://doi.org/10.1051/ita:2005039
23. Kuske, D., Zetzsche, G.: Languages ordered by the subword order. In: Bojanczyk,
M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019,
Prague, Czech Republic, April 6-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11425, pp. 348–364. Springer (2019), https://doi.org/10.1007/
978-3-030-17127-8_20
24. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput.
94(1), 1–28 (1991), https://doi.org/10.1016/0890-5401(91)90030-6
25. Morgenstern, A., Schneider, K.: A LTL fragment for GR(1)-synthesis. In: Reich, J.,
Finkbeiner, B. (eds.) Proceedings International Workshop on Interactions, Gamesand Protocols, iWIGP 2011, Saarbrücken, Germany, 27th March 2011. EPTCS,
vol. 50, pp. 33–45 (2011), https://doi.org/10.4204/EPTCS.50.3
26. Morris Jr, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1969), https://dspace.mit.edu/handle/
1721.1/64850
27. Muroya, K.: Hypernet semantics of programming languages. Ph.D. thesis, University of Birmingham, UK (2020), http://ethos.bl.uk/OrderDetails.do?uin=uk.
bl.ethos.817915

Preorder-Constrained Simulations for Program Refinement with Effects

21

28. Muscholl, A., Walukiewicz, I.: An NP-complete fragment of LTL. In: Calude, C.,
Calude, E., Dinneen, M.J. (eds.) Developments in Language Theory, 8th International Conference, DLT 2004, Auckland, New Zealand, December 13-17, 2004,
Proceedings. Lecture Notes in Computer Science, vol. 3340, pp. 334–344. Springer(2004), https://doi.org/10.1007/978-3-540-30550-7_28
29. Plotkin, G.D., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan,
M. (eds.) Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April
2-6, 2001, Proceedings. Lecture Notes in Computer Science, vol. 2030, pp. 1–24.
Springer (2001), https://doi.org/10.1007/3-540-45315-6_1
30. Pous, D.: Up-to techniques for weak bisimulation. In: Caires, L., Italiano, G.F.,
Monteiro, L., Palamidessi, C., Yung, M. (eds.) Automata, Languages and Programming, 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, July
11-15, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3580, pp. 730–
741. Springer (2005), https://doi.org/10.1007/11523468_59
31. Pous, D.: New up-to techniques for weak bisimulation. Theor. Comput. Sci. 380(12), 164–180 (2007), https://doi.org/10.1016/j.tcs.2007.02.060
32. Sangiorgi, D.: On the bisimulation proof method. Mathematical Structures in Computer Science 8(5), 447–479 (1998). https://doi.org/10.1017/S0960129598002527
33. Sangiorgi, D.: Equations, contractions, and unique solutions. ACM Trans. Comput.
Log. 18(1), 4:1–4:30 (2017), https://doi.org/10.1145/2971339
34. Sangiorgi, D., Milner, R.: The problem of "weak bisimulation up to". In: Cleaveland, R. (ed.) CONCUR ’92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings. Lecture Notes in
Computer Science, vol. 630, pp. 32–46. Springer (1992), https://doi.org/10.1007/
BFb0084781
35. Simpson, A., Voorneveld, N.F.W.: Behavioural equivalence via modalities for algebraic effects. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th
European Symposium on Programming, ESOP 2018, Held as Part of the European
Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki,
Greece, April 14-20, 2018, Proceedings. Lecture Notes in Computer Science, vol.
10801, pp. 300–326. Springer (2018), https://doi.org/10.1007/978-3-319-89884-1_
11
36. Tiuryn, J., Wand, M.: Untyped lambda-calculus with input-output. In: Kirchner,
H. (ed.) Trees in Algebra and Programming - CAAP’96, 21st International Colloquium, Linköping, Sweden, April, 22-24, 1996, Proceedings. Lecture Notes in
Computer Science, vol. 1059, pp. 317–329. Springer (1996), https://doi.org/10.
1007/3-540-61064-2_46
37. Urabe, N., Hasuo, I.: Generic forward and backward simulations III: quantitative
simulations by matrices. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy,
September 2-5, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8704,
pp. 451–466. Springer (2014), https://doi.org/10.1007/978-3-662-44584-6_31
38. Yachi, T., Sumii, E.: A sound and complete bisimulation for contextual equivalencein λ-calculus with call/cc. In: Igarashi, A. (ed.) Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23,
2016, Proceedings. Lecture Notes in Computer Science, vol. 10017, pp. 171–186(2016), https://doi.org/10.1007/978-3-319-47958-3_10

22

K. Muroya et al.
xn

x

y0
0
R yw

w

R

y0
0
R yw
x

xk

(a)
Final 1
where εQw0(b) Step ∞ (i) where a1 · · · ak Qw0

xn
y0
0
w
R yw
x
(c) Step ∞ (ii) where wQw0

Fig. 15: Conditions of Def. 7. Black parts are universally quantified, and magenta
parts are existentially quantified.

A

Completeness

It is possible to adjust the definition of preorder-constrained simulation (Def. 3)
and obtain a complete simulation notion with respect to Q-trace inclusion.
Definition 7. A binary relation R ⊆ X1 × X2 is a Q-constrained simulation( Q-simulation in short) from A1 to A2 if, for any (x, y) ∈ R, Final1 and thefollowing Step∞ hold.
aa

Step ∞ For each a1 . . . an ∈ Σ + and x1 . . . xn ∈ X1+ such that x 1 1 x1 2 1a· · · n 1 xn and xn ∈ F1 , there exist k ∈ {1, . . . , n}, w0 ∈ Σ ∗ and y 0 ∈ X2
such that (1) a1 · · · ak Qw0 ; (2) yand y 0 ∈ F2 .

w0

00
2 y ; and (3-i) xk Ry , or (3-ii) k = n

Fig. 15 illustrates the conditions of Def. 7. The condition Final 1 is an instanceof Final M (see also Fig. 6). The condition Step ∞ has two possibilities (i) and(ii), due to the clauses (3-i) and (3-ii). Note that Step ∞ is not quite a limit ofw
Step M . While the length of the sequence x
xM is restricted to M in Step M ,w
the length n of the sequence x
xn in Step ∞ can be an arbitrary positive
number. Additionally, the last state xn is required to be accepting, i.e. xn ∈ F1 .
Theorem 3 ((†) soundness and completeness). For any (x, y) ∈ X1 × X2 ,x vQ y ⇐⇒ x .Q y.
tu
We note that it is the extra clause of the definition of Q-simulations, namely(3-ii) of Step ∞ , that makes the completeness possible.
Corollary 3 (correctness of Q-simulations wrt. refinement).
1. For any t, u ∈ TΩerr , t .Q̇ u ⇐⇒ t Q
err u.
2. For any t, u ∈ TΩnd , t .Q̇∩=remu ⇐⇒ t Qnd u.
{τ }∪Ωnd

3. For any t, u ∈ TΩio , t .Q̇∩=rem{τ }u ⇐⇒ t Q
io u.

t
u

Whereas Q-counting simulation (for Q ⊆ N × N) is defined for NAs (seeDef. 2), the definition is tailored to branching-free NAs all whose accepting states
are stuck states. The NA AΩerr is an example. For these automata, preorderconstrained simulation indeed generalises counting simulation. However, the opposite does not hold.

Preorder-Constrained Simulations for Program Refinement with Effects
a

x2
a
x1
a
x

23

y1
a
y

Fig. 16: Branching-free NAs with a trivial =-simulation
˙

Proposition 5 (Q-counting simulation being Q̇-simulation). If A1 is branchingfree and all its accepting states are stuck states, then each Q-counting simulationfrom A1 to A2 is also a Q̇-simulation from A1 to A2 .
tu
Example 13 (Q̇-simulation not being Q-counting simulation). For the pair ofbranching-free NAs shown in Fig. 16, {(x, y)} is a =-simulation,
˙
because theseNAs have no accepting states. However, there exists no =-counting simulationthat includes (x, y). If such a simulation R exists, (x1 , y1 ) ∈ R must hold by
C-Step, but (x1 , y1 ) does not satisfy C-Step.
The monotonicity property satisfied by (M, Q)-simulations can be extended
to Q-simulations.
Lemma 4 ((†) monotonicity of Step). Let M ∈ N+ .
1. StepM ∧ FinalM =⇒ Step∞
Corollary 4 (monotonicity). Let M ∈ N+ . Each (M, Q)-simulation from A1
to A2 is also a Q-simulation from A1 to A2 .
t
u
M,N,Q
Notably, we do not need to modify the definition of two-player games GA;
1 ,A2
we can simply set M = N = ∞ to achieve games that correspond with Qsimulations. We can extend the spectrum in Fig. 12 and obtain a generative
spectrum shown in Fig. 17.

Lemma 5 (monotonicity). Let M, N ∈ N+ . If Simulator is winning from a
M,N,Q
∞,∞,Q
state (w, x, y) in GA, Simulator is also winning from the state in GA
.
1 ,A2
1 ,A2
t
u
Proposition 6 (correctness). Simulator is winning from a state (ε, x, y) in∞,∞,QGA, if and only if x .Q y.
t
u
1 ,A2

B

Connection to Logical Implication

We briefly investigate the relationship between Q-trace inclusion and logics,
namely fragments of the linear temporal logic (LTL), aiming at a potential application to model checking.

24

K. Muroya et al.
.1,Q −→ .2,Q −→ · · · −→
l

l

.Q

←→ Q-trace inclusion vQ

l

1,∞,Q
2,∞,Q
∞,∞,Q
GA
−→ GA
−→ · · · −→ GA
1 ,A2
1 ,A2
1 ,A2

↑
..
.
↑

↑
..
.
↑

↑
..
.
↑

∞,2,Q
2,2,Q
1,2,Q
−→ · · · −→ GA
−→ GA
GA
1 ,A2
1 ,A2
1 ,A2

↑

↑

↑

∞,1,Q
2,1,Q
1,1,Q
−→ · · · −→ GA
−→ GA
GA
1 ,A2
1 ,A2
1 ,A2

M,N,Q
Fig. 17: A generative spectrum of games GA
and similarities .M,Q , .Q
1 ,A2

Definition 8 (LTL, see e.g. [6]). A linear temporal logic formula (LTL formula) over a set AP is given by the following BNF notation where p ∈ AP.
ϕ ::= true | false | p | ¬p | ϕ ∨ ϕ | ϕ ∧ ϕ | X ϕ | ϕ U ϕ | ϕ R ϕ(1)

The semantics of an LTL formula ϕ is usually defined as a subset JϕK ⊆(2AP )ω of infinite words over 2AP . We use its finitary variant here, as we arefocusing on finite traces.
Definition 9 (LTL semantics on finite traces, cf. [11]). For an LTL formula ϕ, we inductively define JϕKfin ⊆ (2AP )∗ as follows:– JfalseKfin := ∅– JtrueKfin := (2AP )∗– J¬pKfin := {a1 . . . an | n > 0, p ∈/ a1 }– JpKfin := {a1 . . . an | n > 0, p ∈ a1 }– Jϕ1 ∧ ϕ2 Kfin := Jϕ1 Kfin ∩ Jϕ2 Kfin
– Jϕ1 ∨ ϕ2 Kfin := Jϕ1 Kfin ∪ Jϕ2 Kfin
– JX ϕKfin := {a1 . (. . an | n > 0, a2 . . . an ∈ JϕKfin }!)(∀j < i. aj . . . an ∈ Jϕ1 Kfin )– Jϕ1 U ϕ2 Kfin := a1 . . . an ∃i ∈ {1, . . . , n}.
∧ ai . . . an ∈ Jϕ2 Kfin(!)(∃j < i. aj . . . an ∈ Jϕ1 Kfin )– Jϕ1 R ϕ2 Kfin := a1 . . . an ∀i ∈ {1, . . . , n}.
∨ ai . . . an ∈ Jϕ2 Kfin
AP
Let A = (X, Σ, , F ) be a (2 )-labelled NA. For x ∈ X, we write x |=fin ϕwhen L∗ (x) ⊆ JϕKfin . We also use the following syntactic sugar: F ϕ := true U ϕand G ϕ := false R ϕ.
For a state x of an NA A, we write x |=fin ϕ when L∗A (x) ⊆ JϕKfin . Then finite
trace inclusion L∗A1 (x) ⊆ L∗A2 (y) implies y |=fin ϕ =⇒ x |=fin ϕ for each LTL
formula ϕ. If we replace L∗A1 (x) ⊆ L∗A2 (y) with x vQ y, what happens to ϕ? Weattempt to answer this question, using preorders from Ex. 5 and fragments of
LTL found in the literature [28,25,7].
The ⊆∗ -trace inclusion implies implication of a fragment of LTL “without”
negation.

Preorder-Constrained Simulations for Program Refinement with Effects

25

Proposition 7. If x v⊆∗ y then y |=fin ϕ =⇒ x |=fin ϕ for each ϕ given by:
ϕ ::= true | false | ¬p | ϕ ∨ ϕ | ϕ ∧ ϕ | X ϕ | ϕ U ϕ | ϕ R ϕ .

(2)

We can consider the dual. If we replace ⊆∗ with its inverse ⊇∗ , then ¬p in(2) becomes p. This fragment is known as a positive fragment (LTL+ ) [9].
Next, the ⊆sub -trace inclusion implies implication of safety properties guarded
by G.
Proposition 8. If x v⊆sub y then y |=fin ϕ ⇒ x |=fin ϕ for each ϕ given by:
ϕ ::= true | false | ϕ ∨ ϕ | ϕ ∧ ϕ | G ψ ,ψ ::= p | ¬p | ψ ∨ ψ | ψ ∧ ψ | ϕ . (3)We can again consider the dual. Let ⊇sup be the superstring relation defined
defby w ⊇sup w0 ⇔ w0 ⊆sub w. Then ⊇sup -trace inclusion implies implication of
liveness properties guarded by F: namely, G ψ in Prop. 8 is replaced by F ψ.
Finally, we can combine Ex. 5(4) with Ex. 5(5), and define Q so that
a1 . . . ak Qa01 . . . a0k0 means k ≤ k 0 and existence of j1 < · · · < jk such thatai ⊆ a0ji for each i ∈ {1, . . . , k}. Then Q-trace inclusion implies implication of
ϕ’s which are given by removing p from (3).

C

Omitted Proofs

C.1

Proof of Prop. 1

Proof. This is a consequence of Cor. 3 and Prop. 5.
C.2

Proof of Prop. 5

Proof. Let R ⊆ X1 × X2 be a Q-counting simulation, and take an arbitrary pair(x, y) ∈ R. When x ∈ F1 , because the pair satisfies C-Final , y ∈ F1 follows.
Therefore (x, y) ∈ R also satisfies Final 1 .
When (x, y) ∈ R satisfies C-Step, let a1 · · · an ∈ Σ + and x1 · · · xn ∈ X1+aaasatisfy x 1 1 x1 2 1 · · · n 1 xn and xn ∈ F1 . There are two possibilities.
– When the condition (1) holds, there exist x00 ∈ X1 and w ∈ Σ ∗ such thatw
x1 1 x00 6 1 and x00 6∈ F1 . Because A1 is branching-free and its accepting
states are stuck states, xn 6 1 and xn = x00 must hold. We have xn ∈ F1
and x00 6∈ F1 , which is contradiction.
– When the condition (2) holds, there exist x00 ∈ X1 , y 0 ∈ X2 and w, w0 ∈
w

w0

00
0
0
00
0
Σ ∗ , such that x1
1 x , y2 y , |a1 w|Q|w |, and x Ry . Because A1 isbranching-free and its accepting states are stuck states, xn 6 1 holds andthere exists k ∈ {1, . . . , n} such that x00 = xk and w = a2 · · · ak . Therefore,
the conditions (1), (2) and (3-i) of Step ∞ holds.

26

K. Muroya et al.

C.3

Proof of Prop. 2

Proof. The proof is straightforward by definitions (i.e. Def. 1 and Def. 4).
C.4

Proof of Prop. 7

Proof. It suffices to prove the following:∀ϕ : generated by the BNF in Prop. 7. ∀w ∈ Σ ∗ . ∀w0 ∈ Σ ∗ .
w ⊆∗ w0 ∧ w0 ∈ JϕKfin =⇒ w ∈ JϕKfin . (4)We prove it by the induction on the structure of ϕ. Without loss of generality,
we can assume |w| = |w0 |. Let w = a1 , . . . , an and w0 = a01 . . . a0n .

(When ϕ = tt) We always have a1 . . . an ∈ JϕKfin .
(When ϕ = ff) It contradicts to a01 . . . a0n ∈ JϕKfin .
(When ϕ = ¬p) As p ∈/ a01 , we have p ∈/ a1 .
(When ϕ = ϕ1 ∨ ϕ2 ) By a01 . . . a0n ∈ Jϕ1 Kfin ∪ Jϕ2 Kfin and the induction hypothesis, we have a1 . . . an ∈ Jϕ1 Kfin ∪ Jϕ2 Kfin .
(When ϕ = ϕ1 ∧ ϕ2 ) Similar to the above.
(When ϕ = X ϕ0 ) By a02 . . . a0n ∈ Jϕ0 K and the induction hypothesis, we havea2 . . . an ∈ Jϕ0 K .
(When ϕ = ϕ1 U ϕ2 ) By ∃i ∈ {1, . . . , n}. ∀j < i. a0j . . . a0n ∈ Jϕ1 Kfin and a0i . . . a0n ∈Jϕ2 Kfin and the induction hypothesis, we have ∃i ∈ {1, . . . , n}. ∀j < i. aj . . . an ∈Jϕ1 Kfin and ai . . . an ∈ Jϕ2 Kfin .
(When ϕ = ϕ1 R ϕ2 ) Similar to the above.
C.5

Proof of Prop. 8

Proof. It suffices to prove the following two.
∀ϕ : generated by the BNF in Prop. 8.
∀w = a1 . . . an ∈ Σ ∗ . ∀w0 = a01 . . . a0n0 ∈ Σ ∗ .
w ⊆sub w0 ∧ w0 ∈ JϕKfin =⇒ w ∈ JϕKfin(5)∀ψ : generated by the BNF in Prop. 8.
∀w = a1 . . . an ∈ Σ + . ∀w0 = a01 . . . a0n0 ∈ Σ + .
w ⊆sub w0 ∧ w0 ∈ JϕKfin ∧ a1 = a01 =⇒ w ∈ JϕKfin(6)

We prove it by the mutual induction on the structures of ϕ and ψ.

(When ϕ = tt, ff, ϕ1 ∨ ϕ2 or ϕ1 ∧ ϕ2 ) Similar to the proof of Prop. 7.
(When ϕ = G ψ) In this case, we have a0i . . . a0n0 ∈ JψKfin for each i ∈ {1, . . . , n0 }.
By a1 . . . an ⊆sub a01 . . . a0n0 and the induction hypothesis, we have aj . . . an ∈JψKfin for each j ∈ {1, . . . , n}.
(When ψ = p or ¬p) Immediate by a1 = a01 .
(When ψ = ψ1 ∨ ψ2 or ψ1 ∧ ψ2 ) Similar to the proof of Prop. 7.
(When ψ = ϕ) Immediate.

Preorder-Constrained Simulations for Program Refinement with Effects

C.6

27

Proof of Lem. 3

Proof. The parameters M and N constrain Simulator’s moves only. The bigger
M or N is, the more moves Simulator can make, and hence the more positions
Simulator can be winning from.
C.7

Proof of Prop. 3

Proof. We first prove the ⇐= direction, i.e. the “if” part, assuming the existence of an (M, Q)-simulation R such that xRy. We fix Simulator’s strategy sothat Simulator chooses 4 and moves to (ε, x0 , y 0 ) if that is possible and x0 Ry 0 ,and chooses 3 or 5 otherwise. For an arbitrary strategy of Challenger, ourgoal is to show that Simulator is winning from (ε, x, y). Specifically, we prove
the following (?): from each position (ε, x0 , y0 ) such that x0 Ry0 , either anotherposition (ε, x00 , y00 ) such that x00 Ry00 is reachable or Simulator wins.
M,∞,Q
We let the players play the game GAfrom (ε, x0 , y0 ), and pause the play
1 ,A2
when Challenger makes a move 2 or Simulator makes a move 4 .
– If the play never ceases, Challenger keeps choosing 1 and Simulator only
chooses 3 .
• If Challenger gets stuck before making M moves, Simulator wins theplay.
• Otherwise, Challenger can make M moves of 1 . After the M movesof Challenger, the position is necessarily (a1 · · · aM , xM , y0 ) such thata1 ···aMx0
1 xM , since Simulator has only chosen 3 . Because R is an(M, Q)-simulation, by Step M , there exist k ∈ {1, . . . , M }, w0 ∈ Σ ∗ and
a1 ···ak

ak+1 ···aM

0y00 ∈ X2 such that a1 · · · ak Qw0 , x0
1 xk
1 xM , and xk Ry0 .
∗ If k < M , Simulator should have chosen 4 after the k-th move ofChallenger, according to the strategy. This leads to a contradiction.
∗ Otherwise, k = M . This means that after the M -th move of Challenger, Simulator can (and has to, according to the strategy) choose
4 . This also leads to a contradiction.
– If the play ceases with Challenger choosing 2 , after the first choice of 2 ,w
0
we are at a position (X, w, x00 , y0 ) such that x0
1 x0 ∈ F1 and |w| < M .
We have |w| < M because Simulator has only made moves 3 , if any. Since
R is an (M, Q)-simulation, by Final M , there exist w0 ∈ Σ ∗ and y00 ∈ X2
w0such that wQw0 and y0 2 y00 ∈ F2 . Therefore Simulator can choose 5 andwin.
– If the play ceases with Simulator choosing 4 , the first choice of 4 changes
a position (w, x00 , y0 ) to (ε, x00 , y00 ) for some y00 ∈ X2 such that x00 Ry00 .
As a result, (?) holds. Consequently, from (ε, x, y), Simulator can either win or
infinitely continue a play (and win).
We next prove the =⇒ direction, i.e. the “only if” part, assuming that
Simulator is winning from the position (ε, x, y). We define R ⊆ X1 × X2 by
R := {(x0 , y 0 ) | Simulator is winning from (ε, x0 , y 0 )}. It holds that xRy. For an
arbitrary pair (x0 , y 0 ) ∈ R, we prove that it satisfies Final M and Step M .

28

K. Muroya et al.
w

Final M We assume a sequence x0 1 x00 ∈ F1 such that |w| < M .
– If |w| = 0, we have x0 = x00 ∈ F1 . From a position (ε, x0 , y 0 ), we let
Challenger choose 2 and move to (X, ε, x0 , y 0 ). Simulator is necessarily winning from this position, and hence Simulator can choose 5 at(X, ε, x0 , y 0 ). This means that there exist w0 ∈ Σ ∗ and y 00 ∈ X2 suchw0

that y 0 2 y 00 ∈ F2 and εQw0 . Therefore (x0 , y 0 ) satisfies Final M .
– Otherwise, i.e. if |w| > 0, from a position (ε, x0 , y 0 ), we let Challengerw
00
choose 1 for |w| times along x0
1 x and then choose 2 . Because
0 0Simulator is winning from (ε, x , y ), Simulator has a winning strategy
for the |w| + 1 moves of Challenger.
• If the first |w| moves of Simulator according to the strategy are 3 , after Challenger’s |w|+1 moves, we are at a position (X, w, x00 , y 0 ). Simulator is winning from (ε, x0 , y 0 ) and necessarily from (X, w, x00 , y 0 ).
Therefore, the strategy must let Simulator choose 5 at the position(X, w, x00 , y 0 ).
• Otherwise, i.e. if the first |w| moves of Simulator according to thestrategy are 3 interleaved with 4 , after Challenger’s |w| + 1 moves,
we are at a position (X, w2 , x00 , y 00 ) for some w2 ∈ Σ ∗ and y 00 ∈ X2
w1 w2
00
such that: there exist w1 , w00 ∈ Σ ∗ such that x0
1
1 x ∈ F1 ,
w00

00
00
y0
2 y and w1 Qw . Simulator is necessarily winning from the
00 00
position (X, w2 , x , y ). Therefore, the strategy must let Simulator
choose 5 at this position.
As a result, (x0 , y 0 ) satisfies Final M . Note that Q is closed under concatenation.
a1 ···aM
Step M We assume a sequence x0
1 xM . We let Challenger choose 1 for M
times. Because Simulator is winning from (ε, x0 , y 0 ), Simulator has a winning
strategy for the M moves of Challenger.
– If Simulator’s first move is 4 , the move changes a position (a1 , x1 , y 0 )to (ε, x1 , y 00 ) for some x1 ∈ X1 and y 00 ∈ X2 . Simulator must be winningfrom the position (ε, x1 , y 00 ), which means x1 Ry 00 .
– Otherwise, i.e. if the first 0 < k < M moves of Simulator are 3 and Simulator’s next move is 4 according to the strategy, the move 4 changes
a position (a1 · · · ak , xk , y 0 ) to (ε, xk , y 00 ) for some xk ∈ X1 and y 00 ∈ X2 .
w0

There exists w0 ∈ Σ ∗ and we have a1 · · · ak Qw0 and y 0 2 y 00 . Simulator
must be winning from the position (ε, xk , y 00 ), which means xk Ry 00 .
As a result, (x0 , y 0 ) satisfies Step M .
Consequently, R is an (M, Q)-simulation.
C.8

Proof of Prop. 6

Proof. We first prove the ⇐= direction, i.e. the “if” part, assuming the existenceof a Q-simulation R such that xRy. We fix Simulator’s strategy so that Simulator
chooses 4 and moves to (ε, x0 , y 0 ) if that is possible and x0 Ry 0 , and chooses 3
or 5 otherwise. For an arbitrary strategy of Challenger, our goal is to show that

Preorder-Constrained Simulations for Program Refinement with Effects

29

Simulator is winning from (ε, x, y). Specifically, we prove the following (?): fromeach position (ε, x0 , y0 ) such that x0 Ry0 , either another position (ε, x00 , y00 ) suchthat x00 Ry00 is reachable or Simulator wins.
∞,∞,Q
We let the players play the game GAfrom (ε, x0 , y0 ), and pause the play
1 ,A2
when Challenger makes a move 2 or Simulator makes a move 4 .
– If the play never ceases, Challenger keeps choosing 1 and Simulator only
chooses 3 .
• If Challenger gets stuck, Simulator wins the play.
• Otherwise, Simulator can win the infinite play by keep choosing 3 .
– If the play ceases with Challenger choosing 2 , after the first choice of 2 ,w
we are at a position (X, w, x00 , y0 ) such that x0 1 x00 ∈ F1 .
• If |w| = 0, i.e. w = ε, we have x0 = x00 ∈ F1 . By Final 1 , there exist
w00
w0 ∈ Σ ∗ and y00 ∈ X2 such that εQw0 and y0
2 y0 ∈ F2 . This meansthat Simulator can choose 5 and win.
• Otherwise, |w| > 0. Because Simulator has only chosen 3 , by Step ∞ ,w00
there exist w0 ∈ Σ ∗ and y00 ∈ X2 such that wQw0 and y0
2 y0 ∈ F2 .
This means that Simulator can choose 5 and win.
– If the play ceases with Simulator choosing 4 , the first choice of 4 changes
a position (w, x00 , y0 ) to (ε, x00 , y00 ) for some y00 ∈ X2 such that x00 Ry00 .

As a result, (?) holds. Consequently, from (ε, x, y), Simulator can either win or
infinitely continue a play (and win).
We next prove the =⇒ direction, i.e. the “only if” part, assuming that
Simulator is winning from the position (ε, x, y). We define R ⊆ X1 × X2 by
R := {(x0 , y 0 ) | Simulator is winning from (ε, x0 , y 0 )}. It holds that xRy. For an
arbitrary pair (x0 , y 0 ) ∈ R, we prove that it satisfies Final 1 and Step ∞ .
Final 1 We assume that x0 ∈ F1 . From a position (ε, x0 , y 0 ), we let Challenger
choose 2 and move to (X, ε, x0 , y 0 ). Simulator is necessarily winning fromthis position, and hence Simulator can choose 5 at (X, ε, x0 , y 0 ). This means
w000
0that there exist w0 ∈ Σ ∗ and y 00 ∈ X2 such that y 0
2 y ∈ F2 and εQw .
1
0 0
Therefore (x , y ) satisfies Final .
a1 ···an
Step ∞ We assume a sequence x0
1 xn ∈ F1 . We let Challenger choose 1
for n times, and then choose 2 , moving to a position (X, a1 · · · an , xn , y 0 ).
Simulator must be winning from this position, which means that Simulator
can choose 5 . This means that there exist y 00 ∈ F2 and w0 ∈ Σ ∗ such that

a1 · · · an Qw0 and y 0

w0

2 y

00

. Therefore (x0 , y 0 ) satisfies Step ∞ .

Consequently, R is a Q-simulation.