Logical Methods in Computer Science
Vol. 12(1:7)2016, pp. 1–32
www.lmcs-online.org

Submitted
Published

Sep. 10, 2015
Mar. 31, 2016

HISTORY-REGISTER AUTOMATA
RADU GRIGORE a AND NIKOS TZEVELEKOS b
a

University of Kent
e-mail address: radugrigore@gmail.com

b

Queen Mary University of London
e-mail address: nikos.tzevelekos@qmul.ac.uk

Abstract. Programs with dynamic allocation are able to create and use an unbounded
number of fresh resources, such as references, objects, files, etc. We propose History-Register
Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs
extend the expressiveness of previous approaches and bring us to the limits of decidability
for reachability checks. The distinctive feature of our machines is their use of unbounded
memory sets (histories) where input symbols can be selectively stored and compared with
symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We
show that the combination of consumption and reset capabilities renders the automata
powerful enough to imitate counter machines, and yields closure under all regular operations
apart from complementation. We moreover examine weaker notions of HRAs which strike
different balances between expressiveness and effectiveness.

1. Introduction
Program analysis faces substantial challenges due to its aim to devise finitary methods and
machines which are required to operate on potentially infinite program computations. A
specific such challenge stems from dynamic generative behaviours such as, for example,
object or thread creation in Java, or reference creation in ML. A program engaging in such
behaviours is expected to generate a possibly unbounded amount of distinct resources, each
of which is assigned a unique identifier, a name. Hence, any machine designed for analysing
such programs is expected to operate on an infinite alphabet of names. The latter need has
brought about the introduction of automata over infinite alphabets in program analysis,
starting from prototypical machines for mobile calculi [27] and variable programs [23], and
recently developing towards automata for verification tasks such as equivalence checks of
ML programs [29, 30], context-bounded analysis of concurrent programs [10, 3] and runtime
program monitoring [20].
The literature on automata over infinite alphabets is rich in formalisms each based
on a different approach for tackling the infiniteness of the alphabet in a finitary manner
(see e.g. [36] for an overview). A particularly intuitive such model is that of Register
2012 ACM CCS: [Theory of computation]: Formal languages and automata theory.
Key words and phrases: register automata, automata over infinite alphabets, infinite systems reachability,
freshness, counter automata.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

c
DOI:10.2168/LMCS-12(1:7)2016

CC

R. Grigore and N. Tzevelekos
Creative Commons

2

R. GRIGORE AND N. TZEVELEKOS

q0

P
∅, 1
1, 2

O
O

P

The automaton starts at state q0 with empty history and nondeterministically makes a transition to state P or Q, accepting
the respective symbol. From state P , it accepts any input name
a which does not appear in any of its histories (this is what ∅
stands for), puts it in history number 1, and moves back to q0 .
From state O, it accepts any input name a which appears in
history number 1, puts it in history number 2, and moves back
to q0 .
Figure 1: History-register automaton accepting L0 .

Automata (RA) [23, 31], which are machines built around the concept of an ordinary finitestate automaton attached with a fixed finite amount of registers. The automaton can store
in its registers names coming from the input, and make control decisions by comparing new
input names with those already stored. Thus, by talking about addresses of its memory
registers rather than actual names, a so finitely-described automaton can tackle the infinite
alphabet of names. Driven by program analysis considerations, register automata have been
recently extended with the feature of name-freshness recognition [38], that is, the capability
of the automaton to accept specific inputs just if they are fresh — they have not appeared
before during computation. Those automata, called Fresh-Register Automata (FRA), can
account for languages like the following,
L0 = {a1 . . . an ∈ N ∗ | ∀i 6= j. ai 6= aj }
which captures the output of a fresh-name generator (N is a countably infinite set of names).
FRAs are expressive enough to model, for example, finitary fragments of languages like the
π-calculus [38] or ML [29].
The freshness oracle of FRAs administers the automata with perhaps too restricted an
access to the full history of the computation: it allows them to detect name freshness, but
not non-freshness. Consider, for instance, the following simple language,
L0 = {w ∈ ({O, P } × N )∗ | each letter of w appears exactly once in it
∧ each (O, a) in w is preceded by some (P, a) }
where the alphabet is made of pairs containing an element from the set {O, P } and a name
(O and P can be seen as different processes or agents exchanging names). The language L0
represents a paradigmatic scenario of a name generator P coupled with a name consumer O:
each consumed name must have been created first, and no name can be consumed twice. It
can capture e.g. the interaction of a process which creates new files with one that opens
them, where no file can be opened twice. The inability of FRAs to detect non-freshness, as
well as the fact that names in their history cannot be removed from it, do not allow them
to express L0 . More generally, the notion of re-usage or consumption of names is beyond
the reach of those machines. Another limitation of FRAs is the failure of closure under
concatenation, interleaving and Kleene star.
Aiming at providing a stronger theoretical tool for analysing computation with names,
in this work we further capitalise on the use of histories by effectively upgrading them
to the status of registers. That is, in addition to registers, we equip our automata with
a fixed number of unbounded sets of names (histories) where input names can be stored
and compared with names to follow. As histories are internally unordered, the kind of

HISTORY-REGISTER AUTOMATA

3

FRA

unary HRA

HRA

RA

non-reset
HRA

DA / CMA

Figure 2: Expressiveness of history-register automata compared to previous models (in
italics). The inclusion M −→ M0 means that for each A ∈ M we can effectively
construct an A0 ∈ M0 accepting the same language as A. All inclusions are strict.
name comparison we allow for is name belonging (does the input name belong to the i-th
history? ). Moreover, names can be selected and removed from histories, and individual
histories can be emptied/reset. We call the resulting machines History-Register Automata
(HRA). For example, L0 is accepted by the HRA with 2 histories depicted in Figure 1, where
by convention we model pairs of symbols by sequences of two symbols.1
The strengthening of the role of histories substantially increases the expressive power of
our machines. More specifically, we identify three distinctive features of HRAs:
(1) the capability to reset histories;
(2) the use of multiple histories;
(3) the capability to select and remove individual names from histories.
Each feature allows us to express one of the paradigmatic languages below, none of which
are FRA-recognisable.
L1 = {a0 w1 . . . a0 wn ∈ N ∗ | ∀i. wi ∈ N ∗ ∧ a0 wi ∈ L0 } for given a0
L2 = {a1 a01 . . . an a0n ∈ N ∗ | a1 . . . an , a01 . . . a0n ∈ L0 }
L3 = {a1 . . . an a01 . . . a0n0 ∈ N ∗ | a1 . . . an , a01 . . . a0n0 ∈ L0 ∧ ∀i.∃j. a0i = aj }
Apart from the gains in expressive power, the passage to HRAs yields a more well-rounded
automata-theoretic formalism for generative behaviours as these machines enjoy closure under
all regular operations apart from complementation. On the other hand, the combination of
features (1-3) above enables us to use histories as counters and simulate counter machines. We
therefore obtain non-primitive recursive bounds for checking language emptiness. Given that
language containment and universality are undecidable already for register automata [31],
HRAs are fairly close to the decidability boundary for properties of languages over infinite
alphabets. Nonetheless, starting from HRAs and weakening them in each of the first two
factors (1,2) we obtain automata models which are still highly expressive but computationally
more tractable. Overall, the expressiveness hierarchy of the machines we examine is depicted
in Figure 2 (weakening in (1) and (2) respectively occurs in the second column of the figure).
Motivation and related work. The motivation for this work stems from semantics and
verification. In semantics, the use of names to model resource generation originates in the
work of Pitts and Stark on the ν-calculus [32] and Stark’s PhD [37]. Names have subsequently
been incorporated in the semantics literature (see e.g. [21, 4, 1, 24]), especially after the advent
1Although, technically speaking, the machines we define below do not handle constants (as e.g. O, P ), the
latter are encoded as names appearing in initial registers, in standard fashion.

4

R. GRIGORE AND N. TZEVELEKOS

of Nominal Sets [18], which provided formal foundations for doing mathematics with names.
Moreover, recent work in game semantics has produced algorithmic representations of game
models using extensions of fresh-register automata [29, 30, 28], thus achieving automated
equivalence checks for fragments of ML and Java. In a parallel development, a research
stream on automated analysis of dynamic concurrent programs has developed essentially
the same formalisms, this time stemming from trace-based operational techniques [10, 3].
This confluence of different methodologies is exciting and encourages the development of
stronger automata for a wider range of verification tasks, and just such an automaton we
examine herein.
Although our work is driven by program analysis, the closest existing automata models
to ours come from XML database theory and model checking. Research in the latter area has
made great strides in the last years on automata over infinite alphabets and related logics
(e.g. see [36] for an overview from 2006). As we show in this paper, history-register automata
fit very well inside the big picture of automata over infinite alphabets (cf. Figure 2) and in
fact can be seen as closely related to Data Automata (DA) [7] or, equivalently, Class Memory
Automata (CMA) [5]. A crucial difference lies in the reset capabilities of our machines, which
allow us to express languages like L1 that cannot be expressed by DA/CMAs. On the other
hand, the local termination conditions of DA/CMAs allow them to express languages that
HRAs cannot capture. We find the correspondence between HRAs and DAs particularly
pleasing as it relates two seemingly very different kind of machines, with distant operational
descriptions and intuitions.
A recent strand of research in foundations of atom-based computation [6, 9, 8] has
examined nominal variants of classical machine models, ranging from finite-state automata
to Turing machines. Finally, since the publication of the conference version of this paper [39],
there has been work in nested DA/CMAs [14, 13], which can be seen as extensions of
non-reset HRAs whereby the histories satisfy some nesting relations. The latter are a clean
extension of our machines, leading to higher reachability complexities.
This article is the journal version of [39], with strengthened results and with full proofs.
Section 4 is new: it collects all results that show how registers can be simulated by other
means. Many upper bounds are tighter: Propositions 4.1, 4.4, 5.4, 6.2, 6.8. Some results are
new: Propositions 4.5, 4.7, 5.6, 6.10. Example 4.3 is new. Most proofs have been revised.
Section 7 is new: it collects in one place the main properties of HRAs. Also, we relate our
work to what has been done after the conference version was published.
Overview. In Section 2 we introduce HRAs and their basic properties. In Section 3 we
examine regular closure properties of HRAs. In Section 4 we explain how registers can
be simulated by other means, such as histories. In Section 5 we prove that emptiness is
Ackermann-complete. In Section 6 we introduce weaker models, and study their properties.
In Section 7 we summarize the main properties of HRAs. In Section 8 we connect HRAs to
existing automata formalisms. We conclude by discussing future directions which emanate
from this work.
2. Definitions and first properties
We start by fixing some notation. Let N be a countably infinite alphabet of names, over
which we range by a, b, c, etc. For any pair of natural numbers i ≤ j, we write [i, j] for the
set {i, i+1, . . . , j}, and for each i we let [i] be the set {1, . . . , i}. For any set S, we write |S|

HISTORY-REGISTER AUTOMATA

5

for the cardinality of S, we write P(S) for the powerset of S, we write Pfn (S) for the set
of finite subsets of S, and we write P6=∅ (S) for the set of nonempty subsets of S. We write
id : S → S for the identity function on S, and img(f ) for the image of f : S → T .
We define automata which are equipped with a fixed number of registers and histories
where they can store names. Each register is a memory cell where one name can be stored at
a time; each history can hold an unbounded set of names. We use the term place to refer to
both histories and registers. Transitions are of two kinds: name-accepting transitions and
reset transitions. Those of the former kind have labels of the form (X, X 0 ), for sets of places
X and X 0 ; and those of the latter carry labels with single sets of places X. A transition
labelled (X, X 0 ) means:
• accept name a if it is contained precisely in places X, and
• update places in X and X 0 so that a be contained precisely in places X 0 after the transition
(without touching other names).
By a being contained precisely in places X we mean that it appears in every place in X,
and in no other place. In particular, the label (∅, X 0 ) signifies accepting a fresh name (one
which does not appear in any place) and inserting it in places X 0 . On the other hand, a
transition labelled by X resets all the places in X; that is, it updates each of them to the
empty set (registers are modelled as sets with at most one element). Reset transitions do
not accept names; they are -transitions from the outside. Note that the label (X, ∅) has
different semantics from the label X: the former stipulates that a name appearing precisely
in X be accepted and then removed from X; whereas the latter clears all the contents of
places in X, without accepting anything.
2.1. Definitions. Formally, let us fix positive integers m and n which will stand for the
default number of histories and registers respectively in the machines we define below. The
set Asn of assignments and the set Lab of labels are:
Asn = { H : [m + n] → Pfn (N ) | ∀i > m. |H(i)| ≤ 1 }
Lab = P([m + n])2 ∪ P([m + n])
For example, {(i, ∅) | i ∈ [m+n]} is the empty assignment.2 We range over elements of Asn
by H and variants, and over elements of Lab by ` and variants.
Let H ∈ Asn be an assignment, let a ∈ N be a name, let S ⊆ N be a set of names, and
let X ⊆ [m + n] be a set of places. We introduce the following notation:
• We set H@X
to be the
T
S set of names which appear preciselySin places X in H; that is,
H@X = i∈X H(i) \ i∈X
/ H(i). In particular, H@ ∅ = N \ i H(i) is the set of names
which do not appear in H.
• H[X 7→ S] is the update H 0 of H so that all places in X are mapped to S; that is,
H 0 = {(i, H(i)) | i 6∈ X} ∪ {(i, S) | i ∈ X}. E.g., H[X 7→ ∅] resets all places in X.
• H[a in X] is the update of H which removes name a from all places and inserts it back
in X; that is, H[a in X] is the assignment:
{(i, H(i) ∪ {a}) | i ∈ X ∩ [m]} ∪ {(i, {a}) | i ∈ X \ [m]} ∪ {(i, H(i) \ {a}) | i ∈
/ X}
Note above that operation H[a in X] acts differently in the case of histories (i ≤ m) and
registers (i > m) in X: in the former case, the name a is added to the history H(i), while
in the latter the register H(i) is set to {a} and its previous content is cleared.
2We represent functions as sets of pairs.

6

R. GRIGORE AND N. TZEVELEKOS

We can now define our automata.
Definition 2.1. A history-register automaton (HRA) of type (m, n) is a tuple A =
hQ, q0 , H0 , δ, F i where:
• Q is a finite set of states, q0 is the initial state, F ⊆ Q are the final ones,
• H0 ∈ Asn is the initial assignment, and
• δ ⊆ Q × Lab × Q is the transition relation.
For brevity, we shall call A an (m, n)-HRA.
X,X 0

X

We write transitions in the forms q −→ q 0 and q −→ q 0 , for each kind of transition label.
In diagrams, we may unify different transitions with common source and target, for example
X,X 0

X,X 0 / Y,Y 0

Y,Y 0

q −→ q 0 and q −→ q 0 may be written q −−−−−−−→ q 0 ; moreover, we shall lighten notation
and write i for the singleton {i}, and ij for {i, j}.
We already gave an overview of the semantics of HRAs. This is formally defined by
means of configurations representing the current computation state of the automaton. A
configuration of A is a pair (q, H) ∈ Q̂, where:
Q̂ = Q × Asn
From the transition relation δ we obtain the configuration graph of A as follows.
Definition 2.2. Let A be an (m, n)-HRA as above. Its configuration graph (Q̂, −→),

x
where −→ ⊆ Q̂ × N ∪ {} × Q̂, is constructed by setting (q, H) −→ (q 0 , H 0 ) if and only
if one of the following conditions is satisfied.
X,X 0

• x = a ∈ N and there is q −→ q 0 ∈ δ such that a ∈ H@X and H 0 = H[a in X 0 ].
X

• x =  and there is q −→ q 0 ∈ δ such that H 0 = H[X 7→ ∅].
The language accepted by A is
w

L(A) = { w ∈ N ∗ | (q0 , H0 ) −→
−→ (q, H) and q ∈ F }
x1 ...x

x

x

k
1
k
where −→
−→ is the reflexive transitive closure of −→ (i.e. q̂ −−−−→
→
q̂ 0 if q̂ −→
· · · −→
q̂ 0 ).

Note that we use  both for the empty sequence and the empty transition so, in particular,
when writing sequences of the form x1 . . . xk we may implicitly consume ’s. It is worth
noting here that our formulation follows M-automata [23] in that multiple places can be
mentioned at each transition.
Example 2.3. The language L1 of the Introduction is recognised by the following (1, 1)HRA (leftmost below), with initial assignment {(1, ∅), (2, a0 )}. The automaton starts by
accepting a0 , leaving it in register 2, and moving to state q1 . There, it loops accepting fresh
names (appearing in no place) which it stores in history 1. From q1 it goes back to q0 by
resetting its history.
∅,1 / 2,12

∅,1

q0

2,2
1

q1

q0

1,∅

∅,1

q1

q0

1,∅

q1

∅,2 / 1,12

We can also see that the other two HRAs, of type (2, 0) and (1, 0), accept the languages L2
and L3 respectively. Both automata start with empty assignments.

HISTORY-REGISTER AUTOMATA

7

Finally, the automaton we drew in Figure 1 is, in fact, a (2,2)-HRA where its two registers
initially contain the names O and P respectively. The transition label O corresponds to
(3, 3), and P to (4, 4).
As mentioned in the introductory section, HRAs build upon (Fresh) Register Automata [23, 31, 38]. The latter can be defined within the HRA framework as follows.3
Definition 2.4. A Register Automaton (RA) of n registers is a (0, n)-HRA with no
reset transitions. A Fresh-Register Automaton
(FRA) of n registers is a (1, n)-HRA
S
A = hQ, q0 , H0 , δ, F i such that H0 (1) = i H0 (i) and:
• for all (q, `, q 0 ) ∈ δ, there are X, X 0 such that ` = (X, X 0 ) and 1 ∈ X 0 ;
• for all (q, {1}, X 0 , q 0 ) ∈ δ, there is also (q, ∅, X 0 , q 0 ) ∈ δ.
Thus, in an FRA all the initial names must appear in its history, and the same holds
for all the names the automaton accepts during computation (1 ∈ X 0 ). As, in addition, no
reset transitions are allowed, the history effectively contains all names of a run. On the
other hand, the automaton cannot recognise non-freshness: if a name appearing only in the
history is to be accepted at any point then a totally fresh name can be also be accepted in
the same way. Now, from [38] we have the following.
Lemma 2.5. The languages L1 , L2 and L3 are not FRA-recognisable.
Proof. L1 was explicitly examined in [38]. For L2 and L3 we use a similar argument as the
one for showing that L0 ∗ L0 is not FRA-recognisable [38] .
2.2. Bisimulation. Bisimulation equivalence, also called bisimilarity, is a useful tool for
relating automata, even from different paradigms. It implies language equivalence and is
generally easier to reason about than the latter. We will be using it avidly in the sequel.
Definition 2.6. Let Ai = hQi , q0i , H0i , δi , Fi i be (m, n)-HRAs, for i = 1, 2. A relation
R ⊆ Q̂1 × Q̂2 is called a simulation on A1 and A2 if, for all (q̂1 , q̂2 ) ∈ R,




• if q̂1 −→
−→ q̂10 and π1 (q̂10 ) ∈ F1 then q̂2 −→
−→ q̂20 for some π1 (q̂20 ) ∈ F2 , where π1 is the first
projection function;

a

a
• if q̂1 −→
−→ · −→ q̂10 then q̂2 −→
−→ · −→ q̂20 for some (q̂10 , q̂20 ) ∈ R.
R is called a bisimulation if both R and R−1 are simulations. We say that A1 and A2 are
bisimilar, written A1 ∼ A2 , if ((q01 , H01 ), (q02 , H02 )) ∈ R for some bisimulation R.
Lemma 2.7. If A1 ∼ A2 then L(A1 ) = L(A2 ).
2.3. Determinism. We close our presentation here by describing the deterministic class of
HRAs. We defined HRAs in such a way that, at any given configuration (q, H) and for any
input symbol a, there is at most one set of places X that can match a, i.e. such that a ∈ H@X.
As a result, the notion of determinism in HRAs can be ensured by purely syntactic means.
X1
Xn 0
X
Below we write q −→
−→ q 0 ∈ δ if there is a sequence of transitions q −→
· · · −→
q in δ such
Sn
∅
that X = i=1 Xi . In particular, q −→
−→ q ∈ δ.
3The definitions given in [23, 31, 38] are slightly different but can routinely be shown equivalent.

8

R. GRIGORE AND N. TZEVELEKOS

Definition 2.8. We say that an HRA A is deterministic when, for any reachable config
a

a
uration q̂ and any name a, if q̂ −→
−→ · −→ q̂1 and q̂ −→
−→ · −→ q̂2 then q̂1 = q̂2 . We say that an
HRA A is strongly deterministic when, for any state q and any sets X, X1 , X2 , Y1 , Y2 ,
Y

X\Y1 ,X1

Y

X\Y2 ,X2

1
2
if q −→
−→
· −−−−−→ q1 ∈ δ and q −→
−→
· −−−−−→ q2 ∈ δ then q1 = q2 , Y1 = Y2 and X1 = X2 .

Even if A is deterministic, it is still possible to have multiple paths in the configuration
graph that are labeled by the same word. However, such paths may only differ in their
-transitions. In the definition of ‘strongly deterministic’, the set X is guessing where the
name a occurs.
Lemma 2.9. If A is strongly deterministic then it is deterministic.

3. Closure properties
History-register automata enjoy good closure properties with respect to regular language
operations. In particular, they are closed under union, intersection, concatenation and
Kleene star, but not closed under complementation.
In fact, the design of HRAs is such that the automata for union and intersection
come almost for free through a straightforward product construction which is essentially
an ordinary product for finite-state automata, modulo reindexing of places to account for
duplicate labels (cf. [23]). The constructions for Kleene star and concatenation are slightly
more involved as there is need for passing through intermediate automata which do not
touch their initial names.
We shall need the following technical gadget. Given an (m, n)-HRA A and a sequence
w of k distinct names, we construct a bisimilar (m, n+k)-HRA, denoted A fix w, in which
the names of w appear exclusively in the additional k registers, which, moreover, remain
unchanged during computation. The construction will allow us, for instance, to create
feedback loops in automata ensuring that after each feedback transition the same initial
configuration occurs.
Lemma 3.1. Let A be an (m, n)-HRA with initial assignment H0 and w = a1 . . . ak a
sequence of distinct names. We can effectively construct an (m, n+k)-HRA A fix w with
initial assignment H00 such that A fix w ∼ A and:
• H00 (m+n+i) = ai for all i ∈ [k], and H00 (i) = H0 (i) \ {a1 , . . . , ak } for all i ∈ [m+n];
• for all reachable configurations (q, H) of A fix w and all i > m+n, H(i) = H00 (i).
Proof. We construct A fix w = hQ0 , q00 , H00 , δ 0 , F 0 i as follows. First, we insert/move all names
of w to the new registers (places [m+n+1, m+n+k]), i.e. we set H00 (i) = H0 (i) \ {a1 . . . ak }
for all i ∈ [m+n], and H00 (m+n+i) = {ai } for each i ∈ [k]. The role of the new registers is
to constantly store the names in w and act on the behalf of other places when the latter
intend to use those names: during computation, whenever an ai is captured by a transition
of the initial automaton A, in A fix w it will be instead simulated by a transition involving
the new registers. In order for the simulation to be accurate, we shall inject inside states
information specifying the intended location of the ai s in the places of A. Thus, the states
of the new automaton are pairs (q, f ), where q ∈ Q and f is a function recording, for each
of the new registers, where would the name of the register appear in the original automaton
A. That is,
Q0 = Q × {f : [k] → P([m+n]) | ∀j 6= j 0. f (j) ∩ f (j 0 ) ⊆ [m]}

HISTORY-REGISTER AUTOMATA

9

while q00 = (q0 , {(i, {j | ai ∈ H0 (j)}) | i ∈ [k]}) and F 0 = {(q, f ) ∈ Q0 | q ∈ F }. Finally, δ 0
operates just like δ albeit taking into account the f ’s of states to figure out the intended
positions of the ai s and, at the same time, update the f ’s after each transition. We therefore
include in δ 0 precisely the following transitions. Below we write i◦ for m+n+i. For each
X,X 0

(q, f ) ∈ Q0 and q −→ q 0 ∈ δ,
X,X 0

• add a transition (q, f ) −→ (q 0 , f );
{i◦ },{i◦ }

• if f (i) = X for some i then add (q, f ) −−−−−→ (q 0 , f 0 ) where f 0 = f [i 7→ X 0 ];
X

X

Moreover, for each q −→ q 0 ∈ δ include (q, f ) −→ (q 0 , f 0 ) where f 0 = {(j, f (j) \ X) | j ∈ [k]}.
Following the above line of reasoning, we can show that the relation
{((q, H), (q, f, H 0 )) | ∀i ∈ [m+n]. H(i) = H 0 (i) ∪ {aj | i ∈ f (j)}}
with (q, H), (q, f, H 0 ) reachable configurations, is a bisimulation.
We write L ◦ L0 for concatenation of languages, and L∗ for Kleene closure of a language.
We use the same definitions as the standard ones for languages over finite alphabets: L ◦ L0
is { ww0 | w ∈ L ∧ w0 ∈ L0 }, and L∗ is the least fixed-point of the equations  ∈ L∗
and L∗ ◦ L ⊆ L∗ , where  is the empty word.
Proposition 3.2. Languages recognised by HRAs are closed under union, intersection,
concatenation and Kleene star.
Proof. We show concatenation and Kleene star only. For the former, consider HRAs
Ai = hQi , q0i , H0i , δi , Fi i, i = 1, 2, and assume wlog that they have common type (m, n). Let
w be an enlistment of all names in H02 and construct A0i = Ai fix w, for i = 1, 2. Then, the
concatenation L(A1 ) ◦ L(A2 ) is the language recognised by connecting A01 and A02 serially,
that is, the automaton obtained by connecting each final state of A01 to the initial state of A02
with a transition labelled [m+n], and with initial/final states those of A01 /A02 respectively.
Finally, given an (m, n)-HRA A and an enlistment w of its initial names, we construct
an automaton A0 by connecting the final states of A fix w to its initial state with a transition
labelled [m+n]. We can see that L(A0 ) = L(A)∗ .
As we shall next see, while universality is undecidable for HRAs, their emptiness problem
can be decided by reduction to coverability for transfer-reset vector addition systems. In
combination, these results imply that HRAs cannot be effectively complemented. In fact,
there are HRA-languages whose complements are not recognisable by HRAs. This can be
shown via the following example, adapted from [26].
Lemma 3.3. HRAs are not closed under complementation.
Example 3.4. Consider L4 = {w ∈ N ∗ | not all names of w occur exactly twice in it },
which is accepted by the (2, 0)-HRA below.
∅,1 / 1,1

∅,1 / 1,1

q0

∅,2

q1

∅,1 / 1,1

∅,1 / 1,1
2,2

q2

2,1

q3

The automaton non-deterministically selects an input name which either appears only once
in the input or at least three times. We claim that L4 , the language of all words whose
names occur exactly twice in them, is not HRA-recognisable.

10

R. GRIGORE AND N. TZEVELEKOS

Proof. Suppose it were recognisable (wlog, Proposition 4.1) by an (m, 0)-HRA A with k
states. Then, A would accept the word w = a1 . . . ak a1 . . . ak where all ai ’s are distinct and
do not appear in the initial assignment of A. Let p = p1 p2 be the path in A through which w
is accepted, with each pi corresponding to one of the two halves of w. Since all ai s are fresh for
A, the non-reset transitions of p1 must carry labels of the form (∅, X), for some sets X. Let
q be a state appearing twice in p1 , say p1 = p11 (q)p12 (q)p13 . Consider now the path p0 = p01 p2
where p01 is the extension of p1 which repeats p12 , that is, p01 = p11 (q)p12 (q)p12 (q)p13 . We
claim that p0 is an accepting path in A. Indeed, by our previous observation on the labels of
X,Y

p1 , the path p01 does not block, i.e. it cannot reach a transition q1 −−→ q2 , with X 6= ∅, in
some configuration (q1 , H1 ) such that H1 @X = ∅. We need to show that p2 does not block
either (in p0 ). Let us denote (q, H1 ) and (q, H2 ) the configurations in each of the two visits
of q in the run of p on w; and let us write (q, H3 ) for the third visit in the run of p01 , given
that for the other two visits we assume the same configurations as in p. Now observe that,
for each nonempty X ⊆ [m], repeating p12 cannot reduce the number of names appearing
precisely in X, therefore |H2 @X| ≤ |H3 @X|. The latter implies that, since p does not block,
p0 does not block either. Now observe that any word accepted by w0 is not in L4 , as p01
accepts more than k distinct names, a contradiction.

4. Removing Registers
Although registers are convenient for expressing some languages (Example 4.2 and Example 4.3), when reasoning about HRAs it is more convenient to focus on histories only. In
this section, we show that this approach is sound and in particular we present three ways of
removing registers:
• we can construct a bisimilar automaton if we are allowed to use extra histories and resets;
• we can preserve language if we are allowed to use extra histories (but no resets);
• we can preserve emptiness if we are allowed to use extra states (but no histories nor
resets).
Each of these constructions will be useful in the sequel either for devising emptiness checks
and, more generally, they demonstrate that registers can be considered as a derivative notion.
4.1. Simulating Registers with Histories and Resets. The semantics of registers is
very similar to that of histories. The main difference is that registers are forced to contain
at most one name. To simulate registers with histories, we reset histories before inserting
names. Resetting histories might cause the automaton to forget names that are necessary
for deciding how to proceed. The solution is to use two histories for each register: one holds
the old name, the other holds the new name. Only the history where the new name will be
written needs to be reset.
Proposition 4.1. Let A = hQ, q0 , H0 , δ, F i be an (m, n)-HRA. We can construct an (m +
0
n
2n, 0)-HRA A0 = hQ0 , q00 , H00 , δ 0 , F 0 i that is bisimilar to A. We have |Q
 | ∈ O(2 |Q|) and
0
n
0
0
|δ | ∈ O(2 |δ|). The construction can be done in O (m + n)(|Q | + |δ |) time.
Proof. For each q in Q, we include 2n states (q, f ) in Q0 , where f : [n] → [2n] is such that
f (i) ∈ {i, i + n} for all i. The name that A holds in register i will be found in history m + f (i)
of A0 . We set f¯ to be the complement of f ; that is, f¯(i) , n + 2i − f (i). Let f † (i) be i if
i ∈ [m] and m + f (i) otherwise. Moreover, q00 = (q0 , id), F 0 = {(q, f ) | q ∈ F }, and H00 is

HISTORY-REGISTER AUTOMATA

11

H0 extended so that H00 (i) = ∅ for all i > m + n. Finally, we include in δ 0 precisely the
following transitions.
X,X 0

Y

f † (X),f¯† (X 0 )

• For each q −→ q 0 ∈ δ, add (q, f ) −→ · −−−−−−−−→ (q 0 , f 0 ) where Y = [m+1, m+2n] \
img(f ), and f 0 is given by: f 0 (i) = f¯(i) if i ∈ X ∪ X 0 and f 0 (i) = f (i) otherwise. (Note
that we need a few extra states in Q0 , which remain nameless in this proof.)
f † (X)

X

• For each q −→ q 0 ∈ δ, add (q, f ) −−−−→ (q 0 , f ).
The relation { ((q, H), ((q, f ), H 0 )) | H = H 0 ◦ f † } witnesses bisimilarity.
4.2. Replacing Registers with Histories using Colours. The result of Proposition 4.1
comes at the cost of introducing reset transitions even if the original automaton does not
have such transitions. Reset transitions are undesirable because they increase the complexity
of the emptiness problem (Section 5). We can avoid introducing reset transitions by using the
colouring technique of [5]. The construction is more involved and the resulting automaton is
not bisimilar to the original, but it is language equivalent.
Before we proceed with the proof, let us illustrate the technique on two examples.
Example 4.2 illustrates how to check that a name is not in the simulated register; Example 4.3
illustrates also how to check that a name is in the simulated register.
Example 4.2. The language
L5 = { a1 . . . an | ai 6= ai+1 for all i }
is recognized by both of the automata below (with histories initially empty):
∅,1 / 2,1

q0

∅,1

∅,2 / 2,2

q0

∅,2 / 1,2

q1
∅,1 / 1,1

The one on the left is a (0, 1)-HRA, and we can straight away see its accepted language
is L5 . The one on the right is a (2, 0)-HRA for which it is less clear why it accepts L5 . The
reason is the following invariant:
• H(1) ] H(2) is a partition of all names seen so far; and
• if the state is qk then the last seen name is in H(k + 1), for k ∈ {0, 1}; and
• all possible partitions of the names are realisable.
The first two points are easy to check. Because all transitions have labels of the form (X, {i}),
all seen names are remembered in precisely one history. Because all transitions incoming
into qk have labels the form (X, {k + 1}), the last seen name is remembered in H(k + 1).
The consequence of these first two points is that the automaton on the right accepts a name
only if it is different from the last seen name. Indeed, all transitions outgoing from qk have
labels of the form (X, X 0 ) with k + 1 ∈
/ X. Thus, the first two points should be seen as
lemmas which let us establish that all words accepted by the automaton on the right belong
to L5 .
Informally, the third point is the key lemma that lets us establish the converse, that all
words in L5 are accepted. However, to see why this is so, we need to rephrase it in a more
formal way. Given a word a1 . . . an ∈ L5 , we consider an arbitrary partition H(1) ] H(2)
of the set {a1 , . . . , an }. Without loss of generality, assume an ∈ H(1). The claim is that

12

R. GRIGORE AND N. TZEVELEKOS

there exists a run of the automaton on the right that accepts the word a1 . . . an and ends in
configuration (q0 , H). We can prove this by induction. If an−1 ∈ H(k + 1) then the previous
state in the run must have been qk , for k ∈ {0, 1}. Suppose an−1 ∈ H(2); the other case is
symmetric. Then, by the induction hypothesis, we know that there is a run that accepts the
word a1 . . . an−1 and ends in configuration (q1 , H 0 ), where we choose
(
H(1) \ {an } if an ∈
/ {a1 , . . . , an−1 }
H 0 (1) ,
H 0 (2) , H(2) \ {an }
H(1) ∪ {an } if an ∈ {a1 , . . . , an−1 }
It is clear that H 0 (1) ] H 0 (2) is a partition of {a1 , . . . , an−1 }, as required. Finally, we need
an
to show that (q1 , H 0 ) −→
(q0 , H) belongs to the configuration graph. If an ∈
/ {a1 , . . . , an−1 },
∅,1

then this is true because of q1 −→ q0 ; if an ∈ {a1 , . . . , an−1 }, then this is true because of
1,1

q1 −→ q0 .
Example 4.3. The language
L6 = { a1 . . . an | ai = ai+1 iff i is odd }
is recognized by both of the following automata:
∅,1 / 3,1

q2

∅,1

q0

q1

q0

∅,1

q1

1,2
1,3

1,1
∅,1 / 2,1

q3

The one on the left is a (0, 1)-HRA, while the one on the right is a (3, 0)-HRA. As in
the previous example, the fact that the (3, 0)-HRA accepts L6 is not immediately clear.
Informally, the reason is the following invariant:
• H(1) ] H(2) ] H(3) is a partition of the names seen so far;
• if the state is qk then the last seen name is in H(k), for k ∈ {1, 2, 3};
• |H(1)| = 1 in q1 , and |H(1)| = 0 otherwise; and
• for each partition H(1) ] H(2) ] H(3) that is compatible with the previous constraints,
there is a nondeterministic run that realises it.
The first two points hold for the same reasons as in Example 4.2. The third point holds
because all incoming transitions of q1 insert a name in H(1), all outgoing transitions of q1
remove a name from H(1), and all runs alternate between state q1 and some other state.
After an odd number of names was processed, the automaton is in state q1 and H(1) contains
only the last name seen. All outgoing transitions from q1 accept a name only if it is in
H(1) — in other words, if it equals the last seen name. After an even and positive number
of names was processed, the automaton is in state q2 or q3 . All outgoing transitions from q2
accept a name only if it is not in H(2), where the last seen name is; q3 acts symmetrically.
Thus, the first three points let us establish that all words accepted by the automaton on the
right belong to L6 .
As in Example 4.2, the last point lets us establish that all word in L6 are accepted.
Given that the proof of the last point is very similar to the one in Example 4.2, let us
only sketch it. Given a word a1 . . . an ∈ L6 with n > 0, we consider an arbitrary partition
H(1) ] H(2) ] H(3) of the set {a1 , . . . , an } such that H(1) ⊆ {an }. Let k be such that
an ∈ H(k). Formally, the claim of the last point is that there exists a run of the automaton

HISTORY-REGISTER AUTOMATA

13

on the right that is labelled by the word a1 . . . an and ends in the configuration (qk , H). The
case n odd and > 1 is similar to the previous example: We pick k 0 such that an−1 ∈ H(k 0 )
and
(
H(5 − k 0 ) \ {an } if an ∈
/ {a1 , . . . , an−1 }
0
0 0
0
0
0
H (1) , ∅ H (k ) , H(k ) \ {an } H (5 − k ) ,
0
H(5 − k ) ∪ {an } if an ∈ {a1 , . . . , an−1 }
Then we invoke the induction hypothesis to show there is a run that accepts a1 . . . an−1 and
ends in configuration (qk0 , H 0 ). In the case n even, we pick
H 0 (1) , {an }

H 0 (2) , H(2) \ {an }

H 0 (3) , H(3) \ {an }

and then invoke the induction hypothesis to show that there is a run that accepts a1 . . . an−1
and ends in configuration (q1 , H 0 ). We skip the case n = 1 in this proof sketch.
We are now ready for the general result, which we prove in two steps. The main
construction will be presented first and only applies to HRAs with initially empty registers.
(The correctness of the main construction requires that certain graphs are 2-colourable. The
arguments in the previous two examples can be seen as giving explicit colouring algorithms
that work in special cases.) At a second stage, we show how to initially simulate nonempty
registers at the expense of some more additional histories.
Proposition 4.4. Let A = hQ, q0 , H0 , δ, F i be an (m, n)-non-reset-HRA with registers
initially empty. We can construct an (m + 3n, 0)-non-reset-HRA A0 = hQ0 , q00 , H00 , δ 0 , F 0 i
that accepts the same language as A. We have |Q0 | ∈ O(22n · |Q|) and |δ 0 | ∈ O(23.3n · |δ|).
Proof. Each register i will be simulated by three histories, named iR , iB and iY respectively.4
Each state q ∈ Q will be simulated by several states (q, f ) ∈ Q0 , where f : [m + 1, m + n] →
{∅, R, B, Y}. The construction will ensure the following invariant:
• H(iR ) ] H(iB ) ] H(iY ) is a partition of the names that have been written to register i
and have subsequently been rewritten by other names or are still in register i;5
• |H(iR )| = 1 if f (i) = R, and |H(iR )| = 0 otherwise; and
• if f (i) 6= ∅ then the current name of register i is in H(if (i) ); register i is empty otherwise.
Thus, according to the last point above, f records in which of histories iR , iB , iY has the
current name of register i been stored. We shall instrument A0 in such a way that it will
only store that name, say a, in iR if the next time register i is being invoked by A is for
reading a. This way we shall ensure that iR never contains more than one name. Otherwise,
i.e. if A next invokes i for overwriting its contents, f will be mapping i to one of iB , iY .
These can be seen as garbage collecting histories: they contain all names that have passed
from register i and will not be immediately read from it. The reason why we need two of
these, iB and iY , is to be able to reuse old names of register i without running the risk of
confusing them with its current name a.
X,X 0

To simulate one transition q −→ q 0 , accepting say a name a, we shall use several
Z,Z 0

transitions of the form (q, f ) −→ (q 0 , f 0 ) where f and f 0 agree outside X ∪ X 0 . Let us
consider an arbitrary such pair (f, f 0 ), and see how to pick Z and Z 0 . On histories, X and Z
coincide: X ∩ [m] = Z ∩ [m]. For each register i ∈ X \ [m], we need that a be equal to the
4B and Y are the black and yellow colours of [5]; R stands for ‘read’.
5note that a name can also be transferred out of register i (via transition with label X, Y where i ∈ X \ Y ),

instead of being directly rewritten, in which case we would not store it in H(iR ) ] H(iB ) ] H(iY ).

14

R. GRIGORE AND N. TZEVELEKOS

name currently written in register i. But, we know the current name in register i only if
Z,Z 0

f (i) = R. That is why we include a transition (q, f ) −→ (q 0 , f 0 ) only if X \ [m] ⊆ f −1 (R),
and we include { iR | i ∈ X \ [m] } in Z. For each register i ∈ [m + 1, m + n] \ X, we must
ensure that a is not equal to the current name in register i, which resides in H(if (i) ). Hence,
we pick all Z such that
Z = (X ∩ [m]) ] Z1 ] Z0
where Z1 = { iR | i ∈ X \ [m] } and Z0 ⊆ { ix | i ∈ [m + 1, m + n] \ X ∧ x ∈ {B, Y} ∧ x =
6 f (i) }
is such that, for all i, |Z0 ∩ {iB , iY }| ≤ 1. Now we must write the current name to histories
X 0 ∩ [m], and we must simulate writing the current name to registers X 0 \ [m]. For each
i ∈ X 0 \ [m] we shall nondeterministically write the current name to one of iR , iB , iY by
guessing whether register i will be used next for reading or not. The place where we write is
given by f 0 (i), that is,
Z 0 = (X 0 ∩ [m]) ] { if 0 (i) | i ∈ X 0 \ [m] }.
Finally, we make sure that all i ∈ ([m + 1, m + n] ∩ X) \ X 0 in f 0 are mapped to ∅, as these
registers are now empty, i.e. we impose f 0 (([m + 1, m + n] ∩ X) \ X 0 ) ⊆ {∅}.
Thus, in summary, we take Q0 = Q × ([m + 1, m + n] → {∅, R, B, Y}) and:
0
• q0 = (q0 , {(i, ∅) | i ∈ [m + 1, m + n]}) and F 0 = F × ([m + 1, m + n] → {∅, R, B, Y});
• H00 = H0 ∪ {(i, ∅) | i ∈ [m + n + 1, m + 3n]};
Z,Z 0

X,X 0

• we include (q, f ) −→ (q 0 , f 0 ) in δ 0 just if there is some q −→ q 0 in δ such that:
– X \ [m] ⊆ f −1 (R),
– for all i ∈ [m + 1, m + n] \ (X ∪ X 0 ), f 0 (i) = f (i),
– for all i ∈ ([m + 1, m + n] ∩ X) \ X 0 , f 0 (i) = ∅,
– Z = (X ∩ [m]) ] {iR | i ∈ X \ [m]} ] Z0
with Z0 ⊆ {ix | i ∈ [m + 1, m + n] \ X ∧ x 6= f (i)},
0
– Z = (X 0 ∩ [m]) ] { if 0 (i) | i ∈ X 0 \ [m] }.
Let us now see what is the size of the HRA A0 so constructed. We have |Q0 | ∈ O(4n · |Q|).
X,X 0

Z,Z 0

For each transition q −→ q 0 in A, we introduce several transitions (q, f ) −→ (q 0 f 0 ) in A0 .
Let us count how many. There are ≤ 4n choices for f ; there are ≤ 3n choices for Z0
because for each i we pick iB , or iY , or none of them; and there are ≤ 3n choices for f 0
because f 0 (X 0 ) ⊆ {iR , iB , iY } and f 0 is uniquely determined outside X 0 . In summary,
|δ 0 | ∈ O(22(1+log2 3)n · |δ|).
Finally, we show that L(A) = L(A0 ). Let first w ∈ L(A0 ) have an accepting transition
Zk ,Z 0

path p0 in A0 with edges (qk , fk ) −→k (qk+1 , fk+1 ), for k = 1, . . . , N . Reading the definition
Xk ,X 0

of δ 0 backwards, this yields an accepting transition path p in A with edges qk −→k qk+1
where
• Xk = (Zk ∩ [m]) ∪ { i | iR ∈ Zk },
• Xk0 = (Zk0 ∩ [m]) ∪ { i | {iR , iB , iY } ∩ Zk0 6= ∅ }.
To see that p accepts w, suppose that p0 yields a sequence of configurations ((qk , fk ), Hk0 ).
Then, by induction, we can show that p yields a sequence of configurations (qk , Hk ), where:
• for all i ∈ [m], Hk (i) = Hk0 (i);
• for all i ∈ [m + 1, m + n], if fk (i) 6= ∅ then Hk (i) = {a} for some a ∈ Hk0 (ifk (i) ), otherwise
Hk (i) = ∅;
• for all names a, if a ∈ Hk0 @Zk then a ∈ Hk @Xk .

HISTORY-REGISTER AUTOMATA

15

Hence, w ∈ L(A).
Conversely, let w = a1 · · · aN ∈ L(A) have an accepting transition path p in A with edges
Xk ,X 0

qk −→k qk+1 for k = 1, . . . , N . We construct a corresponding accepting path p0 in A0 with
Zk ,Z 0

edges (qk , fk ) −→k (qk+1 , fk+1 ) as follows. We have that f0 = {(i, ∅) | i ∈ [m]}. Moreover,
Zk = (Xk ∩ [m]) ∪ Wk and Zk0 = (Xk0 ∩ [m]) ∪ Wk0 where:
(a) For each position k such that the previous appearance of ak in w is some ak0 = ak with
k 0 < k, we set Wk = Wk0 0 . If there is no previous appearance, we set Wk = ∅.
(b) For each position k and i ∈ Xk0 \ [m] such that the next appearance of ak in w is some
ak0 with i ∈ Xk0 , we include iR in Wk0 .
(c) For each position k and i ∈ Xk0 \ [m] such that the next appearance of ak in w is some
ak0 with i ∈
/ Xk0 , we include in Wk0 one of iB , iY . We do the same also if there is no next
appearance of ak in w.
The above specifications determine the values of all Wk , Wk0 , modulo the choice between
B and Y in case (c). Clearly, if the path p0 can be so constructed then A0 accepts w. It
remains to show that p0 can indeed be implemented in A0 . The form of the fk ’s is derived
from (a-c) according to the definition of δ 0 . But note that the definition of δ 0 imposes the
following condition:
(d) For each position k and iY ∈ Wk0 such that the next appearance of any ix in p0 is in
some Wk0 (with k < k 0 ), we must have iB ∈ Wk0 . Dually if iB ∈ Wk0 .
For example, if iY ∈ W20 but none of iB , iY , iR occurs in any of W3 , W30 , W4 , W40 , W5 , W50 ,
then {iB , iY , iR } ∩ W6 ⊆ {iB }. This condition stems from the interdiction to include if (i) in
Wk0 when f (i) 6= iR . The consequence of condition (d) is that in case (c) above we cannot
pick B and Y arbitrarily.
We need to show that a choice of “colours” (B and Y) satisfying both (c) and (d) can
be made. We achieve this by applying a graph colouring argument. Let us define a labelled
graph G with:
• Vertices (k, i) and (k, i)0 for each k ∈ [0, N − 1] and i ∈ [m + 1, m + n];
• For each i and k < k 0 as in (c) above, an edge between (k, i)0 and (k 0 , i) labelled with “=”.
• For each i and k < k 0 as in (d) above, an edge between (k, i)0 and (k 0 , i) labelled with “6=”.
Then, a valid choice of colours can be made as long as G can be coloured with B and Y in
such a way that =-connected vertices have matching colours, while 6=-connected vertices
have different colours. For the latter, it suffices to show that the graph obtained by merging
=-connected vertices can be 2-coloured, for which it is enough to show that G contains no
cycles. Suppose G contained a cycle. Then, by definition of the edge relation of the graph, it
must be the case that the leftmost vertex (i.e. the one with the least k index) in the cycle
be some (k, i)0 . The vertex (k, i)0 has two outgoing edges, one for each label. The 6=-edge in
particular connects to some (k 0 , i) such that k < k 0 , obtained from condition (d). Since (k 0 , i)
is part of the cycle, it must have an outgoing =-edge to some vertex (k 00 , i)0 with k 00 < k 0 .
But note that condition (d) stipulates that there is no mention of i between k and k 0 in p0 ,
and therefore k 00 ≤ k. Moreover, k 00 = k is not an option as it would imply that register i
was not rewritten between steps k and k 0 in p, in which case k and k 0 would fall under case
(b) above. Hence, k 00 < k which contradicts our assumption that (k, i)0 was the leftmost
vertex in the cycle.

16

R. GRIGORE AND N. TZEVELEKOS

Note that the above result can be extended to handle the case in which registers are
not initially empty by simply making use of Lemma 3.1. However, the construction in
that lemma leads to a doubly exponential blow-up in size, which we can be avoided by the
alternative approach that follows.
Proposition 4.5. Let A = hQ, q0 , H0 , δ, F i be an (m, n)-non-reset-HRA. We can construct
a bisimilar (m + n, n)-non-reset-HRA A0 = hQ0 , q00 , H00 , δ 0 , F 0 i such that, for all i ∈ [m + n +
1, m + 2n], H0 (i) = ∅. Moreover, we have |Q0 | ∈ O(2n · |Q|) and |δ 0 | ∈ O(22n · |δ|).
Proof. The main idea behind the construction of A0 is to use the additional n histories to
store just the initial names of the registers in A. Once these names have been used in the
computation, they are transferred to their actual registers (if any). We will also need to
track which of the registers in A are still simulated by histories in A0 . Thus, we set
Q0 = Q × ([m + 1, m + n] → {0, 1})
and q00 = (q0 , {(i, 1) | i ∈ [m + 1, m + n]}), H00 = H0 ∪ {(m + n + i, ∅) | i ∈ [n]} and
X,X 0

F 0 = F × ([m + 1, m + n] → {0, 1}). Moreover, for each q −→ q 0 in δ and map f , we include
Y,Y 0

in δ 0 a transition (q, f ) −→ (q 0 , f 0 ) where:
• Y = (X ∩ [m]) ] Y1 ] Y0 , where
Y1 = { i ∈ X | f (i) = 1 } ∪ { n + i | i ∈ X ∧ f (i) = 0 }
and Y0 ⊆ { i ∈ [m + 1, m + n] | i ∈
/ X ∧ f (i) = 0 };
• Y 0 = (X 0 ∩ [m]) ∪ { n + i | i ∈ X 0 \ [m] };
• f 0 = f [i 7→ 0 | i ∈ X ∪ X 0 ].
Then, taking R to be the relation:
R = { ((q, H), ((q, f ), H 0 ) | H  [m] = H 0  [m] ∧ ∀i ∈ [m + 1, m + n].
∧ f (i) = 1 =⇒ H 0 (n + i) = ∅ ∧ H 0 (i) = H(i)
∧ f (i) = 0 =⇒ H 0 (n + i) = H(i)
∧ ∀j ∈ [m + 1, m + n]. H 0 (i) ∩ H 0 (n + j) = ∅ }
we can show that R is a bisimulation.
Let us now see what is the size of the HRA A0 we constructed. We have |Q0 | ∈ O(2n ·|Q|).
X,X 0

Y,Y 0

For each transition q −→ q 0 in A, we introduce several transitions (q, f ) −→ (q 0 f 0 ) in A0 :
there are ≤ 2n choices for f ; and there are ≤ 2n choices for Y0 . In summary, |δ 0 | ∈ O(22n ·|δ|).
Hence, the general case follows.
Corollary 4.6. Let A = hQ, q0 , H0 , δ, F i be an (m, n)-non-reset-HRA. We can construct
an (m + 4n, 0)-non-reset-HRA A0 = hQ0 , q00 , H00 , δ 0 , F 0 i that accepts the same language as A.
We have |Q0 | ∈ O(23n · |Q|) and |δ 0 | ∈ O(25.3n · |δ|).

HISTORY-REGISTER AUTOMATA

17

4.3. Simulating Registers Symbolically. So far we saw how to simulate registers using
histories. If we are interested only in emptiness/reachability rather than language equivalence,
we can actually simulate the behaviour of registers without the inclusion of additional histories.
This alternative is going to be crucial in Section 6.2, where the number of histories will be
fixed to just one.
We next describe how this simulation can be done. Given an assignment H with m
histories and n registers, we can represent H symbolically as follows:
• we map each name stored in the registers of H to a number from the set [n];
• we subsequently replace in H all these names by their number.
For example, consider the assignment

1 7→ {a, b, c}, 2 7→ {d}, 3 7→ ∅, 4 7→ {a}, 5 7→ {d}
of a (1, 4)-HRA. We can simulate it symbolically by mapping d to 1, and a to 2. This results
to a symbolic representation:

1 7→ {2, b, c}, 2 7→ 1, 3 7→ ∅, 4 7→ 2, 5 7→ 1
where the nominal part has been curtailed to the fact that H(1) contains the names b and c.
We can now employ this representation technique to represent configurations of (m, n)HRAs by corresponding ones belonging to (m, 0)-HRAs. In particular, given the configuration
 

q, 1 7→ {a, b, c}, 2 7→ {d}, 3 7→ ∅, 4 7→ {a}, 5 7→ {d}
of a (1, 4)-HRA, we map it to the configuration
 

 
q, 1 7→ {2}, 2 7→ 1, 3 7→ ∅, 4 7→ 2, 5 7→ 1 , 1 →
7 {b, c}
of a (1, 0)-HRA which incorporates the non-nominal part of our representation scheme in
its state. Clearly, the state space of the new automaton in this simulation will experience
an exponential blowup, as the next result shows. However, no additional histories will be
needed, which is the main target here.
Proposition 4.7. Let A = hQ, q0 , H0 , δ, F i be an (m, n)-HRA. We can construct an (m, 0)HRA A0 = hQ0 , q00 , H00 , δ 0 , F 0 i that is empty if and only if A is empty. We have |Q0 | ∈
O(2mn nBn |Q|) and |δ 0 | ∈ O(2mn nBn |δ|), where Bn is the nth Bell number. Moreover, A0
contains reset transitions if and only if A contains reset transitions.
Proof. Each state q ∈ Q will be simulated by several states (q, f ) ∈ Q0 , where f : [m + n] →
P([n]) will be called an assignment skeleton. Such a skeleton f is valid when:
• |f (i)| ≤S1 for registers i ∈ [m + 1, m + n];
• f (i) ⊆ nj=1 f (m + j) for histories i ∈ [m];
S
• for all k ∈ [n] there is a k 0 ∈ [k] such that ki=1 f (m + i) = [k 0 ].
The latter condition essentially stipulates that f is a partition function on the set [m+1, m+n]:
the elements of the set are uniquely assigned numbers which can be seen as class indices —
two elements are assigned the same number iff they belong to the same class. There is also a
special class in this partition, namely of all elements of [m + 1, m + n] to which f assigns ∅.
We can now define the rest of A0 . First, we let q00 = (q0 , f0 ), where (f0 , H00 ) is the
symbolic representation of H0 . In order to construct δ 0 we define a transition relation on
skeletons, which is very similar to the configuration graph of HRAs (Definition 2.2) except
X,X 0

that it allows symbols to be permuted after the transition is taken. We write f −→ f 0 when

18

R. GRIGORE AND N. TZEVELEKOS

there exists a permutation π on [n] and a k ∈ [n] such that k ∈ f @X and f 0 = π ◦ (f [k in X 0 ]).
X

We write f −→ f 0 when there exists a permutation π such that f 0 = π ◦ (f [X 7→ ∅]).
X,X 0

To simulate one transition of the form q −→ q 0 from δ, we use several transitions of the
`
form (q, f ) −→ (q 0 , f 0 ) in δ 0 . Let us consider an arbitrary pair (f, f 0 ) of valid skeletons, and
see how to pick `. There are four cases, depending on whether X and X 0 mention or not
registers.
∅,∅

• Case X ⊆ [m] and X 0 ⊆ [m]. It must be that f −→ f 0 , and we pick ` = (X, X 0 ).
∅,X 0

• Case X ⊆ [m] and X 0 6⊆ [m]. It must be that f −→ f 0 , and we pick ` = (X, ∅).
X,∅

• Case X 6⊆ [m] and X 0 ⊆ [m]. It must be that f −→ f 0 , and we pick ` = (∅, X 0 ).
X,X 0

• Case X 6⊆ [m] and X 0 6⊆ [m]. It must be that f −→ f 0 , and we pick ` = (∅, ∅).
X

Similarly, each reset transition q −→ q 0 from δ yields several transitions of the form
Z
(q, f ) −→ (q 0 , f 0 ) in δ 0 . Given an arbitrary pair (f, f 0 ) of valid skeletons, we pick Z as follows.
X

If X ⊆ [m] then it must be that f 0 = f and we pick Z = X. Otherwise, f −→ f 0 and we
pick Z = ∅.
To estimate |Q0 | it suffices to count how many valid skeletons there are. The values
f (m + 1), . . . , f (m + n) of a valid skeleton correspond to a partition of the registers and a
selection of a class (if any) whose registers are empty. There are Bn possible partitions and
≤ (n + 1) possible selections, which gives ≤ (n + 1)Bn cases. For the values f (1), . . . , f (m)
of a valid skeleton there are ≤ 2mn possibilities. In total, |Q0 | ≤ 2mn (n + 1)Bn |Q|.
To estimate |δ 0 |, note that once f is fixed in the construction above, the constraints on
0
f determine it uniquely. So, the number of transitions increases by the same factor as the
number of states.

Since log Bn ∈ Θ(n log n), we have that log 2mn (n + 1)Bn ∈ Θ(mn + n log n).
5. Emptiness and Universality
5.1. Emptiness. Here we show that deciding emptiness is Ackermann-complete. We work
by reducing from and to state reachability problems in counter systems (similarly e.g. to [7, 5]).
For the upper bound, we reduce nonemptiness of HRAs to control-state reachability of TVASSs. For the lower bound, we reduce control-state reachability of R-VASSs to nonemptiness
of HRAs. Recall that the nonemptiness problem for HRAs asks, given an HRA A with
w
initial state q0 and initial assignment H0 , whether (q0 , H0 ) −→
−→ (qF , HF ) for some word w,
final state qF and assignment HF .
The configurations of a k-dimensional TR-VASS (Transfer–Reset Vector Addition System
with States) have the form (q, ~v ), where q is a state from a finite set, and ~v is a k-dimensional
vector of nonnegative counters. A VASS has moves that shift the counter vector, changing ~v
into ~v + ~v 0 , where ~v 0 comes from some finite and fixed subset of Zk . An R-VASS also has
moves that reset a counter, changing ~v into ~v [i 7→ 0] for some counter i. A T-VASS also
has moves that transfer the content of one counter into another counter, changing ~v into
~v [j 7→ ~v (i) + ~v (j)][i 7→ 0] for some i =
6 j. A TR-VASS is the obvious combination of the
above, and is formally defined as follows.

HISTORY-REGISTER AUTOMATA

19

Definition 5.1 (TR-VASS). A k-dimensional Transfer-Reset Vector Addition System
with States A is a pair hQ, δi, where Q is a finite set of states, and δ ⊆ Q×(Zk ][k]2 ][k])×Q
is a transition relation. A configuration of A is a pair (q, ~v ) of a state q and a vector
~v ∈ Nk of counter values. The configuration graph of A is constructed by including an
arc (q, ~v ) → (q 0 , ~v 0 ) when one of the following holds:
• there is some (q, ~v 00 , q 0 ) ∈ δ such that ~v 0 = ~v + ~v 00
• there is some (q, (i, j), q 0 ) ∈ δ such that ~v 0 = ~v [i 7→ 0][j 7→ ~v (i) + ~v (j)] and i 6= j
• there is some (q, (i, i), q 0 ) ∈ δ and ~v 0 = ~v
• there is some (q, i, q 0 ) ∈ δ such that ~v 0 = ~v [i 7→ 0].
The control-state reachability problem for A asks whether, given states q0 , qF and initial
vector ~v0 , is there some ~vF such that (q0 , ~v0 ) −→
−→ (qF , ~vF ).
The reduction from a (m, 0)-HRA to a T-VASS of dimension 2m − 1 is done by mapping
e of the corresponding T-VASS. Then,
each nonempty set of histories X into a counter X
name-accepting transitions are mapped into counter decreases
and increases, while resets

result in transfers between the counters. Let e· : P [m] → [0, 2m − 1] be a bijection such
i−1 . Further, given an assignment H,
e ,P
that e
∅ = 0; for instance, one could take X
i∈X 2
m −1
2
e denote the vector (h1 , . . . , h2m −1 ) ∈ N
let H
such that hXe = |H@X|, for all nonempty
X ⊆ [m]; that is, hXe counts how many names occur in exactly the histories indexed by X.
Lemma 5.2. Given an (m, 0)-HRA A it is possible to construct a T-VASS A0 of dimension
2m − 1 such that, for all q, q 0 , H, H 0 ,
w
f0 ).
e →
∃w, (q, H) −→
−→A (q 0 , H 0 )
if and only if
(q, H)
→A0 (q 0 , H
Let Q and δ be the states and the transitions of A, and let Q0 and δ 0 be the transitions
of A0 . We have that |Q0 | ∈ O(2m |Q|) and |δ 0 | ∈ O(2m |δ|). Moreover, the construction takes
O(|Q0 | + m|δ 0 |) time. If there are no reset transitions in A, then A0 is a |δ|-dimensional
VASS with Q0 = Q and |δ 0 | = |δ| that uses only increments and decrements.
Let ~0 be the all-zero vector (0, . . . , 0). Let ~δi be ~0[i 7→ 1] for i ∈ [m], and ~δ0 be ~0.
~
δ e 0 −~
δe

X,X 0

X
−−−X
→ q 0 in
Proof. For each transition q −→ q 0 of the HRA, we construct a transition q −−
X
the T-VASS. For each transition q −→ q 0 of the HRA, we construct a path

1,j1

2,j2

3,j3

2m −2,j2m −2

2m −1,j2m −1

q −→ · −→ · −→ · · · −−−−−−−−→ · −−−−−−−−→ q 0
in the T-VASS such that jYe = Y^
\ X. To construct such a path we iterate through 2m − 1
nonempty sets Y , and for each we compute Y \ X in O(m) time.
Lemma 5.2 implies that nonemptiness of a HRA reduces to control-state reachability
of a T-VASS. We shall describe an algorithm that solves control-state reachability for the
T-VASS constructed in Lemma 5.2. The analysis of this algorithm depends on the so-called
Length Function Theorem, which is phrased in terms of the Fast Growing Hierarchy and
bad sequences. We define these next.
The Fast Growing Hierarchy consists of classes F0 , F1 , F2 , . . . of functions, where
F0 = F1 contain the linear functions, F2 contains the elementary functions, primitive

20

R. GRIGORE AND N. TZEVELEKOS

recursive functions are in Fk for some finite k, and Fω is the Ackermann complexity class.
The classes Fk are defined in terms of the following functions:
Fn+1 (x) , (Fn ◦ · · · ◦ Fn )(x) = Fnx+1 (x)
{z
}
|

F0 (x) , x + 1

Fω (x) , Fx (x)

x + 1 times
f ∈ O(Fkn )

For k ≥ 2, (a) f ∈ Fk if and only if
for some n; and (b) a nondeterministic
algorithm using space bounded by some function in Fk can be transformed into a deterministic
algorithm using time bounded by some (other) function in Fk .
Let X be a partially ordered set with some size function |·| : X → N. We say that a
sequence x0 , x1 , x2 , . . . of elements of X is a bad sequence when xi 6≤ xj for all i < j. Given
a strictly increasing function g : N → N, we say that the sequence is controlled by g when
|xi+1 | ≤ g(|xi |) for all i. We will consider such sequences of VASS configurations, where the
order is given by
(q, ~v ) ≤ (q 0 , ~v 0 )

iff

q = q 0 ∧ ~v (1) ≤ ~v 0 (1) ∧ ~v (2) ≤ ~v 0 (2) ∧ ~v (3) ≤ ~v 0 (3) ∧ . . .

Lemma 5.3 (Length Function Theorem [34]). Let q̂0 , q̂1 , q̂2 , . . . be a bad sequence of kdimensional VASS configurations. If the sequence is controlled by some function g ∈ Fγ with
γ ≥ 1, then its length is bounded by f (|q̂0 |) for some function f ∈ Fγ+k .
We can now describe and analyze an algorithm for deciding emptiness of a (m, 0)-HRA.
Proposition 5.4. The emptiness problem for (m, 0)-HRAs is in F2m when m > 0. Thus,
the emptiness problem is in Fω when m is part of the input.
Proof. Let A be the given HRA, and let A0 be the T-VASS constructed as in Lemma 5.2.
We use the backward coverability algorithm [34, Sections 1.2.2 and 2.2.2], which explores all
bad sequences (q0 , ~v0 ), (q1 , ~v1 ), . . . , (qL , ~vL ) such that
• (q0 , ~v0 ) is a minimal final configuration, and
• (qk , ~vk ) is a minimal configuration out of those that can reach a configuration ≥ (qk−1 , ~vk−1 ).
The constraint that (q0 , ~v0 ) is a minimal final configuration simply means that q0 is final
and ~v0 = ~0. To construct such sequences, we need an effective way of generating all possible
(qk , ~vk ), given a fixed (qk−1 , ~vk−1 ). For this, we enumerate all transitions of A0 that go to qk−1 .
~
δi −~
δj

i,j

~
δi −~
δj

There are two types of such transitions: qk −→ qk−1 and qk −→ qk−1 . For qk −→ qk−1 ,
i,j
we let ~vk be max(~vk−1 − ~δi + ~δj , ~0), where max is taken pointwise. For qk −→ qk−1 with
i,j

i = j, we take ~vk to equal ~vk−1 . For qk −→ qk−1 with i 6= j, we may have multiple choices
for ~vk . Assuming ~vk−1 (i) = 0, it could be that ~vk (i) is any of 0, 1, . . . , ~vk−1 (j); otherwise, if
~vk−1 (i) 6= 0, the transition could not have been taken. In all the cases from above, we keep
only those choices of ~vk that ensure the sequence is bad.
To show that the sequences so constructed are finite, we use Lemma 5.3. Let |(q, ~v )| be the
number bits in a concrete representation of (q, ~v ): we encode q with ∼ log2 |Q0 | = m log2 |Q|
bits, then we write each ~v (i) in binary, precede each of its bits by 1 and mark the end
with 0. (For example, we represent 5 by 1110110.) For the sequences constructed as in the
previous paragraph, we have |(qk , ~vk )| ≤ 2 · |(qk−1 , ~vk−1 )|. Thus, the sequences are controlled
by g(x) = 2x, which is a function in F1 . As A0 has dimension 2m − 1, Lemma 5.3 gives us
that the length L of the sequence is bounded by some function in F2m .
A nondeterministic algorithm can repeatedly guess the correct successor in the sequence,
using 2L · |(q0 , ~0)| space. If m ≥ 1, then this is bounded by f (m log |Q|) for some function

HISTORY-REGISTER AUTOMATA

21

f ∈ F2m , and we are in a situation where the distinctions time/space and deterministic/
nondeterministic are irrelevant.
It is possible to modify the algorithm described in the previous proof so that it works
directly on the HRA representation, without appealing to Lemma 5.2. Similarly, it is possible
to extend the algorithm described in the previous proof to handle registers directly, without
appealing to Proposition 4.1. Such improvements may be worthwhile in an implementation,
but the complexity upper bound remains Ackermannian.
Doing the opposite reduction we show that deciding emptiness is Ackermann-hard
even for strongly deterministic HRAs. In this direction, each R-VASS of dimension m can
be simulated by an (m, 0)-HRA so that the value of each counter i of the former is the same
as the number of names appearing precisely in history i of the latter. In order to extend the
bound to strongly deterministic HRAs one can choose to reduce from a restricted class of
R-VASSs, so that the image of the reduction can be made strongly deterministic, or resolve
nondeterminacy at the level of HRAs by appropriate obfuscation. We follow the latter,
simpler solution.
Proposition 5.5. The emptiness problem for strongly deterministic HRAs is Ackermannhard.
Proof. Let A be an m-dimensional R-VASS whose additive transitions only increment or
~v
decrement single counters: for each transition q −→ q 0 , we have ~v = ±~δi for some i. By [35],
control-state reachability for such R-VASSs is Ackermann-hard. We construct an (m, 0)δ

∅,{i}

−δ

i
i
HRA A0 with the same states as A, and we map: each q −
→
q 0 to q −→ q 0 , each q −−→
q 0 to

{i},∅

i

{i}

q −→ q 0 , and each q →
− q 0 to q −→ q 0 . We can see that A0 simulates the behaviour of A by
storing the value of each counter i as |H@{i}|. Hence, L(A0 ) is nonempty if and only if qF
is reachable, from (q0 , ~v0 ), in the R-VASS A.
We observe that A0 may not be strongly deterministic. Suppose that the size of the
transition function of A is n. We can then impose strong determinacy on A0 by enriching
it with n registers and preluding each transition of the above translation with a transition
reading from one of the additional registers. We thus obtain an (m, n)-HRA that is strongly
deterministic and simulates A as above.
Proposition 5.6. The emptiness problem of HRAs is Ackermann-complete.
Proof. Combine Proposition 4.1 with Proposition 5.4 and Proposition 5.5.
5.2. Universality. We finally consider universality and language containment. Note first
that our machines inherit undecidability of these properties from register automata [31].
However, these properties are decidable in the deterministic case.
In order to simplify our analysis, we shall be reducing HRAs to the following compact
form where -transitions are incorporated inside name-accepting ones. As we show below,
no expressiveness is lost by this packed form.
A packed (m, 0)-HRA is a tuple A = hQ, q0 , δ, H0 , F i defined exactly as an (m, 0)-HRA,
with the exception that now:
δ ⊆ Q × P([m]) × P([m]) × P([m]) × Q

22

R. GRIGORE AND N. TZEVELEKOS

Y ;X,X 0

We shall write q −−−−−→ q 0 for (q, Y, X, X 0 , q 0 ) ∈ δ. The semantics of such a transition is
Y

X,X 0

the same as that of a pair of transitions q −→ · −→ q 0 of an ordinary HRA. Formally,
configurations of packed HRAs are pairs (q, H), like in HRAs, and the configuration graph
a
of a packed HRA A like the above is constructed as follows. We set (q, H) −→ (q, H 0 ) if
Y ;X,X 0

there is some q −−−−−→ q 0 in δ such that, setting HY = H[Y 7→ ∅], we have a ∈ HY @X and
H 0 = HY [a in X 0 ].
Lemma 5.7. Let A be an (m, 0)-HRA. There is a packed (m, 0)-HRA A0 such that A ∼ A0 .
Proof. Let A = hQ, q0 , δ, H0 , F i. We set A0 = hQ, q0 , δ 0 , H0 , F 0 i where:
Y

F 0 = {q 0 ∈ Q | ∃q ∈ F, Y. q 0 −→
−→ q ∈ δ}
Y

X,X 0

δ 0 = {(q, Y, X, X 0 , q 0 ) | q −→
−→ · −→ q 0 ∈ δ}
Bisimilarity of A and A0 is witnessed by the identity on configurations, which means that
R = { ((q, H), (q, H)) | q ∈ Q ∧ H ∈ Asn } is a bisimulation.
We shall decide language containment via complementation. In particular, given a
deterministic packed HRA A, the automaton A0 accepting the language N ∗ \ L(A) can
be constructed in the analogous way as for deterministic finite-state automata, namely by
obfuscating the automaton with all missing transitions and swapping final with non-final
states.
Lemma 5.8. Deterministic packed HRAs are closed under complementation.
Proof. Let A = hQ, q0 , δ, H0 , F i be a packed (m, 0)-HRA. Following the above rationale, we
construct a packed (m, 0)-HRA A0 = hQ ] {qF }, q0 , δ ∪ δ 0 , H0 , F 0 i, where F 0 = {qF } ∪ (Q \ F )
Y ;X\Y,X 0

and δ 0 is given as follows. For each q ∈ Q and all X such that there is no q −−−−−−→ q 0 add
∅;X,∅

[m];∅,∅

a transition q −−−−→ qF in δ 0 . In addition, δ 0 contains a transition qF −−−−−→ qF .
We claim that L(A0 ) = N ∗ \ L(A). Indeed, if s ∈ L(A0 ) and s is accepted at a state in Q \ F
then, since A is deterministic, we have s ∈
/ L(A). Otherwise, if s = s0 as00 with a the point
where a transition to the sink state is taken then, upon acceptance of s0 by A, a appears
precisely in some histories X such that A has no transition to accept a at that point. Thus,
s∈
/ L(A).
Conversely, if s ∈ N ∗ \ L(A) then either s induces a configuration in A which does not end
in a final state, or s = s0 as00 where s0 is accepted by A but at that point a is not a possible
transition. We can see that, in each case, s ∈ L(A0 ).
Proposition 5.9. Language containment and universality are undecidable for (general)
HRAs and Ackermann-complete for strongly deterministic HRAs.
Proof. Undecidability in the general case is inherited from RAs.
Now consider two HRAs A and A0 such that we can compute the complement of A0 .
Then, we can decide the language containment L(A) ⊆ L(A0 ) by checking whether the
product of A with the complement of A0 is empty. The product construction is polynomial,
and the emptiness check is in Ackermann (Proposition 5.4). Thus, language containment
is in Ackermann if computing the complement of A0 is in Ackermann. This is the case
because (a) removing registers can be done while preserving determinism with only an
exponential increase in size (Proposition 4.1), and (b) complementing deterministic HRAs

HISTORY-REGISTER AUTOMATA

23

without registers takes polynomial time (Lemma 5.8). For hardness, note that emptiness
and universality are equally hard in the deterministic case (Lemma 5.8), and emptiness is
Ackermann-hard (Proposition 5.5).
We showed that language containment is in Ackermann and universality is Ackermann-hard. Finally, note that there is a trivial reduction from universality to language
containment.

6. Weakening HRAs
Since the complexity of HRAs is substantially high, e.g. for deciding emptiness, it is useful
to seek for restrictions thereof which allow us to trade expressiveness for efficiency. As
the encountered complexity stems from the fact that HRAs can simulate computations of
R-VASSs, our strategy for producing weakenings is to restrict the functionalities of the
corresponding R-VASSs. We follow two directions:
(a) We remove reset transitions. This corresponds to removing counter transfers and resets
and drops the complexity of control-state reachability to exponential space.
(b) We restrict the number of histories to just one. We thus obtain polynomial space
complexity as the corresponding counter machines are simply one-counter automata.
This kind of restriction is also a natural extension of FRAs with history resets.
Observe that each of the aspects of HRAs targeted above corresponds to features (1,2) we
identified in the Introduction, witnessed by the languages L1 and L2 respectively. We shall
see that each restriction leads to losing the corresponding language.
6.1. Non-reset HRAs. We first weaken our automata by disallowing resets. We show that
the new machines retain all their closure properties apart from Kleene-star closure. The
latter is concretely manifested in the fact that language L1 of the Introduction is lost. On
the other hand, the emptiness problem reduces in complexity to exponential space.
Definition 6.1. A non-reset HRA of type (m, n) is an (m, n)-HRA A = hQ, q0 , H0 , δ, F i
X

such that there is no q −→ q 0 ∈ δ.
Closure properties. Of the closure constructions of Section 3 we can see that union and
intersection readily apply to non-reset HRAs, while the construction for concatenation needs
some amendments.
More specifically, of the two constructions presented in the proof of Proposition 3.2,
the one for concatenation can be adapted to non-reset HRAs as follows. We add empty
transitions from the final states of A01 to the initial state of a version of A02 which keeps the
places used by A01 untouched and uses its own separate copy of places, obfuscating its own
transitions so as to capture accidental matchings of the legacy names of A01 . This solution
cannot be used for Kleene closure as in each loop the automaton needs to find a fresh copy
of its initial configuration, and be able to use it (in the previous construction, the final
assignment of A01 is lost).
On the other hand, using an argument similar to that of [5, Proposition 7.2], we can
show that the language L1 is not recognised by non-reset HRAs and, hence, the latter are
not closed under Kleene star. Finally, note that the HRA constructed for the language L4

24

R. GRIGORE AND N. TZEVELEKOS

in Example 3.4 is a non-reset HRA, which implies that non-reset HRAs are not closed under
complementation.
Emptiness. In the general case we saw an upper bound of F2m (Proposition 5.4), by a
reduction to T-VASS followed by the backward coverability algorithm. For a non-reset HRA,
the same reduction yields a VASS, without transfers. In the absence of transfers, better
bounds are known for the backward coverability algorithm [11]. More generally, it has been
known for some time that coverability for VASS is ExpSpace-complete [12, 25].
The following result refers to the number N of bits used to represent an HRA. Of course,
N depends on the exact representation being used. Still, we do not make this representation
explicit because the result holds for a wide variety of possible representations. We only
require that the representation obeys m, n, |δ|, log |Q| ∈ O(N ).
Proposition 6.2. The emptiness problem
for a non-reset HRA is in ExpSpace. More

precisely, it is in NSpace 2O(N log N ) , where N is the number of bits used to represent the
HRA.
Proof. We start with an (m, n)-non-reset-HRA A = hQ, q0 , δ, H0 , F i. We use Proposition 4.7
to construct an (m, 0)-non-reset-HRA A0 = hQ0 , q00 , δ 0 , H00 , F 0 i that preserves emptiness.
Moreover, log |Q0 | ∈ O(mn + n log n + log |Q|). Using Lemma 5.2, we reduce A0 to a (|δ| + 1)dimensional VASS with |Q0 | states that uses only increments/decrements. (Lemma 5.2 creates
an m-dimensional VASS where m is the number of sets labelling transitions. Proposition 4.7
puts in A0 only sets that already occurred in A, with the possible exception of ∅.) Now
we apply the backward coverability algorithm, as described in the proof of Proposition 5.4.
By [11, Theorem 2], the algorithm will only consider counter values less than some V =
O(|δ| log |δ|)
(3|Q0 |)2
. In the nondeterministic version of the algorithm, we guess the next
configuration, which means we only need space O((|δ| + 1) log V ) to store a couple of
configurations. We have
log log V = O(|δ| log |δ| + log log |Q0 |) = O(|δ| log |δ| + log(mn + n log n + log |Q|))
Since m, n, |δ|, log |Q| ∈ O(N ), we conclude log |δ| + log log V ∈ O(N log N ). This implies that a nondeterministic
version of the backward coverability algorithm works in

O(N
log
N
)
NSpace 2
.
The previous proposition has a couple of obvious consequences. First, emptiness is also in

O(N log N ) 
DSpace 2O(N log N ) , by Savitch’s theorem. Second, emptiness is also in DTime 22
,
by a standard easy argument [19, Theorem 5.3]. In fact, one can show that the time bound
applies to the backward coverability algorithm, without invoking generic constructions from
complexity theory: By [11, Theorem 2], the runtime of the backward coverability algorithm —
O(|δ| log |δ|) 
like the counter values — is also upper bounded by some T = O (3|Q0 |)2
. The rest
of the argument is as in the proof of Proposition 6.2.
Proposition 6.3. The emptiness problem for non-reset HRAs is ExpSpace-hard.
Proof. By [25], the control-state reachability problem for VASS is ExpSpace-hard even if
all the transitions are restricted to have labels of the form ±~δi . (More precisely, Lipton
proves that certain parallel programs of size poly(k) can simulate any Turing machine that
uses < 2k space. Then, [25, Lemma 2] asserts that reachability in these programs reduces
to reachability in VAS, the full proof being: ‘We omit a detailed proof of this lemma. It

HISTORY-REGISTER AUTOMATA

25

should, however, be clear that parallel programs can be encoded as vector addition systems.’
Similarly, we claim without proof, that it should be clear how Lipton’s programs reduce to
the control-state reachability problem for VASSs whose transitions only increment/decrement
single counters.) We shall reduce the control-state reachability problem for such VASSs to
the emptiness problem for non-reset HRAs.
Let m be the dimension of the VASS. We construct a HRA with m0 histories, where
0
0
m is the smallest integer such that m ≤ 2m − 1. As a result, there exists an injection
φ : [m] → P6=∅ ([m0 ]); we fix arbitrarily one such injection.
+~
δ

∅,φ(i)

−~
δ

φ(i),∅

• For each transition q −→i q 0 in the VASS, we include a transition q −→ q 0 in the HRA.
• For each transition q −→i q 0 in the VASS, we include a transition q −→ q 0 in the HRA.
This construction maintains the invariant |H@φ(i)| = ~v (i). To establish the invariant, we
pick the initial history assignment H0 accordingly. Finally, we set as final the state in whose
reachability we are interested.
The reduction described above is clearly polynomial, from which it follows that emptiness
of non-reset HRAs (even without registers) is ExpSpace-hard.
Proposition 6.4. The emptiness problem for non-reset HRAs is ExpSpace-complete.
Proof. Immediate from Proposition 6.2 and Proposition 6.3.
6.2. Unary HRAs. Our second restriction concerns allowing resets but bounding the
number of histories to just one. Thus, these automata are closer to the spirit of FRAs
and, in fact, extend them by rounding up their history capabilities. We show that these
automata require polynomial space complexity for emptiness and retain all their closure
properties apart from intersection. The latter is witnessed by failing to recognise L2 from
the Introduction. We can see that extending this example to multiple interleavings we can
show that intersection is in general incompatible with bounding the number of histories.
Definition 6.5. A (1, n)-HRA is called unary HRA of n registers.
In other words, unary HRAs are extensions of FRAs where names can be selectively
inserted or removed from the history and, additionally, the history can be reset. These
capabilities give us in fact a strict extension.
Example 6.6. The automata used in Example 2.3 for L1 and L3 were unary HRAs. Note
that neither of those languages is FRA-recognisable. On the other hand, in order to recognise
L2 , an HRA would need to use at least two histories: one history for the odd positions of
the input and another for the even ones. We can formalise an argument to show that L2 is
not recognisable by unary HRAs as follows.
Proof. Suppose L2 = L(A) for some unary HRA A of n registers and let
w = a1 b1 . . . ak bk b1 a1 · · · bk ak
for k = n + 1 and some pairwise distinct names a1 , b1 , . . . , ak , bk . As w ∈ L2 , there is a path,
say p, in A which accepts w. We divide p as p1 p2 with p2 accepting the second half of w. Let
p̂ = p̂1 p̂2 be the corresponding configuration path and let (q 0 , H 0 ) be the first configuration
in p̂2 . We set S = {a1 , b1 , · · · , ak , bk } \ {a | a ∈ H 0 (i) ∧ i > 1} and do a case analysis on the
labels of the form (X, X 0 ) which appear in p2 and accept names from S. Since names in S

26

R. GRIGORE AND N. TZEVELEKOS

do not appear in any H 0 (i), for i > 0, it must be that each such X is either {1} or ∅. We
have the following cases.
• There are two such labels, say ({1}, Xi ) and ({1}, Xj ), accepting names ai and bj respectively. But this would imply that A also accepts w0 , where w0 is w with these occurrences
of ai and bj swapped, contradicting L(A) = L2 (as w0 ∈
/ L2 ).
• There are two such labels, say (∅, Xi ) and (∅, Xj ), accepting names ai and bj respectively.
In order for A not to accept w0 (w0 as above), it is necessary that a reset transition with
label Y 3 1 occurs between the two transitions. Suppose i < j. Then, since k > n, there
is a name ai0 which does not appear in any place after clearing Y . Thus, (∅, Xj ) can
accept ai0 and complete the path p by accepting a word w0 ∈
/ L2 . Dually if j ≤ i.
• Each ai ∈ S is accepted by a label ({1}, X 0 ), and each bj ∈ S by a label (∅, X 0 ). Let
ai ∈ S be the last such accepted in p2 . This means that the rest of the path has length
at most 2n. Therefore, since k > n, there is a bj ∈ S accepted in p2 before ai . Let
(q, H) be the configuration just before accepting bj . In order for A not to accept any ai0
at that point, it must be that all ai0 ∈ S appear in H. Since |S| > n + 1, there exists
ai0 ∈ H(1) ∩ S such that ai0 6= ai . But then, the transition accepting ai can accept ai0
instead and lead to acceptance of a word w0 6∈ L2 .
We therefore reach a contradiction in every case.
Closure properties. The closure constructions of Section 3 readily apply to unary HRAs, with
one exception: intersection. For the latter, we can observe that L2 = L(A1 ) ∩ L(A2 ), where
L(A1 ) = {a1 a01 . . . an a0n ∈ N ∗ | a1 . . . an ∈ L0 } and L(A2 ) =
∅,1
q0
q1
{a1 a01 . . . an a0n ∈ N ∗ | a01 . . . a0n ∈ L0 }, and A1 and A2 are the
unary (1, 0)-HRAs on the side, with empty initial assignments. On
∅,∅ / 1,1
the other hand, unary HRAs are not closed under complementation
∅,∅ / 1,1
as well, as one can construct unary HRAs accepting L(A1 ) and
q0
q1
L(A2 ), and then take their union to obtain a unary HRA for L2 .
∅,1
Emptiness. In the case of just one history, the results on TR-VASS reachability [35, 16]
from Section 5 provide rather rough bounds. It is therefore useful to do a direct analysis.
We reduce nonemptiness for unary HRAs to control-state reachability for one dimensional
R-VASSs. Our analysis below shows that the minimal path has length at most quadratic,
from which it follows that nonemptiness has polynomial complexity.
The following result applies to any R-VASS representation for which |Q| log |Q| ∈ O(N ),
where |Q| is the number of states of the R-VASS, and N is the number of bits used to
represent the R-VASS. Note that the condition is true if all the states are listed in the
R-VASS representation, something all reasonable representations would do.
Lemma 6.7. Control-state reachability for one dimensional R-VASSs is in NL, provided
that non-reset transitions increase and decrease the counter by at most 1.
Proof. Let A = hQ, δi be an R-VASS of dimension 1. The proof relies on two observations:
Fact 1: If (q, i) −→
−→ (q 0 , i0 ) is a configuration path of A then, for each k > 0, there is a path
(q, i+k) −→
−→ (q 0 , i00 ) of the same length.
Fact 2: If (q, i) −→
−→ (q 0 , i0 ) is a configuration path of A in which there are no reset transitions
and the counter never becomes less than some k > 0, then there is a path (q, i−k) −→
−→
(q 0 , i00 ) of the same length.

HISTORY-REGISTER AUTOMATA

27

Consider an instance (A, q0 , i0 , qF ) of the control-state reachability problem: Is the
state qF reachable in A starting from configuration (q0 , i0 )? Let p be a configuration path of
minimal length from (q0 , i0 ) to some configuration whose state is qF . Let us see if a state can
appear repeatedly in p. By Fact 1, p is non-decreasing: any path segment (q, i) −→
−→ (q, i0 )
0
can be circumvented if i ≥ i . Now suppose that p contains a segment (q, i) −→
−→ (q, i + k)
for some k > 0. Consider the segment (q, i + k) −→
−→ (q 00 , i00 ) that follows, uses only non-reset
transitions, and is maximal. By Fact 2, if the counter never becomes < k in the latter
segment, then there exists a path (q, i) −→
−→ (q 00 , i00 ) of the same length. Since p is minimal,
this is a contradiction, and therefore the counter must become < k, somewhere after (q, i + k).
Let p0 be the segment (q, i + k) −→
−→ (q 0 , k − 1). Since non-reset transitions decrease the
counter by ≤ 1, it must be that all the values i + k, i + k − 1, . . . , k − 1 occur in p0 . When
one of these values is reached for the first time, it must be paired with a state that was not
used for the bigger values. It follows that (i + k) − (k − 1) + 1 ≤ |Q|, and so i ≤ |Q| − 2.
This gives us a bound on the counter value of any state that can be repeated in p. Thus,
each state can appear in p at most |Q| times. This implies that the length of p is at most
|Q|2 and that in p the counter does not exceed the value i0 + |Q|2 .
We can therefore answer the instance (A, q0 , i0 , qF ) of the control-state reachability
problem as follows. Note first that, by Facts 1 and 2 and because the length of minimal
reaching path is ≤ |Q|2 , we can replace i0 by min(i0 , |Q|2 ). Because we only consider initial
counter values ≤ |Q|2 and because the minimal path has length ≤ |Q2 |, we can store one
configuration on the minimal path using O(log |Q|) bits. Since |Q| log |Q| ∈ O(N ), we
have log |Q| ∈ O(log N ), and therefore O(log N ) bits suffice to represent a configuration of
the minimal path. Finally, we note that a nondeterministic algorithm can guess the next
configuration on the minimal path.
We remark that an NL upper bound follows from an analysis of the backward coverability
algorithm as well. However, the proof from above has the advantage that it is self-contained.
We now give an upper bound for the emptiness problem of unary HRAs. The result
holds for all representations that obey several weak requirements. Let hQ, q0 , δ, H0 , F i be a
unary HRA with n registers, represented with N bits. We require that
• n ∈ O(N ), which is justified because there are > 2n possible labels on transitions;
• |δ| ∈ O(N ), which is justified because we expect each transition to require at least a bit;
• |Q| log |Q| ∈ O(N ), which is justified because we expect each state to be mentioned at
least once in the representation. (This last point implies that log |Q| ∈ O(log N ).)
Proposition 6.8. The emptiness problem for unary HRAs is in PSpace. More precisely,
it is in NSpace(N log N ), where N is the number of bits used to represent the HRA.
Proof. Let A = hQ, q0 , δ, H0 , F i be the given unary HRA. Using Proposition 4.7, we
build a (1, 0)-HRA A0 that preserves emptiness, has O(Bn 2n n log |δ|) transitions, and has
O(Bn 2n n log |Q|) states. Using the construction from Lemma 5.2, we reduce the emptiness
of A0 to control-state reachability in an R-VASS A00 . Specialized to our case, the construction
says that
∅,{1}

+1

{1},∅

−1

• for each transition q −→ q 0 in A0 , we include a transition q −→ q 0 in A00 ;
• for each transition q −→ q 0 in A0 , we include a transition q −→ q 0 in A00 ; and
{1}

reset

• for each transition q −→ q 0 in A0 , we include a transition q −→ q 0 in A00 .

28

R. GRIGORE AND N. TZEVELEKOS

According to Lemma 6.7, the control-state reachability problem for A00 is in NSpace(log N 00 ),
where N 00 is the number of bits used to represent A00 . Thus, it remains to compute N 00
as a function of N . For this, we pick one particular representation of A00 , namely a list of
transitions. For such a representation we have N 00 = O Bn 2n n|δ| · log(Bn 2n n|Q|) . Thus,
log N 00 = O(n log n + log |δ| + log(n log n + log |Q|)) = O(N log N )
The last step assumes that n, |Q| log |Q|, |δ| ∈ O(N ). We require the representation of A
to satisfy these assumptions.
Proposition 6.9. The emptiness problem for unary HRAs is PSpace-hard.
Proof. By [15, Theorem 5.1a], the nonemptiness problem of register automata is PSpacehard. Register automata are a special case of unary HRAs.
Proposition 6.10. The emptiness problem for unary HRAs is PSpace-complete.
Proof. Immediate from Proposition 6.8 and Proposition 6.9.

7. Summary of Main Results
The theorems in this section summarize the main results proved in the previous sections.
Theorem 7.1. Languages recognised by HRAs are closed under union, intersection, concatenation, and Kleene star, but not under complementation. Also,
• if resets are banned, then closure under Kleene star is lost;
• if the number of histories is bounded, then closure under intersection is lost.
Proof. Immediate from Proposition 3.2, Lemma 3.3, and the closure results of Section 6.
Theorem 7.2. Deciding emptiness of an (m, n)-HRA has the following complexity:
(a) NL-complete if m = n = 0;
(b) NP-complete if m = 0 and all sets labelling transitions are singletons;
(c) PSpace-complete if m ≤ 1;
(d) ExpSpace-complete if there are no reset transitions; and
(e) Ackermann-complete in the general case.
Proof. (a) When m = n = 0, nonemptiness is equivalent to reachability in a directed graph,
which is a standard NL-complete problem. (b) In this case, HRAs are equivalent to RAs
that disallow repetitions of values in registers, as they were originally defined [23]. For such
RAs, nonemptiness is known to be NP-complete [33, Theorem 4]. (c) Proposition 6.10.
(d) Proposition 6.4. (e) Proposition 5.6.
For universality and language inclusion, see Proposition 5.9.

HISTORY-REGISTER AUTOMATA

29

8. Connections with existing formalisms
We have already seen that HRAs strictly extend FRAs. In this section, we compare HRAs
with CMAs (class memory automata). Like HRAs and FRAs, CMAs work on infinite
alphabets, and have a decidable nonemptiness problem. Implicitly, we also compare with
other formalisms: CMAs have been shown to express the same languages as data automata [5,
Proposition 3.7]; and data automata have been shown to express the same languages as the
two-variable fragment of existential monadic second order logic with data equality, position
successor, and class successor [7, Proposition 14].
Definition 8.1. A Class Memory Automaton (CMA) is a tuple A = hQ, q0 , φ0 , δ, F1 , F2 i
where Q is a finite set of states, q0 ∈ Q is initial, F1 ⊆ F2 ⊆ Q are sets of final states and
the transition relation is of type δ ⊆ Q × (Q ∪ {⊥}) × Q. Moreover, φ0 is an initial class
memory function, that is, a function φ : N → Q ∪ {⊥} with finite domain ({ a | φ(a) 6= ⊥ }
is finite).
The semantics of a CMA A is given as follows. Configurations of A are pairs of the
form (q, φ), where q ∈ Q and φ a class memory function. The configuration graph of A is
a
constructed by setting (q, φ) −→ (q 0 , φ0 ) just if there is (q, φ(a), q 0 ) ∈ δ and φ0 = φ[a 7→ q 0 ].
The initial configuration is (q0 , φ0 ), while a configuration (q, φ) is accepting just if q ∈ F1
and, for all a ∈ N , φ(a) ∈ F2 ∪ {⊥}.
Thus, CMAs resemble HRAs in that they store input names in “histories”, only that
histories are identified with states: for each state q there is a corresponding history q (note
notation overloading), and a transition which accepts a name a and leads to a state q must
store a in the history q. Moreover, each name appears in at most one history (hence the
type of φ), while the finality conditions for configurations allow us to impose that, at the
end, all names must appear in specific histories, if they appear in any. For instance, the
language L4 of Example 3.4, which we know cannot be recognized by HRAs (Lemma 3.3),
can be recognized by the following CMA on the left (with F1 = F2 = {q0 }).
∅,1

⊥

q0
q1

q1

q0

⊥

1,2

q1

q1
1,2
∅,1

Each name is put in history q1 when seen for the first time, and in history q0 when seen for
the second time. The automaton accepts if all its names are in q0 . This latter condition
is what makes the essential difference to HRAs, namely the capability to check where the
names reside for acceptance. For example, the HRA on the right above would accept the
same language it we were able to impose
S the condition that accepting configurations (q, H)
satisfy a ∈ H@{2} for all names a ∈ i H(i). Note though that, extending HRAs with such
finality conditions would render their nonemptiness problem reducible from reachability of
R-VASS (i.e. the question whether a specific state and counter content can be reached), a
problem known to be undecidable [2].
The above example proves that HRAs cannot express the same languages as CMAs.
Conversely, as shown in [5, Proposition 7.2], the fact that CMAs lack resets does not allow
them to express languages like, for example, L1 . As a result, the languages expressed by
CMAs are closed under intersection, union and concatenation, but not under Kleene star.
In the latter sections of [5] several extensions of CMAs are considered, one of which does

30

R. GRIGORE AND N. TZEVELEKOS

involve resets. However, the resets considered there do not seem directly comparable to the
reset capability of HRAs.
On the other hand, a direct comparison can be made with non-reset HRAs. We already
saw in Proposition 4.4 that, in the latter idiom, histories can be used for simulating register
behaviour. In the absence of registers, CMAs differ from non-reset HRAs solely in their
constraint of relating histories to states (and their termination behaviour, which is more
expressive). As the latter can be easily counterbalanced by obfuscating the set of states, we
obtain the following.
Proposition 8.2. For each non-reset HRA A there is a CMA A0 such that L(A) = L(A0 ).

9. Further directions
Our goal is to apply automata with histories in static and runtime verification. For static
verification, the complexity results derived in this paper may seem discouraging at first.
However, they are based on very specific representations of hard problems; in practice, we
expect programs to yield automata of simpler complexities. Experience with tools based
on coverability of TR-VASSs, like e.g. BFC [22], positively testify in that respect. Another
solution, already pursued herein, is to explore constrained versions of our machines. A
specific such variant we envisage to consider is one with restricted resets, in analogy to
e.g. [17]. In a related direction, we aim to look at abstractions that would allow us to
attack the model-checking problem for these automata, and also look at temporal logics that
capture part or all of the expressivity of HRAs.
In this work we examined nondeterministic automata but did not look at alternating
variants. This is justified by the undecidability of universality already at the level of register
automata. However, if one is willing to restrict the number of registers and histories, there
may still be room for decidability. In the case of register automata, it has been shown [15]
that alternating register automata with one register are decidable for emptiness, and become
undecidable at two registers. While these automata cannot capture languages that inherently
require more than one register, they can use alternation to express name freshness and
e.g. capture the languages L0 , L2 of the Introduction, and also a variant of L1 which uses
constants for tokenizing the input (instead of a0 ). It would be useful to examine whether a
similar restriction can yield decidable alternating HRAs, and what would their expressivity
be. Finally, a problem left open here is decidability and complexity of bisimilarity. (In a
private communication, Piotrek Hofman sketched a proof that bisimilarity is decidable.)
References
[1] S. Abramsky, D. R. Ghica, A. S. Murawski, C.-H. L. Ong, and I. D. B. Stark. Nominal games and full
abstraction for the nu-calculus. In Logic in Computer Science (LICS), 2004.
[2] T. Araki and T. Kasami. Some decision problems related to the reachability problem for Petri nets.
Theoretical Computer Science (TCS), 1976.
[3] M. Faouzi Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with
dynamic creation of threads. Logical Methods in Computer Science (LMCS), 2011.
[4] N. Benton and B. Leperchey. Relational reasoning in a nominal semantics for storage. In Typed Lambda
Calculi and Applications (TLCA), 2005.
[5] H. Björklund and T. Schwentick. On notions of regularity for data languages. Theoretical Computer
Science (TCS), 2010.

HISTORY-REGISTER AUTOMATA

31

[6] M. Bojanczyk, L. Braud, B. Klin, and S. Lasota. Towards nominal computation. In Principles of
Programming Languages (POPL), 2012.
[7] M. Bojanczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words.
Transactions on Computational Logic (TOCL), 2011.
[8] M. Bojanczyk, B. Klin, and S. Lasota. Automata theory in nominal sets. Logical Methods in Computer
Science (LMCS), 2014.
[9] M. Bojanczyk, B. Klin, S. Lasota, and S. Torunczyk. Turing machines with atoms. In Logic in Computer
Science (LICS), 2013.
[10] A. Bouajjani, S. Fratani, and S. Qadeer. Context-bounded analysis of multithreaded programs with
dynamic linked structures. In Computer Aided Verification (CAV), 2007.
[11] L. Bozzelli and P. Ganty. Complexity analysis of the backward coverability algorithm for VASS. In
Reachability Problems (RP), 2011.
[12] Rackoff C. The covering and boundedness problems for vector addition systems. Theoretical Computer
Science (TCS), 1978.
[13] C. Cotton-Barratt, A. S. Murawski, and C.-H. Luke Ong. Weak and nested class memory automata. In
Language and Automata Theory and Applications (LATA), 2015.
[14] N. Decker, P. Habermehl, M. Leucker, and D. Thoma. Ordered navigation on multi-attributed data
words. In Concurrency Theory (CONCUR), 2014.
[15] S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. Transactions on Computational Logic (TOCL), 2009.
[16] D. Figueira, S. Figueira, S. Schmitz, and P. Schnoebelen. Ackermannian and primitive-recursive bounds
with Dickson’s lemma. In Logic in Computer Science (LICS), 2011.
[17] A. Finkel and A. Sangnier. Mixing coverability and reachability to analyze VASS with one zero-test. In
Current Trends in Theory and Practice of Computer Science (SOFSEM), 2010.
[18] M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects
of Computing, 2002.
[19] O. Goldreich. Computational Complexity: A Conceptual Perspective. Cambridge University Press, 2008.
[20] R. Grigore, D. Distefano, R. L. Petersen, and N. Tzevelekos. Runtime verification based on register
automata. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2013.
[21] A. Jeffrey and J. Rathke. Towards a theory of bisimulation for local names. In Logic in Computer Science
(LICS), 1999.
[22] A. Kaiser, D. Kroening, and T. Wahl. Efficient coverability analysis by proof minimization. In Concurrency
Theory (CONCUR), 2012.
[23] M. Kaminski and N. Francez. Finite-memory automata. Theoretical Computer Science (TCS), 1994.
[24] J. Laird. A fully abstract trace semantics for general references. In Automata, Languages, and Programming (ICALP), 2007.
[25] R. J. Lipton. The reachability problem requires exponential space. Technical report, Yale University,
1976.
[26] A. Manuel and R. Ramanujam. Class counting automata on datawords. Foundations of Computer
Science (IJFCS), 2011.
[27] U. Montanari and M. Pistore. An introduction to history dependent automata. Electronic Notes in
Theoretical Computer Science (ENTCS), 1997.
[28] A. S. Murawski, S. J. Ramsay, and N. Tzevelekos. Game semantic analysis of equivalence in IMJ. In
Automated Technology for Verification and Analysis (ATVA), 2015.
[29] A. S. Murawski and N. Tzevelekos. Algorithmic nominal game semantics. In European Symposium on
Programming (ESOP), 2011.
[30] A. S. Murawski and N. Tzevelekos. Algorithmic games for full ground references. In Automata, Languages,
and Programming (ICALP), 2012.
[31] F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets.
Transactions on Computational Logic (TOCL), 2004.
[32] A. M. Pitts and I. Stark. On the observable properties of higher order functions that dynamically create
local names, or: What’s new? In Mathematical Foundations of Computer Science (MFCS), 1993.
[33] H. Sakamoto and D. Ikeda. Intractability of decision problems for finite-memory automata. Theoretical
Computer Science (TCS), 2000.

32

R. GRIGORE AND N. TZEVELEKOS

[34] S. Schmitz and P. Schnoebelen. Algorithmic aspects of WQO theory. Lecture Notes hcel-00727025v2i,
2012.
[35] P. Schnoebelen. Revisiting Ackermann-hardness for Lossy Counter Machines and Reset Petri Nets. In
Mathematical Foundations of Computer Science (MFCS), 2010.
[36] L. Segoufin. Automata and logics for words and trees over an infinite alphabet. In Computer Science
Logic (CSL), 2006.
[37] I. D. B. Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge Computing
Laboratory, 1995.
[38] N. Tzevelekos. Fresh-register automata. In Principles of Programming Languages (POPL), 2011.
[39] N. Tzevelekos and R. Grigore. History-register automata. In Foundations of Software Science and
Computation Structures (FoSSaCS), 2013.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a
copy of this license, visit http://creativecommons.org/licenses/by-nd/2.0/ or send a
letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or
Eisenacher Strasse 2, 10777 Berlin, Germany

