History-Dependent Nominal µ-Calculus
Clovis Eberhart∗

Bartek Klin†

National Institute of Informatics
Tokyo, Japan

University of Warsaw

Abstract—The µ-calculus with atoms, or nominal µ-calculus,
is a temporal logic for reasoning about transition systems that
operate on data atoms coming from an infinite domain andcomparable only for equality. It is, however, not expressive
enough to define some properties that are of interest from theperspective of system verification. To rectify this, we extend thecalculus with tests for atom freshness with respect to the global
history of transitions. Since global histories can grow arbitrarily
large, it is not clear whether model checking for the extended
calculus is decidable. We prove that it is, by showing that one
can restrict attention only to locally relevant parts of the history.

I. I NTRODUCTION
Formal verification of infinite-state systems is a rich andactive field of study. Sources of infinity are numerous anddiverse: one may consider systems with unbounded counters,
stacks or FIFO channels, timed systems with unboundedclocks, systems whose states are generated by regular or pushdown processes, and so on. In each of these settings, formal
verification relies on methods for symbolic representation of
infinite models by finite means. One may then decide whether
systems thus represented satisfy desirable properties, in theprocess of model checking. The properties involved are often
expressed in suitable versions of temporal logics such as themodal µ-calculus [1] or its fragments CTL∗ [2] and LTL.
In this paper we focus on systems where the source of
infinity is an infinite domain of data values that can only
be compared for equality. In practical systems such data
values may appear, e.g., as randomly generated passwords,
unique process identifiers in distributed algorithms, or noncesin cryptographic protocols. A typical property that one mightwant to verify about a system with access to a black-box
password generator is: a computation path where generated
passwords are all different will never reach a bad state.
Several approaches to defining and checking properties ofmodels equipped with data values have been considered. For
example, in [3, 4, 5, 6] the linear time temporal logic LTL
was extended with a freeze quantifier that can store a currently
observed data value for future reference. This can be used todetect repetitions of data values, a goal followed also in [7, 8].
Another idea is to extend a temporal logic with the ability
to express constraints about locally observed data values, as∗ Supported by ERATO HASUO Metamathematics for Systems Design
Project (No. JPMJER1603), JST.
† Supported by the European Research Council (ERC) under the European
Unions Horizon 2020 research and innovation programme (ERC consolidator
grant LIPA, agreement no. 683080).

in [9, 10]. Temporal logics are closely connected to automata,and extending them with data values amounts to consideringso-called register automata. In particular, the modal µ-calculus
corresponds to alternating tree automata, and a register versionof those were studied in [11, 12].
In all these works, the authors take care to ensure that
their logics have a decidable satisfiability problem (does agiven formula have a model?). To this end, they impose
subtle conditions on their formalisms and inevitably limit theirexpressivity to some degree. If one gives up on decidable
satisfiability, the data-equipped logic can get much more
expressive. An example is the first-order µ-calculus of [13, 14],which features constraints over data values from arbitrary infinite domains. There even the model-checking problem (doesa given model satisfy a given formula?) becomes undecidable,
and incomplete proof procedures are the main focus.
This paper is a continuation of [15], where an atomic µcalculus was proposed. Its design relies on the framework ofsets with atoms, also known as nominal sets [16, 17], wheredata atoms from an infinite set A, with their inherent symmetry, are built already into set-theoretic foundations. Originallyintended as an algebraic approach to name binding, sets withatoms have found applications in language and computation
theory, with notions such as nominal automata [18] and Turingmachines with atoms [19] providing insights into propertiesof computing devices over infinite alphabets. A key featureof this approach is a relaxed notion of finiteness, called orbitfiniteness. Orbit-finite structures, although usually infinite, canbe symbolically presented by finite means and are amenable
to algorithmic manipulation.
The atomic µ-calculus of [15] extends the classical calculus with orbit-finite (instead of just finite) disjunctions andconjunctions. It can express properties of Kripke models(alternatively, labeled transition systems) equipped with data
values, with formulas such as⋁ (a ∧ ◇µX.(a ∨ ◇X))a∈A

meaning: some data atom that appears in the present state,appears again on some future path. Its satisfiability problem
is undecidable, but model checking on orbit-finite models
remains decidable, so the calculus is potentially applicable tothe verification of systems that manipulate data atoms.
However, the calculus of [15] is not expressive enough to
be useful in practice. In fact, one of the main results of that
paper was the non-obvious fact that the calculus cannot express

a property called #PATH: there exists an infinite path where nodata atom appears more than once. As a consequence, many
practically motivated properties such as the one regarding
password generators mentioned above, are also undefinable.
#PATH is decidable on orbit-finite models, which makes its
undefinability all the more disappointing. It is easy to define itin an extension of CTL∗ with atoms (which is not a fragmentof the µ-calculus with atoms), but model checking of that
logic is undecidable. The challenge of finding a syntacticallyeconomic extension of the µ-calculus with atoms that could
express #PATH while retaining the decidability of model
checking, was the main open problem left in [15].
Our main contribution is a solution to that problem. We
extend the µ-calculus from [15] with simple tests of the form♯a (read “fresh a”), saying that an atom a has never appeared
before in any basic predicate that held on the computation
path that led to the present state. In a sense, ♯ is an extremely
limited past-time modality. Similar freshness conditions havebeen considered before for automata over finite words [20], inthe general framework of the aptly named history-dependent
automata [21]. With this extension, #PATH is easily definable,
as well as many other properties of potential practical interest.
As examples, we present a simple system with a passwordprotected critical section, and the cryptographic Needham–
Schroeder protocol [22] that relies on generating uniquenonces.
In the extended calculus, formulas are interpreted in thecontext of global histories, i.e., sets of atoms that haveappeared in the past. Such histories can grow arbitrarily
large, and so it becomes unclear whether model checking forthe extended calculus remains decidable. Our main technicalresult (Theorem 10) is that it does. The proof relies on theobservation that, since the behavior of each state in an orbitfinite system only depends on a fixed set of atoms, only alimited part of the global history is relevant at any given state
and the rest of the history may be conveniently forgotten andlater reinvented as needed.
The structure of the paper is as follows. In Sec. II, we recall
the classical modal µ-calculus, followed by an introduction tosets with atoms in Sec. III. In Sec. IV, we recall the basicsof the calculus from [15], and in Sec. V we extend it to thehistory-dependent µ-calculus. After showing two examples inSec. VI, in Sec. VII we prove that model checking is decidable.
We conclude in Sec. VIII with a brief discussion of the mostpressing directions for future work.
Acknowledgment. We are grateful to Grzegorz Fabiański for
spotting a significant mistake in an earlier version of this paper,and to anonymous reviewers for pointing out some relevant
related work.

In the last clause above, the least fixpoint is taken for afunction on the complete lattice of subsets of K orderedby set inclusion. Thanks to the positivity assumption on ϕ,this function is monotone, and therefore by Tarski’s fixpoint
theorem it does have a least fixpoint. It can be approximatedfrom below by a transfinite sequence

II. M ODAL µ- CALCULUS

Ψ0 ⊆ Ψ1 ⊆ Ψ2 ⊆ ⋯ ⊆ Ψω ⊆ Ψω+1 ⊆ ⋯ ⊆ K

We shall only need basic notions of the syntax and semantics of the modal µ-calculus; any of the texts [23, 24, 25, 26,
27] contains this and much more material. Everything in thissection is completely standard, and we recall it only to fix thenotation and to prepare the ground for further sections.

Fix a set B of basic predicates and a set X of variables.
The set of µ-calculus formulas is generated by the grammar
ϕ ∶∶= ⊺ ∣ p ∣ ¬ϕ ∣ ϕ ∨ ϕ ∣ ◇ϕ ∣ X ∣ µX.ϕ

(1)

where p ranges over B and X over X. The set FV(ϕ) ⊆ X of
free variables in a formula ϕ is defined in the usual way, withthe constructor µX.ϕ binding X in ϕ. A formula is closed if
it does not have free variables.
It is standard to write, as syntactic sugar: = ¬⊺,ϕ ∧ ψ = ¬(¬ϕ ∨ ¬ψ),ϕ → ψ = ¬ϕ ∨ ψ,

νX.ϕ = ¬µX.¬ϕ[X ↦ ¬X].

◻ϕ = ¬ ◇ (¬ϕ),

A formula is considered legal only if it is positive, i.e., if
in every subformula µX.ϕ the variable X occurs freely in ϕonly under an even number of nested negations.
Formulas are interpreted in Kripke models of the form
K = (K, Ð→, ⊧)where K is a set of states, Ð→ ⊆ K × K is the transition
relation and ⊧ ⊆ K × B is the satisfaction relation for basic
predicates. For a state x ∈ K, we denotepred(x) = {p ∈ B ∣ x ⊧ p}.
A model is finite if it has finitely many states and if pred(x)is finite for every state x.
The semantics of a formula ϕ in a model K is defined fora context ξ, which is a finite partial functionξ ∶ X ⇀ PK
which is defined at least on all the free variables in ϕ. Then,for any formula ϕ, the set JϕKξ ⊆ K is defined inductively:
for all x ∈ K

x ∈ J⊺Kξx ∈ JpKξ ⇐⇒ p ∈ pred(x)x ∈ J¬ϕKξ ⇐⇒ x ∈/ JϕKξx ∈ Jϕ ∨ ψKξ ⇐⇒ x ∈ JϕKξ or x ∈ JψKξ(2)x ∈ J◇ϕKξ ⇐⇒ ∃y ∈ JϕKξ s.t. x Ð→ yx ∈ JXKξ ⇐⇒ x ∈ ξ(X)JµX.ϕKξ=

lfp (Ψ ↦ JϕKξ[X↦Ψ] ) .

defined byΨα+1 = JϕKξ[X↦Ψα ]Ψβ = ⋃ Ψα
α<βfor a limit ordinal β(3)(in particular Ψ0 = ∅). For any K this sequence eventuallystabilizes at the desired least fixpoint.
Example 1. Let B = {m, d}, where m stands for “mistake”,
and d for “disaster”. The formulaµX.(d ∨ ◇X)
holds in a state x ∈ K iff some state where d holds is reachable
from x by a sequence of transitions. Put into words, it saysthat a disaster is possible on some future path. Its negation:
νX.(¬d ∧ ◻X)
says that a disaster cannot be reached, and the formulaνX.((m → µY.(d ∨ ◻Y )) ∧ ◻X)
means that every future mistake will inevitably lead to adisaster.
If the model K is finite, then for every fixpoint formula, thecorresponding sequence of approximants (3) stabilizes after afinite number of steps. This means that the inductive definition (2) actually provides an effective procedure to computethe interpretation of a formula in a finite model. It is easy to seethat this computation can be performed in space polynomial in
the size of ϕ and K, which gives a polynomial space algorithm
for the following model checking problem:
Given a closed formula ϕ and a state x in a finite
model K, does x ∈ JϕK∅ ?
This algorithm is rather naive. More sophisticated procedures
rely on a correspondence between µ-formulas and parity
games (see, e.g., [27]), where recent breakthroughs [28]achieved quasi-polynomial time solutions to the modelchecking problem.
III. S ETS WITH ATOMS
There are several, essentially equivalent ways to introduce
sets with atoms, also known as nominal sets [16]. We follow
the set-theoretic presentation of [17], culminating in the notionof orbit-finite sets [16, 18] and computable operations on them.
Fix a countably infinite set A, whose elements we shall callatoms. A bijection on A will be called an atom automorphism,
and the group of atom automorphisms is denoted Aut(A).1
A set with atoms is a set that can have atoms, or other setswith atoms, as elements. Formally, the universe UA of setswith atoms is defined by a von Neumann-like hierarchy, bytransfinite induction on ordinal numbers α:
UA
0 = ∅,AUA
α+1 = P(Uα ) + A,AUA
β = ⋃ Uα ,α<βfor β a limit ordinal; here + denotes the disjoint union of sets.
There is a group action of atom automorphisms on UA :_ ⋅ _ ∶ UA × Aut(A) → UA ;1 An alternative definition, taken in [16, 17], is to let Aut(A) be the groupof all finite bijections, i.e., those that fix almost all a ∈ A. This distinction
does not make any difference for our purposes here.

an automorphism acts on a set by consistently renaming all
atoms in it. Formally, this is defined by transfinite induction.
For a finite set S ⊆ A, let AutS (A) be the group of those
automorphisms of A that fix every element of S. We say thatS supports a set X if X ⋅ π = X for every π ∈ AutS (A). It
should be clear that every set X is supported by the set of
all atoms that appear in it, i.e., are elements of X or appear
in some elements of it. But the notion of support is more
subtle than that: for example, for any atoms a, b, c ∈ A, theset A ∖ {a, b, c} is supported by {a, b, c}. The intuition is thata set X is supported by S if it can be defined in a way that
does not mention any specific atoms other than those in S.
A set with atoms is considered legal only if it is hereditarily
finitely supported, i.e., if it has a finite support, its every
element has some (perhaps different) finite support and so on.
We shall only consider sets with this property.
If X has a finite support then it has the least finite support(see [16] for a proof), denoted supp(X). A set is equivariant
if supp(X) = ∅.
Relations and functions are sets in the usual sense, so thenotions of support and equivariance applies to them as well.
Unfolding the definitions, for equivariant sets X and Y , a
relation R ⊆ X × Y is equivariant if (x, y) ∈ R implies (x ⋅π, y ⋅ π) ∈ R and a function f ∶ X → Y is equivariant if
f (x ⋅ π) = f (x) ⋅ π, for every π ∈ Aut(A). The intuition isthat a relation or function is equivariant if it can be definedin a way that only relies on comparing atoms for equality, but
without mentioning any specific atoms.
For any x with atoms, the S-orbit of x is the set{x ⋅ π ∣ π ∈ AutS (A)}.
For example, if S supports x then the S-orbit of x is the
singleton {x}.
For any S, S-orbits form a partition of the universe UA .
Moreover, for any S-supported set X, the S-orbits of its
elements form a partition of X. Then X is S-orbit-finite if
it is a union of finitely many S-orbits. Then, for any finite
T ⊇ S, X is also T -orbit-finite. Thanks to this observation, we
may drop the qualifier and simply call X orbit-finite, meaning“S-orbit-finite for any/every S that supports X”.
Example 2.
● Any classical set (without atoms) is anequivariant set with atoms. Its every element forms its
own orbit, so such a set is orbit-finite iff it is finite.
● An atom a ∈ A has no elements, and it is supported by{a}. A subset of A is finitely supported iff it is finite or
co-finite; a finite set is supported by itself, and a co-finite
one by its complement.
A● The set A of atoms, the set ( ) of two-element sets of2
2
atoms, and the set A of ordered pairs of atoms, areequivariant sets. The first two have a single orbit each,and the last one has two equivariant orbits:
A2 = {(a, a) ∣ a ∈ A} ∪ {(a, b) ∣ a ≠ b ∈ A}.

(4)

Similarly, An is orbit-finite for every n ∈ N, with thenumber of orbits equal to the n’th Bell number. The setA∗ of finite sequences of atoms is not orbit-finite.

The powerset P(A) is equivariant itself, but it contains
elements that are not finitely supported, so it is notconsidered a legal set with atoms. For any legal set withatoms X, the set Pfs (X) of all finitely supported subsets
of X and the smaller set Pfin (X) of all finite subsets ofX, are both legal and supported by supp(X). Both ofthem may fail to be orbit-finite even if X is orbit-finite.
● There are four equivariant binary relations on A: theempty relation, equality, inequality and the full relation.
A● There is no equivariant function from ( ) to A, but
2●{({a, b}, a) ∣ a ≠ b ∈ A}

(5)

is a legal equivariant relation, and the function constantat a is supported by {a}. The only equivariant function
from A to A is the identity. The only equivariant functions
from A2 to A are projections, and the only equivariant
function from A to A2 is the diagonal a ↦ (a, a).
Example 3. The following Kripke model represents a FIFO
buffer of size 3 that can input and output atoms. The set ofstates is K = A3 . The transition relation is:(a, b, c) Ð→ (d, e, f )⇐⇒e = a, f = b.

Let the set of basic predicates be
B = {ina ∣ a ∈ A} ∪ {outa ∣ a ∈ A}

(6)

interpreted by a satisfaction relation ⊧ such that:pred(a, b, c) = {ina , outc }.
This is an equivariant Kripke model with atoms, with five
orbits of states and two orbits of basic predicates. For every
atom a ∈ A, every state in K satisfies the µ-formulaνX.((ina → ◻◻outa ) ∧ ◻X),

(7)

meaning that whenever a is input to the buffer, it will be output
exactly two steps later.
It is easy to check that, for any X and Y with atoms,
supp(X, Y ) = supp(X) ∪ supp(Y )and, for any function f ∶ X → Y and x ∈ X,
supp(f (x)) ⊆ supp(f, x).
The cartesian product of two orbit-finite sets is orbit-finite,
and a finitely supported subset of an orbit-finite set is orbitfinite. As a result, any finitely supported relation or function
between orbit-finite sets, considered as a set of pairs, is orbitfinite. Furthermore, for any finite S ⊆ A and any orbit-finite X
and Y supported by S, the set of S-supported functions fromX to Y is finite. This is because for a fixed S, an orbit-finite
set can have only finitely many S-supported subsets.
Orbit-finite sets, although usually infinite, can be presented
by finite means and are therefore amenable to algorithmic
manipulation. There are a few ways to do this. One way, usedin [19], is to present orbit-finite sets by formal set-builder
expressions of the form{e ∣ v1 , . . . , vn ∈ A, ϕ}
where e is again an expression, vi are bound atom variablesand ϕ is a first-order formula with equality. We refer to [19]for a precise formulation (and to [29] for a proof that allorbit-finite sets can be presented this way); suffice it to say
that, after adding some mild syntactic sugar, expressions suchas (4), (5), or (6) above are of this form. The set defined bysuch an expression is supported by the atoms that appear freely
in the expression.
Under the set-builder representation it is not trivial to check
whether two representations define the same set. (Indeed, it isa P SPACE-complete problem, as that is the complexity of thefirst-order theory of equality [30].) However, set equality andother basic operations on orbit-finite sets are computable inpolynomial space on their representations, including:● checking whether one set is an element (or a subset) of
another,● union and intersection of sets, cartesian product, setdifference,● applying an orbit-finite function to an argument, composing functions or relations,● finding the image of a subset along a relation,● checking whether a finite set S supports a given set,
calculating the least support of a set,
● partitioning a given set into S-orbits, calculating the Sorbit of a given element.
These basic operations have been implemented as components of atomic programming languages [31, 32].
Originally [16, 17], sets with atoms (known as nominal
sets in this context) were developed as an algebraic approachto name binding in syntax, with concepts such as name abstraction space introduced to that end. The modal µ-calculus,
with its fixpoint operators, is an archetypical example of aformalism where name binding plays a crucial role, and one
could use nominal techniques to study syntactic aspects of it.
We emphasize that this is not what we aim to do. In fact,
we do not even introduce the concepts of name abstraction,
α-conversion, etc. Rather, we shall build atoms into models,
formulas, variable names, etc., and variable binding in fixpoint
formulas will appear on top of that, independently. In this weare similar to studies of nominal rewriting such as [33].
IV. µ- CALCULUS WITH ATOMSIn this section we present the syntax and semantics of the µcalculus with atoms, following [15]. As an initial motivation,
consider the formula (7) again. That formula refers to aparticular atom a, but the property that it aims to formulate
does not really depend on that atom. One would like to write aformula that says: whenever an atom is input, it will be output
exactly two steps later. A formula like
νX. ( ⋀ (ina → ◻◻outa ) ∧ ◻X)
a∈A

(8)

does not fit the syntax of the µ-calculus as defined in (1)because the inner conjunction is infinite. The µ-calculus withatoms extends the classical calculus with such infinitary (butorbit-finitary) Boolean operators.
A. Syntax and semantics
Considering now the sets X of variables and B of basic
predicates as sets with atoms, we extend the syntax (1) withϕ ∶∶= ⋯ ∣ ⋁ ϕa .

(9)

a∈A

The precise meaning of this is that ϕ(−) is a finitely supported
function from A to the set of formulas. Strictly speaking, thea in the expression ⋁a∈A ϕa is merely decoration, and theexpression could be written just as ⋁ ϕ(−) . As a syntactic
sugar, we use the expected⋀ ϕa = ¬ ⋁ ¬ϕa .
a∈A

a∈A

The extended calculus is interpreted in Kripke models withatoms, where the set of states, the transition relation and thesatisfaction relation are all finitely supported. The semantics
extends (2) with:s{x ∈ ⋁ ϕa⇐⇒ x ∈ Jϕa Kξ
for some a ∈ A.
a∈A

ξ

It is straightforward to check (see [15, Lem. 4.7]) that thefunction J_K(−) is supported by supp(K), so:supp(JϕKξ ) ⊆ supp(ϕ, ξ, K).

Under this definition, formulas are not finite objects anymore,
but they remain finitely supported and orbit-finite. Every
formula has a well-defined finite height, so there is no needfor transfinite induction in structural reasoning on formulas. If
a formula ϕ is closed, then its every subformula ψ has only
finitely many free variables, because each free variable in ψ
must have been introduced by a fixpoint operator on the finite
path from the root of ϕ to the root of ψ. As a result, contexts
ξ can still be seen as partial functions with finite domains.
Our (9) is not the only way to introduce orbit-finitary
disjunction into the µ-calculus. Several equivalent alternatives
exist. In [15], a simple syntax ϕ ∶∶= ⋯ ∣ ⋁ Φ was used, where Φ
is a finitely supported, orbit-finite set of formulas. One could
also use ϕ ∶∶= ⋯ ∣ ⋁a/∈S ϕa where S is a finite set of atoms
and ϕ(−) is a function, supported by S, from A ∖ S to the setof formulas, or even ϕ ∶∶= ⋯ ∣ ∃a.ϕ where a is an atom and ϕa formula. Each approach has its advantages; see Appendix A
for a comparison.
B. Model checking and expressivity
Since a formula ⋁a∈A ϕa (and therefore every formula ofthe µ-calculus with atoms) is a finitely supported, orbit-finite
object, it may be presented by finite means as an instance of acomputational problem such as model checking. Indeed, model
checking of formulas on orbit-finite models K is decidable. To
see this (see [15, Thm. 5.1] for more details), proceed as forthe classical µ-calculus in Section II, inductively computing

the (finitely supported) sets JϕKξ ⊆ K for all subformulas ϕof a given formula.
For the case ϕ = ⋁a∈A ϕa , first calculate S = supp(K, ϕ, ξ).
Then pick any atom b ∈/ S, inductively compute R = Jϕb Kξ ,then compute R ⊆ PK the S-orbit of R, and return⋃ R ∪ Jϕa1 Kξ ∪ ⋯ Jϕan Kξ
where the Jϕai Kξ are computed inductively for {a1 , . . . , an } =S.
For the case ϕ = µX.ψ, it is important to see that thesequence of approximants Ψα (see (3) in Section II) stabilizes
after finitely many steps. This is because, by an easy induction
on the ordinal α, every Ψα is supported by the same set
S = supp(K, X, ψ, ξ). Since K is orbit-finite, it can only havefinitely many S-supported subsets.
Our calculus can now express formulas such as (8), but also
many others. For example, still over the same set B of basic
predicates as in Example 3, the formulaνX. ⋀ (ina → ◻(νY.¬ina ∧ ◻Y ))a∈A

says that on no computation path the same atom is ever input
more than once. (No state in the model from Example 3
satisfies this formula.)
However, the expressive power of the calculus leaves muchto be desired. Even in a simple setting where B = A theproperty #PATH is not definable (see [15, Sec. 7]), and neither
are many properties that are useful in practice.
V. H ISTORY- DEPENDENT µ- CALCULUS
We extend the µ-calculus with atoms with formulas of theform ♯a, where a ∈ A is an atom. The intuition is that ♯a holds
if the atom a has never appeared in any basic predicate thatheld on the transition path that led to the current state.
Put together, we extend (1) to:ϕ ∶∶= ⊺ ∣ p ∣ ♯a ∣ ¬ϕ ∣ ϕ ∨ ϕ ∣ ⋁ ϕa ∣ ◇ϕ ∣ X ∣ µX.ϕ;a∈Asome syntactic sugar is introduced as before.
To simplify the setting, from now on we assume that every
state x in a model satisfies only finitely many basic predicates,i.e., that pred(x) is finite. All examples considered so far, andfurther ones that we present in Section VI below, satisfy thisassumption. Then for any state x in a Kripke model we candefine the finite set of atoms:
evt(x) =⋃supp(p)(10)p∈pred(x)(evt(x) stands for events at x) which contains those atoms thatappear in some basic predicate that holds in x; these atoms
will be considered non-fresh in any path that originates in x.
For the semantics of our history-dependent calculus, aformula ϕ is now interpreted relative to a history H ∈ Pfin A,
i.e., a finite set of atoms. A context ξ also interprets variables
relative to histories, so it is of the type:ξ ∶ X ⇀ Pfin A → PK.

Semantics is formally defined by induction, extending (2) to:H

x ∈ J⊺Kξ

We present two scenarios which rely on comparing data
atoms for equality and can be encoded in our historydependent µ-calculus. The first one features two processes
trying to concurrently access a critical section, while thesecond one is a version of the cryptographic Needham–
Schroeder protocol [22].

for all x ∈ K

Hx ∈ JpKξ ⇐⇒ p ∈ pred(x)Hx ∈ J♯aKξ ⇐⇒ a ∈/ H
H

H

H

H

x ∈ J¬ϕKξ ⇐⇒ x ∈/ JϕKξHx ∈ Jϕ ∨ ψKξ ⇐⇒ x ∈ JϕKξ or x ∈ JψKξ{Hs
H⇐⇒ x ∈ Jϕa Kξ for some a ∈ A
x ∈ ⋁ ϕaa∈AξH

H∪evt(x)x ∈ J◇ϕKξ ⇐⇒ ∃y ∈ JϕKξHx ∈ JXKξJµX.ϕKξ

(11)

s.t. x Ð→ y⇐⇒ x ∈ ξ(X)(H)=

VI. E XAMPLES

lfp (Ψ ↦ JϕKξ[X↦Ψ] ) .

Notice how in the clause for ◇ϕ, the atoms in evt(x) areadded to the current history. Also notice how in the clause forµX.ϕ, the least fixpoint is taken over functions of the typeΨ ∶ Pfin A → PK,that is, over families (of sets of states) indexed by histories.
H
This is unavoidable: one could not define the set JµX.ϕKξ fora specific H by a fixpoint construction, since the variable X
may be evaluated inside ϕ for a history richer than H.
Functions Ψ as above, ordered by (pointwise) inclusion,
form a complete lattice, so the least fixpoint is well-defined.
However, unlike in the history-free setting, (11) does notprovide a method to compute the semantics of a formula.
The trouble is with fixpoint formulas: here approximants Ψαused as in (3) to define a least fixpoint are not orbit-finite
objects, so it is not clear how to even represent them by finite
means, let alone how to compute Ψα+1 from Ψα . Even ifthat was somehow solved, it is not clear why the sequence ofapproximants should stabilize after finitely many steps. Indeed,
unlike in Section IV-B, here approximants are families indexedby elements of an orbit-infinite set and there are infinitely
many of them, even for a fixed support S.
We must proceed with care, because the presence of data
atoms sometimes makes seemingly innocent problems become
undecidable; examples include language equivalence for nondeterministic orbit-finite automata [34], model checking for
CTL∗ with atoms [15], and the existence of a finitely supported homomorphism between two orbit-finite graphs [35].
Nevertheless, in Section VII, we shall deal with the above
issues and prove that model checking on orbit-finite models is
indeed decidable. For now, let us mention that the problematic
property #PATH is now easy to define by a formula:νX. ( ⋀ (a → ♯a) ∧ ◇X) .

A. Critical section
Two concurrent processes A and B have access to acommon critical section S. In order not to enter it together,
they can lock it with a password they must generate each time
before entering it. Only the process that locked the criticalsection can interact with it. The section can then be unlocked
using the same password. A typical interaction is depicted in
Figure 1, where the boxes on each thread show what password
is remembered, and the dashed arrows are actions that cannot
be performed, because of the drawn inequalities.
A
p

S

B
q

lockA

p

unlockB

unlockA
lockB

qr

unlockA

Fig. 1. An interaction between the processes and the critical section

We want to make sure that the two processes will never enter
the critical section together. Of course, this is only true under
the assumption that the processes will not generate the same
passwords. Building that requirement into the model would
make it orbit-infinite (an entire history of passwords would
have to be remembered in the state), so instead our model
will allow processes to generate arbitrary passwords, and thesafety condition will be included in the formula that defines
the desired property.
Formally, we build an orbit-finite, equivariant model K =(K, Ð→, ⊧) on the set of predicates
B = {pa ∣ a ∈ A} ∪ {lockA , lockB , unlockA , unlockB },where pa means that the password a has just been generated,
and the other predicates have obvious meanings. A state x ∈K basically records the passwords each thread remembers;
however, for the states to satisfy the right predicates, we needseveral copies of such a record. Formally, a state s a tuplea∈A

In fact, as the following examples show, the history-dependentcalculus is expressive enough to define some properties thatare interesting from the perspective of system verification.

x = (aA , aB , aS , s, t)(12)where the aX ’s are passwords remembered by the three threads(these may be some a ∈ A or ∅), and s and t form afinite component that models the current stage of interaction.
Specifically, the value of s ∈ {p, lock, unlock, ∅} specifies
whether a password is just being generated, the section locked
or unlocked (or perhaps none of that), and t ∈ {A, B, ∅} says
which one of the two processes is performing the action. In astate x, if s ∈ {lock, unlock} then x ⊧ st ; if s = p then x ⊧ pat ;otherwise x satisfies no basic predicates.
In defining the transition relation we use a simple notation
for updating components of states: x[B ↦ a, s ↦ p] denotes
the state x as in (12) with the component aB set to a and thecomponent s set to p, and so on. Transitions from a state x
as in (12) are as follows:● if s ≠ ∅ or t ≠ ∅, then x Ð→ x[s, t ↦ ∅] is the onlytransition (the states with s = t = ∅ are the “normal”
states of interaction, the other ones are there just to satisfy
the right predicates); otherwise,● x Ð→ x[A ↦ a, s ↦ p, t ↦ A] for every a ∈ A, andsimilarly for B (A and B can generate passwords),● if aS = ∅ and aA ≠ ∅, then x Ð→ x[S ↦ aA , s ↦lock, t ↦ A] and similarly for B (A and B can enter thecritical section when it is free),● if aA = aS ≠ ∅, then x Ð→ x[A, S ↦ ∅, s ↦ unlock, t ↦A] and similarly for B (when A or B unlocks the criticalsection, they forget their current password and have togenerate a new one).
Note that this indeed defines an orbit-finite model.
To define the property, we start by defining a formulasafe = ⋀ (pa → ♯a)a∈Awhich says that whenever there is a newly generated password,
then it has not been generated before. We can then define
PA = νX.(safe → (unlockA ∨ (¬unlockB ∧ ◻X))),
whose meaning is that, in all safe paths (where passwords
are generated at most once) from the current state, B cannot
unlock the critical section unless A has already unlocked it.
We define PB similarly. The property we are interested in isνX.(safe → ((lockA → PA ) ∧ (lockB → PB ) ∧ ◻X)),
which means that, for any safe path, if a process locks thecritical section, then the same process must unlock it before
the other can. This formula indeed holds in the initial state ofthis model (one where all components are ∅).
B. The Needham–Schroeder protocol
The Needham–Schroeder protocol allows two agents toverify each other’s identities on an unsafe network by using
public-key cryptography. A normal interaction according to
the protocol is depicted in the left-hand part of Figure 2. It
proceeds as follows:
1) A generates a nonce nA ,2) A sends (A, nA ) to B, encrypted with kP B (B’s public
key),3) B deciphers (A, nA ) using kSB (B’s secret key),4) B generates a nonce nB ,5) B sends (nA , nB ) to A, encrypted with kP A ,6) A deciphers (nA , nB ) using kSA and checks that the first
nonce is the one she sent,
7) A sends nB to B, encrypted with kP B ,8) B deciphers nB using kSB and checks that it is the nonce
he sent.
We model three agents: Alice, Bob, and Eve (A, B, and
E). Alice and Bob follow the protocol, while Eve does notnecessarily, which can lead to a man-in-the-middle attack [36],as depicted in the right-hand part of Figure 2. We want to see
if a state can be reached where Alice or Bob think they know
someone’s identity but they are actually mistaken.

0
1

sndr

rcvr

A

B

nA

A
nA

E

B

(nA , A)kP E

0nA(nA , A)kP B(nA , A)kP B

2

A, nA
nB

A, nA
2

nB
(nA , nB )kP A

34

5

nA , n B

5nB(nB )kP B
7

7(nA , nB )kP A(nB )kP E

nA , n B
6(nA , nB )kP AnB(nB )kP B

8nB

Fig. 2. The protocol and the man-in-the-middle attack

Formally, we build an equivariant model K = (K, Ð→, ⊧)on the set of predicates{na ∣ a ∈ A} ∪ {ka ∣ a ∈ A} ∪ {bad},with the intuition na represents a nonce (a state satisfies na if
na has just been generated), ka is a key (for brevity, we only
mention secret keys), and bad indicates bad states. Each statex ∈ K records the state of Alice, Bob, and Eve. We need a
few copies of these states so that x ⊧ na and x ⊧ ka happen
only when a nonce or key is generated.
We model Alice and Bob as 7-tuples (k, n, i, n′ , i′ , c, p) of
a key k, nonces n (generated by that agent) and n′ (received
from another agent), identities i (whom they are communicating with) and i′ (whom they hope to be communicating with)from {A, B, E}, a ciphertext c (which is modeled as a tuple ofthe key needed to decipher it and the information contained init), and the phase p of the protocol they are at (p is 0 or a pairof a number from 1..7 together with a flag f ∈ {sndr, rcvr},
depending on whether they sent the first message or received
it, as depicted on the left of Figure 2). All of these variables
may be ∅. Eve is modeled similarly, except she does not needto remember any identities, nor the phase of the protocol she isat, and is thus modeled as a quadruple (k, n, n′ , c). Formally, astate of K is then a quintuple (σA , σB , σE , s, t) where σA , σB ,and σE are the states of Alice, Bob, and Eve, and s ∈ {n, k, ∅}and t ∈ {A, B, E, ∅} specify if an action is being done, andwhich agent is doing it. We shall refer to Alice’s key in σA as
kA , etc. In a state x, if pA is (7, sndr) or (8, rcvr) (the possible
values of p at the end of the protocol) and iA ≠ i′A (Alice ismistaken on the identity of the agent she is communicatingwith), then x ⊧ bad, and similarly for Bob. If s ≠ ∅ and t = n,then x ⊧ nns . If s ≠ ∅ and t = k, then x ⊧ kks .
Any state x where s ≠ ∅ or t ≠ ∅ has a single transitionx Ð→ x[s, t ↦ ∅]. Otherwise, for Alice and Bob, the transition
relation follows the protocol (we let variables X, Y , and Z
range over identities):● they can always generate a public/secret key pair, andmust do so before beginning the protocol: x Ð→ x[kX ↦k, pX ↦ 0, s ↦ k, t ↦ X] for any k ∈ A,
● they can generate nonces (at steps 0 and (3, rcvr)), e.g.:
if pX = 0, then x Ð→ x[nX ↦ a, pX ↦ (1, sndr), s ↦n, t ↦ X] for any a ∈ A (X generates a nonce),● they can send and receive messages (e.g, at step
(1, sndr)): if pX = (1, sndr) and pY = 0, then x Ð→
x[iX ↦ Y, i′X ↦ Z, pX ↦ (2, sndr), iY ↦ X, cY ↦(kZ , X, nX ), pY ↦ (2, rcvr)] (X sends Y a test, thinking
they are Z),● they can decipher messages, provided they have theright key (e.g., at step (2, rcvr)): if pY = (2, rcvr), andcY = (kY , X, n) then x Ð→ x[n′Y ↦ n, i′Y ↦ X, pY ↦(3, rcvr)] (if the cipher is encrypted with the right key,
it is deciphered),and similarly for the other steps of the protocol. They
can also, at any time, decide to reset the protocol: x Ð→
x[nX , iX , n′X , i′X , cX , pX ↦ ∅]. For communications with
Eve, the transitions are nearly the same, except there needs
be no checks about fields not contained in our model of Eve.
There are also transitions corresponding to what Eve can do:● she can forge messages with a false identity, meaning she
does not need to send E as her identity, she can also send
A or B,● when deciphering messages, she decides what to do withnonces (e.g., she may throw them away),● she can “proxy” ciphertexts, meaning, if X (Alice or Bob)
is in phase 0, (2, sndr), or (5, rcvr) (i.e., ready to receivea message), and cE ≠ ∅, then x Ð→ x[cX ↦ cE , pX ↦p+X ], where 0+ = (2, rcvr), (2, sndr)+ = (5, sndr), and(5, rcvr)+ = (7, rcvr).
Note that this indeed defines an orbit-finite model.
Obviously, if there is a collision between keys or nonces(e.g., if kE = kA or nE = nA ) then the protocol can be broken.
We thus define the formulasafe = ⋀ (ka ∨ na → ♯a)a∈Ameaning there are no such collisions. The formula we areinterested in is then¬µX.(safe ∧ (bad ∨ ◇X)),
meaning that no safe path can reach a bad state.

(13)

Because of a well-known attack, this formula does not holdin our model. We can modify this to model a correction of the
protocol [36] by sending (nA , nB , B) encrypted with kP A instep 5), and A accepting only if B is the agent they thinkthey are communicating with. Formula (13) then holds. Notethat this does not mean that there are no attacks against themodified protocol, but only that Eve equipped with capabilities
defined in our model cannot break it.
VII. D ECIDABILITY OF MODEL CHECKING
In this section we shall prove that model checking formulasof the history-dependent µ-calculus against orbit-finite models
is decidable. More specifically, our aim is to show how to∅
inductively compute the set JϕK∅ , defined according to (11),from a given closed formula ϕ and an orbit-finite model K.
To make the proof easier to follow, from now on we assume
that the model K is equivariant. At the end of this section we
explain how this assumption can be dropped.
Since we assumed in Section V that pred(x) is finite forevery state x, recalling (10) it is easy to check thatevt(x) ⊆ supp(x),a useful property to keep in mind.
A. First attempts
Ignoring for a moment the fact that ξ interprets variables asfamilies indexed by arbitrary histories and it is not clear how toHpresent it by finite means, how could we compute JϕKξ from agiven ϕ, ξ and H? Here is an initial idea: intuitively, to check
H
whether x ∈ JϕKξ , it should not matter whether an atom abelongs to H if that atom is not present in the support of thecurrent situation, that is in the support of x, ϕ and perhaps ξ.
Such “locally fresh” atoms should be irrelevant for the validityof the statement. So perhaps one could restrict attention only
to those statements where H ⊆ supp(x, ϕ, ξ), which would
provide some bound on the size of histories considered.
This idea does not quite work, and it is not enough to keep
track of how global histories intersect with local supports. To
see why, consider the equivariant formulaϕ = ⋁ ¬ ♯aa∈Awhich says that some atom is not fresh. Since the formula isclosed, it can be interpreted in the empty context ξ = ∅. If
H
one wants to check whether x ∈ JϕKξ for an equivariant statex ∈ K, then the local support supp(x, ϕ, ξ) is empty. However,H
to check whether x ∈ JϕKξ we must know whether the history
H is empty, and this information is lost in the (necessarily
empty) intersection of H with the local support.
This motivates a refinement of the initial idea: together with
the intersection of a global history H with a local support S,
one should remember the number (but not the identities) of
those atoms in H which do not belong to S. This idea willturn out to work, so we shall now present it more formally.

B. Local-history semantics⎧
there is y ∈ K and D ⊆ A s.t.
⎪
⎪
⎪
⎪
⎪
⎪
x Ð→ y ∈ LϕMρ((n,H∪evt(x))↶S) D ,⎪⎪⎪⎪x ∈ L◇ϕMn,H⇐⇒ ⎨∣D∣ ≤ n,
ρ
⎪
⎪
⎪
⎪
D ⊆ supp(y) ∖ (H ∪ supp(x, ϕ, ρ)),
⎪
⎪
⎪
⎪
⎪
⎪
⎩where S = supp(y, ϕ, ρ),↶A local history is a history together with a natural number:(n, H) ∈ N × Pfin A.
The number n is the anonymous part, and H is the nonanonymous part of the local history.
Basic operations for anonymizing and de-anonymizing
atoms in local histories will be useful. For a local history(n, H) and a finite set of atoms S, define:x ∈ LXMn,H⇐⇒ x ∈ ρ(X)(n, H)
ρLµX.ϕMρ= lfp (Φ ↦ LϕMρ[X↦Φ] ) .

In the last equation, the least fixpoint is taken over functions:Φ ∶ (N × Pfin A) → PK.

(n, H) ↶ S = (n + ∣H ∖ S∣, H ∩ S).

(14)

This operation restricts the local view of a history to atoms
in S, and anonymizes all other atoms. The symbol ↶ is the
middle ground between the set intersection symbol (as the
non-anonymous part H is intersected with S), and a right-toleft arrow (as atoms are transferred from the non-anonymous
to the anonymous part).
Dually, define:↶(n, H)

S = (n − ∣S ∖ H∣, H ∪ S).

(15)

This operation is defined only if ∣S ∖ H∣ ≤ n. It forces all
atoms in S into the non-anonymous part, drawing them fromthe anonymous part if needed.
The anonymization operation can be applied to global
histories as well, writing H ↶ S for (0, H) ↶ S. Note thatH ↶ S is a representation of the S-orbit of H, in the sensethat H ↶S = H ′ ↶S if and only if H and H ′ are in the same SH
orbit. Our informal idea now is that x ∈ JϕKξ depends only on
the S-orbit of H for S = supp(x, ϕ, ξ) and so our semantics
can be computed with only local histories in focus.
To this end, we show an alternative local-history semantics
of our calculus, where a formula is interpreted for a local history (n, H) and a localized context ρ that interprets variables
relative to local histories:ρ ∶ X ⇀ (N × Pfin A) → PK.
The semantics is defined inductively as follows:x ∈ L⊺Mn,Hρx ∈ LpMn,Hρx ∈ L♯aMn,Hρx ∈ L¬ϕMn,Hρn,Hx ∈ Lϕ ∨ ψMρ

for all x ∈ K⇐⇒ p ∈ pred(x)⇐⇒ a ∈/ H⇐⇒ x ∈/ LϕMn,HρThe equations for the single-orbit disjunction and the diamond modality are considerably more complex than thecorresponding ones for the global history semantics (11), sosome explanation is in order.
For a formula ϕ = ⋁a∈A ϕa to hold in a state x given a
local history (n, H), it must be that some ϕa holds in thesame state. If a belongs to H, or if it does not belong to theglobal history whence (n, H) emerged, then the local history
relevant for ϕa in x is still (n, H). However, there is also a
possibility that a belongs to the global history, but it is absent
from the local support S and it had therefore been relegatedto the anonymous part of the local history, i.e., to the number
n. It should then be “de-anonymized”. Before that happens, it
is prudent to restrict the local view by intersecting it with S,
to ensure that the non-anonymous part H remains small.
Similar intuitions apply to ◇ϕ, but here an additional
complication appears: the supports of y and x can in general
be completely unrelated, so some atoms may have to beanonymized while other ones are de-anonymized. To this end,
while making a transition from the state x to y, a set D ofde-anonymized atoms is chosen. There must be at most n ofthem, since this is the size of the anonymous part of the local
history. There is no point in de-anonymizing an atom that isalready in H, so D and H must be disjoint. Furthermore, if an
atom is not in H but has been present in the current support,then the local history claims for a fact that the atom does notbelong to the global history either; so D and supp(x, ϕ, ρ)must be disjoint too. Finally, each de-anonymized atom mustbe part of the new current support S after the transition, whichin this situation is equivalent to belonging to supp(y).
Once D is chosen, a new local history is constructed as
expected; note that the elements of the set pred(x) become
part of the global history, but some of them (those not in S)
immediately go into the anonymous part of the local history.
C. Global vs. local histories⇐⇒ x ∈ LϕMn,Hor x ∈ LψMn,Hρρ

⎧
for some a ∈ A, x ∈ Lϕa Mn,H
, or
⎪
ρ
⎪
⎪
⎪
⎪
⎪
n
>
0
and
for
some
a
∈
/
H
∪
S,
⎪
⎪
⎪
⎪
{a}
x ∈ L ⋁ ϕa Mn,H⇐⇒
⎨ x ∈ Lϕa M((n,H)↶S)
,
ρ
ρ
⎪
⎪
a∈A
⎪
⎪
⎪
⎪
⎪
where S = supp (x, ⋁ ϕa , ρ) ,
⎪
⎪
⎪
⎩
a∈A

We now wish to show a formal correspondence between
the global and the local semantics, arguing by induction on
the structure of formulas. The inductive claim turns out to berather subtle, so we shall first explain why other, seemingly
simpler approaches do not work.
For a finite set S of atoms, a local-history context
ρ ∶ X ⇀ (N × Pfin A) → PK↶can be extended (“de-localized”) to one that depends on global
histories, denoted byρ↑S ∶ X ⇀ Pfin A → PK

if and only if for every x ∈ K, T ⊇ S ∪supp(x) and H ∈ Pfin A:x ∈ Φ(H ↶ T ) ⇐⇒ x ∈ Ψ(H)(compare (18)). From the definition it easily follows thatand defined by:ifρ↑S (X)(H) = ρ(X)(H ↶ S).
Comparing local and global history semantics, at first sight it
is natural to expect that for every formula ϕ, a local-history
context ρ, a global history H and every sufficiently large set
S of atoms:
H(16)
LϕMρH↶S = JϕKρ↑S .
More specifically, it is reasonable to expect this for S ⊇supp(ϕ, ρ), since the formula ϕ and its context ρ form thelocal view on history.
Unfortunately, Equation (16) fails. For a counterexample,
for B = A consider a state x ∈ K with pred(x) = supp(x) ={a} and the formulaϕ = ⋁ (a ∧ ♯a)Φ ∼S ΨandS ⊆ S′thenΦ ∼S ′ Ψ.

We will use this observation extensively in the following.
This relation ∼ is extended to contexts: for ρ ∶ X ⇀ (N ×
Pfin A) → PK and ξ ∶ X ⇀ Pfin A → PK with the same domain,
we write ρ ≈ ξ if and only if ρ(X) ∼supp(X,ρ) ξ(X) for every
X in that domain.
Theorem 4. For every formula ϕ and contextsρ ∶ X ⇀ (N × Pfin A) → PKξ ∶ X ⇀ Pfin A → PK
defined on the free variables of ϕ, if ρ ≈ ξ then
LϕMρ ∼supp(ϕ,ρ) JϕKξ .
Proof. By structural induction on ϕ; see Appendix B.

a∈A

Corollary 5. For any closed formula ϕ, LϕM0,∅∅ = JϕK∅ .
∅with a history H = {a} (the context ρ is irrelevant as ϕ isclosed). Since ϕ is an equivariant formula, one may take S = ∅so that H ↶ S = (1, ∅). It is then easy to check thatx ∈ LϕMH↶S
ρ

but

H

x ∈/ JϕKρ↑S .

Intuitively, the problem here is that we allowed too small an
S, in that it does not contain the support of the state x, whichshould rightly be a part of the local view on history.
To fix that, one may weaken (16) and postulate instead thatHx ∈ LϕMρH↶S ⇐⇒ x ∈ JϕKρ↑S(17)

whenever S ⊇ supp(x, ϕ, ρ). This, however, is ill-suited asa claim to prove by structural induction on ϕ; specifically,
the inductive step for fixpoint formulas µX.ϕ is problematic.
Indeed, for the inductive step one would want to prove that ifx ∈ Φ(H ↶ S) ⇐⇒ x ∈ Ψ(H)(18)

for some Φ ∶ (N × Pfin A) → PK and Ψ ∶ Pfin A → PK suchthat S ⊇ supp(x, ϕ, ρ, Φ, Ψ), then alsoHx ∈ LϕMH↶S
ρ[X↦Φ] ⇐⇒ x ∈ JϕKρ↑S [X↦Ψ] .
To use the inductive assumption (17) about ϕ, one would need:(ρ[X ↦ Φ])↑S = (ρ↑S )[X ↦ Ψ],
but this does not follow from (18). It would follow fromthe stronger assumption Φ(H ↶ S) = Ψ(H), but that would
amount to assuming (16), which fails in general.
To find the right claim to prove by induction, we look forthe middle ground between (16) and (17), by relaxing therelationship between contexts ρ and ρ↑S allowed in (17).
For any Φ ∶ (N×Pfin A) → PK, Ψ ∶ Pfin A → PK and a finite
set of atoms S, we writeΦ ∼S Ψ

(19)

Proof. By Theorem 4, LϕM∅ ∼supp(ϕ) JϕK∅ , and the conclusion
easily follows from the definition of ∼ in (19), as ∅ ↶ T =(0, ∅) for any T .

D. Relevant local histories
By Corollary 5, to find the semantics of a closed formulain a given model, one may equivalently calculate its localhistory semantics. This, however, does not imply yet thatmodel checking is decidable. Indeed it looks like a step
back, since in the local-history semantics fixpoint formulas areapproximated by families indexed by elements of N × Pfin A,
a clearly orbit-infinite set. We shall now show how the set ofindices can be limited to an essentially orbit-finite set, thus
ensuring decidability.
The inductive definition of LϕM0,∅∅ involves calculating many
sets of the form LψMn,Hfor ψ subformulas of ϕ. We willρ
show that the family of all such sets (more precisely, tuples(ψ, ρ, (n, H))) that appear in this calculation for a fixed
formula ϕ and a fixed orbit-finite model K, is essentially orbitfinite. It is clear that a fixed formula ϕ has only an orbitfinite set of subformulas ψ, but we need to find bounds on theremaining three ingredients.
To this end, we shall need a more refined analysis of theinductive definition of the semantics L_M. For a fixed closed
formula ϕ, define the set of relevant tuples (ψ, ρ, (n, H)) as
the least set closed under the following rules:● (ϕ, ∅, (0, ∅)) is relevant;● if (¬ψ, ρ, (n, H)) is relevant, then (ψ, ρ, (n, H)) is relevant;● if (ψ ∨ θ, ρ, (n, H)) is relevant, then (ψ, ρ, (n, H)) and(θ, ρ, (n, H)) are relevant;● if (⋁a∈A ψa , ρ, (n, H)) is relevant, then:– (ψa , ρ, (n, H)) is relevant for every a ∈ A and– if n > 0, then (ψa , ρ, ((n, H) ↶ S) {a}) is relevant
for every a ∉ H ∪ S, where S is as in the definition ofL⋁a∈A ψa Mρ ;● if (◇ψ, ρ, (n, H)) is relevant, then↶↶(ψ, ρ, ((n, H ∪ evt(x)) ↶ S)

D)

is relevant for every x, y ∈ K, and for every D and S asin the definition of L◇ψMρ ;● if (µX.ψ, ρ, (n, H)) is relevant, then, for every ordinal
α, the tuple (ψ, ρ[X ↦ Φα ], (n, H)) is relevant, whereΦα ∶ (N × Pfin A) → PK is defined by induction on α:– Φ0 is constant at ∅,– Φα+1 = LψMρ[X↦Φα ] ,– Φα = ⋃β<α Φβ for a limit ordinal α;′● if (X, ρ, (n, H)) is relevant, then (µX.ψ, ρ , (n, H)) isrelevant, where µX.ψ is the binding occurrence of X in
ϕ, and ρ′ is ρ restricted to free variables in µX.ψ.
Looking at the definition of L_M, it is easy to see that theinductive definition of LϕM0,∅∅ involves only those (and perhaps
not all those) sets LψMn,H
where (ψ, ρ, (n, H)) is relevant forρ
ϕ. For the case of fixpoint formulas, this is because
LµX.ψMn,H= LψMn,Hρρ[X↦Φα ]for some ordinal α. Moreover, in inductive computation of therightmost expression, ρ[X ↦ Φα ] is used for subformulas ofψ. As a result, for the case of variables we have
LXMn,H= Φα (n, H) = LψMn,Hρ
ρ′ [X↦Φβ ]for some β < α (e.g., β = α − 1 if α is not a limit ordinal),
and the tuple (ψ, ρ′ [X ↦ Φβ ], (n, H)) is relevant because(µX.ψ, ρ′ , (n, H)) is.
Our purpose now will be to show that the set of relevanttuples is “almost” orbit-finite, and that it can be usefully
approximated by an orbit-finite set.
First, let us define some auxiliary measures of the complexity of formulas. Let mu-depth(ϕ) denote the maximal numberof nested fixpoint operators in ϕ. Note that every subformulaof ϕ has at most mu-depth(ϕ) free variables. Moreover, let
max-var-supp(ϕ) denote the maximal size of the least support
of a variable name in ϕ, and let max-subf-supp(ϕ) be themaximal size of the least support of a subformula of ϕ. These
are all well-defined natural numbers.
Lemma 6. In every relevant tuple (ψ, ρ, (n, H)), the context
ρ has a support of size at most
mu-depth(ϕ) ⋅ (max-var-supp(ϕ) + max-subf-supp(ϕ)). (20)
Proof. It is enough to show that for every relevant tuple(ψ, ρ, (n, H)), and for every free variable X in ψ, the function
ρ(X) ∶ (N × Pfin A) → PK has a support of size at mostM ⋅ (max-var-supp(ϕ) + max-subf-supp(ϕ)),
where M is the number of fixpoint operators that surround ψ
in ϕ. This is proved by induction on the definition of the setof relevant tuples; see Appendix C for more details.

Note that the upper bound (20) on the size of a support ofρ in a relevant tuple (ψ, ρ, (n, H)) depends only on ϕ but noton ψ, n or H. Denote this upper bound by max-ctx-supp(ϕ).
Furthermore, let dim(K) be the dimension of K, i.e., themaximal size of the least support of a state of K.
Lemma 7. In every relevant tuple (ψ, ρ, (n, H)), the history
H contains at mostdim(K) + max-subf-supp(ϕ) + max-ctx-supp(ϕ) + 1(21)

atoms.
Proof. By induction on the definition of the set of relevanttuples. For the case of ◇ψ, it is easy to check that in the
resulting tuple (ψ, ρ, (n′ , H ′ )) there is H ′ ⊆ supp(y, ψ, ρ),and the conclusion follows since∣supp(y)∣ ≤ dim(K),∣supp(ψ)∣ ≤ max-subf-supp(ϕ), and● ∣supp(ρ)∣ ≤ max-ctx-supp(ϕ).
The case of ψ = ⋁a∈A ψa is similar, and all other cases are
trivial since they do not change the history H.
●●

The upper bound (21) on the size of a local history H ina relevant tuple (ψ, ρ, (n, H)) depends only on ϕ and on themodel K but not on ψ, ρ or n. Denote this upper bound by
max-loc-hist(ϕ, K).
Lemmas 6 and 7 imply that the only potentially unbounded
component of a tuple (ψ, ρ, (n, H)) relevant for a fixed
formula ϕ, is the number n, the size of the anonymous part ofthe local history. To deal with this final component, we shalluse a relative version of the notion of relevant tuple.
Specifically, for a relevant tuple Q = (ψ, ρ, (n, H)) for a
fixed formula ϕ, we say that another tuple (ψ ′ , ρ′ , (n′ , H ′ )) isrelevant for Q if it belongs to the least set of tuples containing
Q and closed under all rules that define the set of relevanttuples except the one for (ϕ, ∅, (0, ∅)). Obviously, if Q isrelevant then every tuple relevant for Q is itself relevant.
Lemma 8. For every relevant tuple Q = (ψ, ρ, (n, H)), andfor every tuple (ψ ′ , ρ′ , (n′ , H ′ )) relevant for Q,
n + ∣H∣ ≤ n′ + ∣H ′ ∣.
Proof. It is enough to show the inequality for all clauses inthe definition of the set of relevant tuples. In all clauses except⋁a∈A ψa and ◇ψ the inequality holds trivially as equality, as
then n′ = n and H ′ = H. For the case of ◇ψ, we haven′ + ∣H ′ ∣ = n + ∣H ∪ evt(x)∣ ≥ n + ∣H∣,
and the case of ψ = ⋁a∈A ψa is similar.
The next lemma applies to any closed formula ϕ andany orbit-finite model K. Intuitively, the lemma says that, if
the anonymous part of a local history grows large enough,its precise size ceases to matter and it may be seen as aninexhaustible supply of non-fresh, anonymous atoms.

Lemma 9. For any numbers m1 ≥ m2 and any ψ, ρ, and H
such that both tuples (ψ, ρ, (m1 , H)) and (ψ, ρ, (m2 , H)) arerelevant, if
m2 + ∣H∣ > max-loc-hist(ϕ, K) + dim(K)

(22)

1 ,H
2 ,H
then the two tuples are equivalent, i.e., LψMm
= LψMm.
ρρ

Proof. If ψ is of the form ⊺, p or ♯a, the conclusion holds trivially. For other cases, the proof follows by fixpoint induction
on the definition of the set of relevant tuples. The two interesting cases are ⋁a∈A ψa and ◇ψ, where a nontrivial conditionon the size of the anonymous part of the history appears. For
these cases it is important that, by (22) and by Lemma 7, wehave m1 , m2 > dim(K), so the side conditions on n in thedefinitions of L⋁a∈A ψa M and L◇ψM become vacuous. Finally,
by Lemma 8, the inequality (22) is preserved in any tuple
relevant for (ψ, ρ, (m1 , H)) and (ψ, ρ, (m2 , H)).
E. Decidability
We are now ready to prove our main technical result:
Theorem 10. Given a closed formula ϕ and a state x in
an equivariant, orbit-finite model K, it is decidable whether∅
x ∈ JϕK∅ .
Proof. By Theorem 4, it is enough to decide whether x ∈LϕM0,∅∅ . To this end, one computes the local-history semantics of ϕ and all its subformulas by induction, much as in
Section IV-B for the history-free µ-calculus with atoms. As
before, the most complex case is for a fixpoint formula µX.ψ,
where a least fixpoint of an operator working over families:Φ ∶ (N × Pfin A) → PK
needs to be computed. By Lemma 7, these families may
be safely restricted to indices (n, H) such that ∣H∣ ≤max-loc-hist(ϕ, K), an upper bound computable from ϕ and
K. Then, by Lemma 9, for any m1 ≥ m2 such that (22) holds(another bound computable from ϕ and K), all families Φ
considered satisfy
Φ(m1 , H) = Φ(m2 , H),
so one may restrict attention to families Φ indexed by (n, H)
such that n ≤ max-loc-hist(ϕ, K) + dim(K), augmented with
one more index for each H that represents a “very large n”.
Altogether, to compute LµX.ψMρ , one builds a series ofapproximating families Φ, each of them indexed by the same
orbit-finite set. The set of indices is equivariant, and the families themselves have a common finite support supp(X, ψ, ρ).
Since K is orbit-finite, this implies that there are only finitely
many families Φ to consider, therefore the approximation
process will reach a fixpoint after finitely many steps.
Remaining cases work as in Section IV-B.
Our decidability proof was formulated under the assumptionthat K is equivariant. This is easy to lift: for an arbitrary orbitfinite model the proof is the same, but with supp(K) added
to all the relevant supports such as supp(x, ϕ, ρ). Whenever afunction or relation is claimed to be equivariant in the proof,
it should now be supported by supp(K).

VIII. F UTURE WORK
To facilitate our decidability proof, we restricted the designof the history-dependent µ-calculus in several ways. The
restrictions help identify local histories as a key tool and still
let us cover substantial examples, but it should be interesting
to see how our techniques extend to richer scenarios.
Perhaps the easiest extension is to allow infinitely many
basic predicates to hold in a state. This is particularly simple
when each basic predicate is built of a single atom, since an
infinite but finitely supported set of atoms must be co-finite. A
cofinite set of basic predicates that hold in a single state leaves
only finitely many predicates fresh, so visiting such states on atransition path makes freshness properties easy to check. The
situation becomes more complicated when arbitrary orbit-finite
sets of basic predicates are considered.
Further in this direction, simple freshness tests ♯a are
but one of many properties of histories than one may want
to check. Others include, e.g., checking whether the global
history is of even size, or some regular properties such as
checking that, historically, every occurrence of a particularpredicate was followed by an occurrence of another one. For
properties that can be restricted to local views of histories, ourproof technique should be applicable.
In the forthcoming [37], an extended version of [15], avectorial version of the µ-calculus with atoms is considered,
where orbit-finitely many variables may be bound by a single fixpoint operator. Intuitively, this amounts to equipping
fixpoint variables with atoms as parameters. Unlike in theatom-less case, the vectorial calculus with atoms is a proper
extension of the “scalar” one. Adding freshness tests to thevectorial calculus is a worthwhile task, and we conjecture thatmodel checking remains decidable for that case. The vectorialµ-calculus is closely connected to alternating tree automata
and parity games, and the next challenge is to draw thatconnection in the presence of freshness tests. In particular, aconnection the tree automata models proposed in [11] needs tobe understood, as the most general of them can check a finitetree version of our #PATH property. A connection to parity
games should also be enlightening, as the idea of forgetting thepast is well established in game theory in the form of various
memoryless strategy theorems. Another potentially interesting
connection is to the notion of history-preserving bisimilarity
in the theory of true concurrency [38], where a model of tree
automata, as well as a µ-like calculus, was introduced.
As argued in [18], the theory of sets with atoms can beformulated more generally, for an infinite relational structure
A subject to some model-theoretic conditions. An example
is the framework of ordered atoms, where atoms are rational
numbers that can be compared not only for equality but also
for order. Ordered data values arise naturally in various systems, e.g., as timestamps or as process identifiers in distributed
protocols such as leader election. In [37] a µ-calculus withordered atoms is introduced, and the question of extending itwith freshness tests remains open.

R EFERENCES[1] D. Kozen, “Results on the propositional µ-calculus,”
Theor. Comp. Sci., vol. 27, no. 3, pp. 333 – 354, 1983.
[2] E. A. Emerson and J. Y. Halpern, ““Sometimes” and“Not Never” revisited: On branching versus linear time
temporal logic,” J. ACM, vol. 33, no. 1, pp. 151–178,
1986.
[3] L. Segoufin, “Automata and logics for words and trees
over an infinite alphabet,” in Procs. CSL 2006, ser. Lect.
Notes in Comp. Sci., vol. 4207, 2006, pp. 41–57.
[4] S. Demri, R. Lazic, and D. Nowak, “On the freeze quantifier in constraint LTL: decidability and complexity,” Inf.
Comput., vol. 205, no. 1, pp. 2–24, 2007.
[5] S. Demri and R. Lazic, “LTL with the freeze quantifier and register automata,” ACM Trans. Comput. Log.,
vol. 10, no. 3, pp. 16:1–16:30, 2009.
[6] D. Figueira and L. Segoufin, “Future-looking logics ondata words and trees,” in Procs. MFCS 2009, ser. Lect.
Notes in Comp. Sci., vol. 5734, 2009, pp. 331–343.
[7] S. Demri, D. D’Souza, and R. Gascon, “Temporal logics
of repeating values,” J. Log. Comput., vol. 22, no. 5, pp.
1059–1096, 2012.
[8] S. Demri, D. Figueira, and M. Praveen, “Reasoning aboutdata repetitions with counter systems,” Logical Methods
in Computer Science, vol. 12, no. 3, 2016.
[9] S. Demri and D. D’Souza, “An automata-theoretic approach to constraint LTL,” Inf. Comput., vol. 205, no. 3,
pp. 380–415, 2007.
[10] C. Carapelle and M. Lohrey, “Temporal logics withlocal constraints (invited talk),” in Procs. CSL 2015, ser.
LIPIcs, vol. 41, 2015, pp. 2–13.
[11] D. Figueira, “Alternating register automata on finite
words and trees,” Logical Methods in Computer Science,
vol. 8, no. 1, 2012.
[12] M. Jurdzinski and R. Lazic, “Alternating automata on
data trees and xpath satisfiability,” ACM Trans. Comput.
Log., vol. 12, no. 3, pp. 19:1–19:21, 2011.
[13] J. F. Groote and R. Mateescu, “Verification of temporal
properties of processes in a setting with data,” in Procs.
AMAST’99, 1999, pp. 74–90.
[14] J. F. Groote and T. A. Willemse, “Model-checking processes with data,” Science of Computer Programming,
vol. 56, no. 3, pp. 251–273, 2005.
[15] B. Klin and M. Łełyk, “Modal µ-Calculus with Atoms,”
in Procs. CSL 2017, ser. LIPIcs, vol. 82, 2017, pp. 30:1–
30:21.
[16] A. M. Pitts, Nominal Sets: Names and Symmetry in
Computer Science. Cambridge University Press, 2013.
[17] M. Gabbay and A. M. Pitts, “A new approach to abstract
syntax with variable binding,” Formal Asp. Comput.,vol. 13, no. 3-5, pp. 341–363, 2002.
[18] M. Bojańczyk, B. Klin, and S. Lasota, “Automata theory
in nominal sets,” Log. Meth. Comp. Sci., vol. 10, 2014.
[19] B. Klin, E. Kopczyński, J. Ochremiak, and S. Toruńczyk,“Locally finite constraint satisfaction problems,” inProcs. LICS 2015, 2015, pp. 475–486.
[20] N. Tzevelekos, “Fresh-register automata,” in ACM SIGPLAN Notices, vol. 46, no. 1. ACM, 2011, pp. 295–306.
[21] U. Montanari and M. Pistore, History-Dependent Automata: An Introduction, 2005, pp. 1–28.
[22] R. M. Needham and M. D. Schroeder, “Using encryption for authentication in large networks of computers,”
Comms. ACM, vol. 21, no. 12, pp. 993–999, 1978.
[23] A. Arnold and D. Niwiński, Rudiments of µ-calculus,
ser. Studies in logic and the foundations of mathematics.
Amsterdam: London, 2001.
[24] J. Bradfield and C. Stirling, “Modal logics and mucalculi: an introduction,” in Handbook of Process Algebra. North-Holland, 2001, pp. 293–330.
[25] Y. Venema, Lectures on the modal µ-calculus. ILLC,
Univ. of Amsterdam, 2007.
[26] J. Bradfield and C.Stirling, “Modal mu-calculi,” in Handbook of Modal Logic. Elsevier, 2007, vol. 3, pp. 721–
756.
[27] J. Bradfield and I. Walukiewicz, “The mu-calculus andmodel-checking,” in Handbook of Model Checking, H. V.
E. Clarke, T. Henzinger, Ed. Springer-Verlag, 2015.
[28] C. S. Calude, S. Jain, B. Khoussainov, W. Li, and
F. Stephan, “Deciding parity games in quasipolynomial
time,” in Procs. 49th STOC. ACM, 2017, pp. 252–263.
[29] J. Ochremiak, “Extended constraint satisfaction problems,” Ph.D. dissertation, University of Warsaw, 2016.
[30] L. J. Stockmeyer and A. R. Meyer, “Word problems requiring exponential time (preliminary report),” in Procs.
STOC’73, 1973, pp. 1–9.
[31] B. Klin and M. Szynwelski, “SMT solving for functional
programming over infinite structures,” in MFSP, vol. 207,2016, pp. 57–75.
[32] E. Kopczyński and S. Toruńczyk, “Lois: Syntax andsemantics,” in Procs. of POPL 2017, 2017, pp. 586–598.
[33] M. Fernández and M. J. Gabbay, “Nominal rewriting,”
Information and Computation, vol. 205, no. 6, pp. 917–
965, 2007.
[34] F. Neven, T. Schwentick, and V. Vianu, “Towards regular
languages over infinite alphabets,” in MFCS, 2001, pp.
560–572.
[35] B. Klin, S. Lasota, J. Ochremiak, and S. Toruńczyk,“Homomorphism problems for first-order definable structures,” in Procs. FSTTCS’16, ser. LIPIcs, vol. 65, 2016,
pp. 14:1–14:15.
[36] G. Lowe, “Breaking and fixing the Needham–Schroeder
public-key protocol using FDR,” in International Workshop on Tools and Algorithms for the Construction andAnalysis of Systems. Springer, 1996, pp. 147–166.
[37] B. Klin and M. Łełyk, “Scalar and vectorial µcalculus with atoms,” 2019, to appear. Available fromhttps://arxiv.org/abs/1803.06752.
[38] P. Baldan and T. Padoan, “Automata for true concurrency
properties,” in Foundations of Software Science andComputation Structures, C. Baier and U. Dal Lago, Eds.
Springer International Publishing, 2018, pp. 165–182.

A PPENDIX AS YNTACTIC VARIANTS OF ORBIT- FINITE DISJUNCTION
Our (9) is not the only way to introduce orbit-finitary
disjunction into the µ-calculus. Several equivalent alternatives
exist, each with its own advantages.
In [15], a simple syntax
ϕ ∶∶= ⋯ ∣ ⋁ Φ(23)

was used, where Φ is a finitely supported, orbit-finite set of
formulas, with semantics defined by:x ∈ J⋁ ΦKξ ⇐⇒ x ∈ JϕKξ for some ϕ ∈ Φ.
One can then dispense with the finite disjunction ϕ ∨ ψ, as it
becomes a special case. It is easy to subsume (9) with this
syntax: for ⋁a∈A ϕa one may write ⋁ Φ where Φ is the range(i.e., direct image) of the function ϕ(−) .
An encoding in the other direction is a little more complex.
First, consider ⋁ Φ where Φ consists of a single S-orbit for
S = supp(Φ). Pick any formula ϕ ∈ Φ and let
T = supp(ϕ) ∖ S = {b1 , . . . , bn }.
Then instead of ⋁ Φ one may write⋁ ⋁ ⋯ ⋁ ψa1 ,...,ana1 ∈A a2 ∈A

an ∈A

with the function ψ from An to the set of formulas definedby:ψ(a1 , . . . , an ) = {ϕ ⋅ πb̄ā

if a1 ≠ ⋯ ≠ an ∈/ S,
otherwise

where πb̄ā denotes any atom automorphism that maps bi to ai
for i = 1..n and fixes every atom in S. Finally, for Φ with morethan orbit, one can encode each of the orbits separately andcombine the formulas thus obtained with finite disjunction.
In this paper we choose the syntax (9) over (23) because
it enforces tighter control on the supports of disjuncts in anorbit-finite disjunction, which will come handy for our proofs.
Specifically, for ϕ = ⋁a∈A ϕa we havesupp(ϕa ) ⊆ supp(ϕ) ∪ {a}for every a ∈ A,

whereas for ϕ = ⋁ Φ, the least support of a formula ψ ∈ Φ
may considerably differ from supp(ϕ). Another reason is thatin practical examples, such as (8), orbit-finite operators tend
to be of the form prescribed by (9).
Actually, in most examples, orbit-finite disjunctions andconjunctions have an even simpler form, where in ⋁a∈A ϕa all
the formulas ϕa have the same shape; formally, they belong
to a single orbit. Indeed, one could replace the syntax (9) withthe following variant:ϕ ∶∶= ⋯ ∣ ⋁ ϕa

(24)

a/∈S

where S is a finite set of atoms and ϕ(−) is a function,
supported by S, from A ∖ S to the set of formulas. It thenfollows that the range of ϕ(−) is a single S-orbit. In thepresence of finite disjunction this syntax is easily equivalent
to (9). Indeed, for ⋁a/∈S ϕa one may write ⋁a∈A ψa whereψa = {ϕa

if a ∈/ S.
otherwise

In the other direction, for ⋁a∈A ϕa , putting S = {a1 , . . . , an } =supp(ϕ(−) ), one may write
ϕa1 ∨ ⋯ ∨ ϕan ∨ ⋁ ϕa .
a/∈S

The syntax (24) is quite convenient in practice, as it lets one
write formulas such as ⋁a ⋁a≠b ⋁c/∈{a,b} ϕa,b,c , guaranteeing
the atoms a, b, c to be distinct in ϕa,b,c .
One could even simplify (24) to write:
ϕ ∶∶= ⋯ ∣ ∃a.ϕ(25)

where a ∈ A, with ∃a.ϕ standing for ⋁b/∈supp(ϕ)∖{a} ψb , whereψb = ϕ⋅(a b). This syntax is particularly appealing, as formulas
over it appear as finite objects. It also represents the usefulintuition that orbit-finite disjunction introduces an atom to thescope of a formula, quantifying it existentially.
For all its simplicity, the syntax (25) may be tricky to workwith for a reader who has not much experience in nominal
techniques. For example, it would be wrong to see a formula∃a.ϕ as a formal pair built of a and ϕ. Indeed, the atoma belongs to the support of such a pair, but the intention
is that a ∈/ supp(∃a.ϕ). Rather, ∃a.ϕ belongs to a so-called
abstraction space [A]F, where F is a set of formulas. The
reader familiar with the book [16] would have no difficulty infollowing this approach, but we prefer to avoid the need toformally introduce abstraction spaces and α-conversion, andwe stick to the more elementary (albeit not finitary) syntax (9).
A PPENDIX B
P ROOF OF T HEOREM 4
For technical convenience, we shall assume that in every
fixpoint formula µX.ϕ,
supp(ϕ) ⊆ supp(X).

(26)

This is not true for a µ-formula in general; consider for
exampleµX.(a ∨ ◇X)
for some fixed a ∈ A and an equivariant variable nameX. However, every formula can again be transformed toan equivalent one with this property, by renaming variables.
Indeed, the variable X in µX.ϕ can be replaced with one
with the name X a1 ,...,an , where (a1 , . . . , an ) is any fixed
enumeration of supp(ϕ). For example, the formula above
becomesµX a .(a ∨ ◇X a ),which satisfies the assumption and is clearly semanticallyequivalent both under the global- and the local-history semantics.
We shall need a few simple observations on the anonymisation and de-anonymisation operators. All of the following areeasy to prove from the definitions (14) and (15).

It is enough to prove that for every ordinal α:

For all local histories (n, H) and sets S, T of atoms, we
have:((n, H) ↶ S) ↶ T = (n, H) ↶ (S ∩ T ),(27)

Φα ∼supp(ϕ,ρ) Ψα .

In the ordinal induction, the case of α a limit ordinal is easy.
For a successor ordinal α + 1 we need to show, under theassumption (31), that

if T ⊆ H then:↶((n, H) ↶ S)

T = (n, H) ↶ (S ∪ T ),(28)

LψMρ[X↦Φα ] ∼supp(ϕ,ρ) JψKξ[X↦Ψα ] .

if T ∩ H ⊆ S then:(n, H) ↶ S = (n, H) ↶ (S ∪ T ),′↶n′ + ∣H ′ ∣ = n + ∣H∣ = n′′ + ∣H ′′ ∣.

or, in other words, that for all Y ∈ FV(ψ)(30)ρ[X ↦ Φα ](Y ) ∼supp(Y,ρ[X↦Φα ]) ξ[X ↦ Ψα ](Y ).

The proof of Theorem 4 proceeds by induction on the
structure of ϕ. There are nine cases to consider:● ϕ = ⊺ is immediate.
● ϕ = p: check

For Y ≠ X, this follows from ρ ≈ ξ. Indeed, as
ρ(Y ) ∼supp(Y,ρ) ξ(Y ) and supp(ρ) ⊆ supp(ρ[X ↦ Φα ]),we haveρ[X ↦ Φα ](Y ) = ρ(Y ) ∼supp(Y,ρ[X↦Φα ]) ξ(Y ) = ξ[X ↦ Ψα ](Y ).

H

x ∈ LpMH↶T⇐⇒ p ∈ pred(x) ⇐⇒ x ∈ JpKξ .
ρ

For Y = X, we rely on our syntactic convention (26) whichguarantees thatϕ = ♯a: the assumption that T ⊇ supp(ϕ) ∋ a ensures the
middle equivalence in:supp(ϕ, ρ) ⊆ supp(X, ρ[X ↦ Φa ]).

H

x ∈ L♯aMH↶T⇐⇒ a ∈/ H ∩ T ⇐⇒ a ∈/ H ⇐⇒ x ∈ J♯aKξ .
ρ●●Using this inclusion together with (31), calculate

ϕ = ¬ψ is immediate.
ϕ = ψ ∨ θ: by the inductive assumption,
LψMρ ∼supp(ψ,ρ) JψKξ

ρ[X ↦ Φα ](X) = Φα ∼supp(X,ρ[X↦Φα ]) Ψα = ξ[X ↦ Ψα ](X),LθMρ ∼supp(θ,ρ) JθKξ .

andAssume that x ∈ LϕMH↶Tρconcluding the proof of (33). We may therefore apply the
inductive assumption about ψ to conclude

for T ⊇ supp(x, ϕ, ρ); without
loss of generality, let x ∈ LψMH↶T. Since supp(ψ) ⊆ρ
supp(ϕ), we have T ⊇ supp(x, ψ, ρ) and we may use theH
inductive assumption to conclude that x ∈ JψKξ , thereforeHx ∈ JϕKξ as required. Other cases are similar.
● ϕ = X: the assumption that ρ ≈ ξ, hence ρ(X) ∼supp(X,ρ)ξ(X), ensures the middle equivalence in:x ∈ LXMH↶T
ρ
●

(32)

Aiming to use the inductive assumption about ψ, we firstprove thatρ[X ↦ Φα ] ≈ ξ[X ↦ Ψα ],
(33)

(29)

and finally, if (n , H ) = (n, H) ↶ S, and ∣T ∣ ≤ n and(n′′ , H ′′ ) = (n, H) T then:
′

●

(31)

LψMρ[X↦Φα ] ∼supp(ψ,ρ[X↦Φα ]) JψKξ[X↦Ψα ] .
To infer (32) from this, it is enough to show thatsupp(ψ, ρ[X ↦ Φα ]) ⊆ supp(ϕ, ρ).
Obviously though, supp(ψ, ρ, X) = supp(ϕ, ρ), andsupp(Φα ) ⊆ supp(ψ, X, ρ)⇐⇒ x ∈ ρ(X)(H ↶ T )H⇐⇒ x ∈ ξ(X)(H) ⇐⇒ x ∈ JXKξ .

ϕ = µX.ψ: the semantics JµX.ψKξ is the limit of theincreasing transfinite sequence:●

follows by easy ordinal induction on α.
ϕ = ⋁a∈A ϕa : for any H ∈ Pfin A, x ∈ K and T ⊇supp(x, ϕ, ρ), assuming that ρ ≈ ξ, we must showH

Ψ0 ⊆ Ψ1 ⊆ Ψ2 ⊆ ⋯ ⊆ Ψω ⊆ Ψω+1 ⊆ ⋯x ∈ LϕMH↶T⇐⇒ x ∈ JϕKξ .
ρ

where Ψα ∶ Pfin A → PK (with the inclusion order above
understood pointwise) are defined by ordinal induction, andin particular

We begin with the left-to-right implication. Unfolding thedefinition of LϕM, consider three cases:(a) There exists some a ∉ H or a ∈ T such that x ∈ Lϕa MH↶T.
ρ
Then it is easy to check that H ↶ T = H ↶ (T ∪ {a}).
Moreover, T ∪{a} ⊇ supp(x, ϕa , ρ), so we may apply the
inductive assumption about ϕa to conclude thatHΨα+1 (H) = JψKξ[X↦Ψα ] .
Similarly, LµX.ψMρ is the limit of:Φ0 ⊆ Φ1 ⊆ Φ2 ⊆ ⋯ ⊆ Φω ⊆ Φω+1 ⊆ ⋯with Φα ∶ (N × Pfin A) → PK and in particular:Φα+1 (n, H) = LψMn,H
ρ[X↦Φα ]∪{a})x ∈ Lϕa MH↶T⇐⇒ x ∈ Lϕa MH↶(T
ρ
ρ
H

(34)

H

⇐⇒ x ∈ Jϕa Kξ Ô⇒ x ∈ JϕKξ .

(b) There exists some a ∈ H ∖ T such that x ∈ Lϕa MH↶T.
ρ
Then pick any b ∉ H ∪ T and let π = (a b) be the atom

automorphism that swaps a and b. Since a, b ∉ T we havethat:
ϕ ⋅ π = ϕ,ρ ⋅ π = ρ.

(35)

∪{a})
x ∈ Lϕa MH↶(T= Lϕa MH↶T.
ρρ

Moreover, we have (H ⋅ π) ↶ T = H ↶ T , hencex ∈ Lϕa M(H⋅π)↶T.
ρThe relation ≈ is equivariant, so we have ρ = ρ ⋅ π ≈ ξ ⋅ π.
Since a ∉ H ⋅ π, by case (a) above we obtain(b) a ∈ H ∖ T . Then obviously ∣H ∖ T ∣ > 0. Moreover, sinceT ⊇ S = supp(x, ϕ, ρ), we get thata ∉ (H ∩ T ) ∪ S,

H⋅πx ∈ JϕKξ⋅πand, applying π to everything involved, by equivarianceHand by (35) we get x ∈ JϕKξ as required.
(c) ∣H ∖ T ∣ > 0 and (denoting S = supp(x, ϕ, ρ) from nowon) there exists someso by definition of LϕM the only thing that remains to bechecked is:x ∈ Lϕa Mρ((H↶T )↶S)

.

↶

↶

↶

↶

= (H ↶ S){a}by (27){a}because S ⊆ T .

{a}.

{a} = (H ↶ S){a} = H ↶ (S ∪ {a}).

(36)First, we notice that

= (H ↶ (T ∩ S))

↶

{a}

↶

((H ↶ T ) ↶ S)

such that((H ↶ T ) ↶ S)

{a}

But, by the same reasoning as in (c) above and using (28):a ∉ (H ∩ T ) ∪ S)↶S)x ∈ Lϕa M((H↶Tρ↶x ⋅ π = x,(a) a ∉ H or a ∈ T . Then it is easy to check that H ↶ T =H ↶(T ∪{a}). Moreover, T ∪{a} ⊇ supp(x, ϕa , ρ), so wemay use the inductive assumption about ϕa to conclude
that

Since S ∪{a} ⊇ supp(x, ϕa , ρ), we may use the inductive
H↶(S∪{a})assumption about ϕa to conclude that x ∈ Lϕa Mρ
as required.
● ϕ = ◇ψ: for any H ∈ Pfin A, x ∈ K and T ⊇ supp(x, ϕ, ρ),assuming that ρ ≈ ξ, we must showH↶{a}) ⋅ π= (H ↶ S) ⋅ π↶{a} ⋅ π= (H ↶ S){b}because a, b ∉ H ∩ T ⊇ H ∩ S= H ↶ (S ∪ {b})by (28), because b ∈ H,

by equivariance↶so, applying π to everything in (36), by equivariance andusing (35), we obtainx ∈ Lϕa ⋅ πMρH↶(S∪{b}) .
By definition of S we have S ∪ {a} ⊇ supp(x, ϕa , ρ),which implies that S ∪ {b} ⊇ supp(x, ϕa ⋅ π, ρ). Thus
we may apply the inductive assumption about ϕa ⋅ π toconclude thatHx ∈ Jϕa ⋅ πKξ .
Applying π to everything here, by equivariance andusing (35) and π −1 = π, we obtainH⋅πx ∈ Jϕa Kξ⋅π ,

hence

H⋅π

x ∈ JϕKξ⋅π .

Again applying π everywhere and using (35), we conclude
Hthat x ∈ JϕKξ as required.
We now move to the right-to-left implication of (34). AsH
sume that there exists some a ∈ A such that x ∈ Jϕa Kξ .
There are two cases to consider:(37)

Note that supp(ϕ) = supp(ψ); we shall use these twointerchangeably without further warnings.
We begin with the left-to-right implication. Unfolding thedefinition of LϕM, assume that x Ð→ y and D ⊆ A such that:(i) D ⊆ supp(y) ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ)),(ii) ∣D∣ ≤ ∣H ∖ T ∣, and(((H↶T )∪evt(x))↶S) D(iii) y ∈ LψMρ
where S = supp(y, ϕ, ρ)and (n, H) ∪ X stands for (n, H ∪ X).
Pick any E ⊆ H ∖ T such that ∣E∣ = ∣D∣ (it exists byassumption (ii)), and let π be an atom automorphism suchthat:(iv) D ⋅ π = E,(v) (supp(y) ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ) ∪ D)) ⋅ π is disjoint
from H ∪ pred(x),(vi) π(a) = a for a ∈ (H ∩ T ) ∪ supp(x, ϕ, ρ).
Such an automorphism exists since conditions (iv)-(vi) restrict its action only on three pairwise disjoint sets of atoms,
and they allow mapping them to other pairwise disjoint sets.
In particular, we havex ⋅ π = x,ψ ⋅ π = ψ,ρ ⋅ π = ρ.

(38)

The transition relation is equivariant, so x = x ⋅ π Ð→ y ⋅ π
is a valid transition. Moreover, applying π to everything inassumption (iii), by equivariance we obtain↶((H ↶ S)x ∈ L◇ψMH↶T⇐⇒ x ∈ J◇ψKξ .
ρ

↶Then pick any b ∈ H ∖ T (it exists since ∣H ∖ T ∣ > 0) andlet π = (a b) be the atom automorphism that swaps a andb (note that it may well be that a = b and π = id A ). Sincea ∉ S and b ∉ T , the identities in (35) hold. Moreover,y ⋅ π ∈ LψMρ((((H↶T )∪evt(x))↶S)

D)⋅π

.

(39)

But, because evt(x) ⊆ supp(x) ⊆ T and π fixes every atomin (H ∪ evt(x)) ∩ T by (vi),D ⊆ supp(y) ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ)),= ((((H ∪ evt(x)) ↶ T ) ↶ S ⋅ π)↶

= ((H ∪ evt(x)) ↶ (T ∩ S ⋅ π))

EE)
by (27)= (H ∪ evt(x)) ↶ ((T ∩ S ⋅ π) ∪ E)

by (28).

so the first two conditions on D imposed by the definitionof L◇ψM are satisfied. Finally,
D↶D) ⋅ π↶D) ⋅ π↶= ((((H ∪ evt(x)) ↶ T ) ↶ S)↶((((H ↶ T ) ∪ evt(x)) ↶ S)

and since it is contained in S and (as we just have said)
disjoint from supp(ϕ, ρ), it is contained in supp(y). Altogether,Devt(x) ⊆ T= ((H ∪ evt(x)) ↶ (T ∩ S)) D= (H ∪ evt(x)) ↶ ((T ∩ S) ∪ D)

by (27)by (28)= (H ∪ evt(x)) ↶ ((T ∪ H) ∩ S)

definition of D(((H ↶ T ) ∪ evt(x)) ↶ S)
= (((H ∪ evt(x)) ↶ T ) ↶ S)↶

We will now show that this is equal to↶(H ∪ evt(x)) ↶ ((T ∩ S ⋅ π) ∪ E ∪ S ⋅ π).

(40)

By (29), it suffices to show that

= (H ∪ evt(x)) ↶ S,

For all a ∈ (H ∪ evt(x)) ∩ S ⋅ π, let us show that a ∈ (T ∩S ⋅ π) ∪ E:
– if a ∈ E, we conclude directly,– if a ∈ (H ∩ T ) ∪ supp(x, ϕ, ρ), then we conclude bysupp(x, ϕ, ρ) ⊆ T ,– otherwise a ∈ S ⋅ π ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ) ∪ E), but
S ⋅ π ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ) ∪ E)

by (29).

For the last equation, it suffices to show that(H ∪ evt(x)) ∩ S ⊆ T ∪ H,
which follows directly from evt(x) ⊆ T .
This completes the proof of (41), which implies that(((H↶T )∪evt(x))↶S) D
y ∈ LψMρ, hence x ∈ L◇ψMH↶Tasρ
required.
This completes the proof of Theorem 4.
↶(H ∪ evt(x)) ∩ S ⋅ π ⊆ (T ∩ S ⋅ π) ∪ E.

= S ⋅ π ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ) ∪ D) ⋅ π= (supp(y) ∖ ((H ∩ T ) ∪ supp(x, ϕ, ρ) ∪ D)) ⋅ π

A PPENDIX CP ROOF OF L EMMA 6

by (iv), (vi), and the definition of S. But, by (v), this isdisjoint from H ∪ evt(x), so there is no such a.
By (40), (39) can be rewritten as

It is enough to show that for every relevant tuple(ψ, ρ, (n, H)), and for every free variable X in ψ, the function
ρ(X) ∶ (N × Pfin A) → PK has a support of size at mosty ⋅ π ∈ LψM(H∪evt(x))↶U,ρM ⋅ (max-var-supp(ϕ) + max-subf-supp(ϕ)),

for U = (T ∩ S ⋅ π) ∪ E ∪ S ⋅ π. Then U ⊇ S ⋅ π = supp(y ⋅π, ψ, ρ) by definition and (38), so we may use the inductive
assumption about ψ and y ⋅ π to conclude
H∪evt(x)y ⋅ π ∈ JψKξ
H

therefore x ∈ JϕKξ as required.
We now turn attention to the right-to-left implication of (37).
H∪evt(x). Define
Assume that x Ð→ y for some y ∈ JψKξ
S = supp(y, ϕ, ρ); by the inductive assumption about ψ wehavey ∈ LψM(H∪evt(x))↶S.
ρ
We want to show that x ∈ L◇ψMρH↶T . To this end we shallchoose a set D as prescribed by the definition of L◇ψM, sothat↶(H ∪ evt(x)) ↶ S = (((H ↶ T ) ∪ evt(x)) ↶ S)

D. (41)

DefineD = (H ∖ T ) ∩ S.
Obviously ∣D∣ ≤ ∣H ∖ T ∣. Moreover, since D is disjoint fromT , it is also disjoint from(H ∩ T ) ∪ supp(x, ϕ, ρ),

where M is the number of fixpoint operators that surroundψ in ϕ. This is proved by induction on the definition of theset of relevant tuples. All cases are evident except the one forµX.ψ. For this case, making the inductive assumption about(µX.ψ, ρ, (n, H)), prove by induction on α that every Φαis supported by the set supp(ρ, X, ψ). As a result, also eachρ[X ↦ Φα ] is supported by that set, which is of size at most
(M + 1) ⋅ (max-var-supp(ϕ) + max-subf-supp(ϕ))
as required.