Effect of aromatic π-bridges on molecular structures and optoelectronic properties of A-π-D-π-A small molecular acceptors based on indacenodithiophene

Article abstract of DOI:10.1016/j.orgel.2020.106015

Investigation on the relationship between molecular structure and device performance is of great important to develop highly efficient A-π-D-π-A small molecular acceptors (SMAs). However, there is still lack of a complete and in-depth study on effects of

Full text of DOI:10.1016/j.orgel.2020.106015

Available online at www.sciencedirect.com
Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
www.elsevier.com/locate/entcs
Expressiveness of Hybrid Temporal Logic on
Data Words
Ahmet Kara1 ,2 Thomas Schwentick1 ,3
TU Dortmund, Germany
Abstract
Hybrid temporal logic (HTL) on data words can be considered as an extension of the logic LTL↓ introduced
by Demri and Lazic [3]. The paper compares the expressive power of HTL on data words with that of LTL↓.
It is shown that there are properties of data words that can be expressed in HTL with two variables but
not in LTL↓. On the other hand, every property that can be expressed in HTL with one variable can also
be expressed in LTL↓ with one variable. The paper further studies the succinctness of HTL in comparison
with LTL↓ and shows that the number-of-variables hierarchy of HTL is infinite.
Keywords: Hybrid logics, temporal logics, data words.
1 Introduction
In this paper, a data word is a finite sequence of positions which carry a data value
and a set of propositions. Logics on data words have been investigated a lot in recent
years, e.g., in [2,3] and many follow-up papers. In this paper we consider hybrid
temporal logic on data words. As an example, the formula ϕ = G(p∧↓x.F(q ∧∼x))
expresses that for every position carrying the proposition p there is a position in
the future that has the same data value and carries proposition q. The quantifier
↓x binds variable x to the current position and ∼x compares the current data value
with the value at the position bound to x. The logic further allows formulas as
@x.χ (evaluate χ at position x) and x (true if x is the current position).
Hybrid temporal logic was first considered in [13], and intensively studied on
linear structures, e.g., in [1,9,15]. It has been noted before that the logic LTL↓
on data words, introduced in [3] is essentially a hybrid temporal logic [4,5,19]. In
1
We acknowledge the financial support by the German DFG under grant SCHW 678/4-1.
2
Email: ahmet.kara@cs.uni-dortmund.de
3
Email: thomas.schwentick@cs.tu-dortmund.de
1571-0661 © 2011 Elsevier B.V.
doi:10.1016/j.entcs.2011.10.010
Open access under CC BY-NC-ND license.

116
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
fact, LTL↓ can be considered as the syntactical fragment of hybrid temporal logic
without formulas of the forms @x.χ and x. Formally, in LTL↓, variables are bound
to data values instead of positions. However, the difference does not matter as long
as the only way to refer to a variable x is through an atomic formula ∼x. Thus,
formula ϕ above can be seen as a LTL↓ formula.
We study hybrid temporal logics with future and past temporal operators (HTL)
on data words and compare its expressive power with that of LTL↓.
There is a correspondence between HTL and LTL↓ on one hand and automata
models for data words, on the other hand. As shown in [4], every property express-
ible in LTL↓ can be decided by an alternating register automaton. The logic HTL,
on the other hand, is captured by pebble automata. This follows directly from the
fact that HTL can only express first-order properties and that even deterministic
one-way pebble automata can express 4 all first-order properties on data words [12].
The relationship between LTL↓ and alternating register automata together with
previous results in [12] immediately yields a separation between LTL↓ and HTL. In-
deed, in [12] a first-order expressible property of data words was defined that cannot
be decided by alternating register automata and therefore cannot be expressed by
LTL↓. On the other hand, it is not hard to show that HTL can express all first-order
properties of data words and thus also this particular property. We strengthen this
result by showing that a similar property that still cannot be expressed in LTL↓
can be expressed by an HTL formula with only two variables, thus establishing
LTL↓ ≤ HTL2.
Interestingly, the difference between HTL and LTL↓ vanishes when we restrict
formulas to one variable. Our main result shows that HTL1 = LTL↓1.
We further show that
HTL1-formulas can be exponentially more succinct than LTL↓-formulas and HTL-
formulas can even be non-elementarily more succinct than LTL↓-formulas; and
that
•
•
the variable hierarchy of HTL on data strings is infinite. To this end, we show
that Rossman’s result that the variable hierarchy for first-order logic on finite
ordered graphs is strict can be carried over to data strings.
Most of our results also hold for infinite data words (cf. Section 5).
We already mentioned related work above. The paper is organized as follows.
After the preliminaries (Section 2) we show in Section 3 the results on HTL with at
least two variables and in Section 4 the results on HTL1. We conclude in Section 5.
Due to lack of space we do not present all proofs in full detail. In particular, some
correctness proofs for translations of formulas are missing. However, we always tried
to design the translated formulas so that the correctness can be verified easily by
the reader.
We thank Thomas Zeume and an anonymous reviewer for many useful sugges-
tions.
4
Formally, this was only shown for finite data words over an empty proposition set in [12]. However, the
proof simply goes through for data words.

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
117
2 Preliminaries
Data Words. Let Σ be a finite set of propositions and D an infinite set of data
values. A string over Σ is a finite sequence of elements from 2Σ. A data word
over Σ is a finite sequence of elements from (2Σ × D). A data word is denoted by
P1
d1
· · · P , where P1, . . . , Pn ∈ 2 and d1, . . . , dn ∈ D. If p ∈ Pi we say that i is
n
Σ
w =
dn
labelled with p and that i is a p-position. We call di the data value of position i. If
p
d
{p}
d
Pi is a singleton set {p} we write instead of
.
Logics. Hybrid temporal logic (HTL) on data words over Σ is an extension of the
linear temporal logic LTL (see e.g. [7]) by past operators and variables. The syntax
of HTL is as follows.
ϕ ::= p | x | ↓x.ϕ | ∼x | @x.ϕ | Xϕ | ϕUϕ | X−ϕ | ϕU−ϕ | ¬ϕ | ϕ ∧ ϕ
where p ∈ Σ and x is a variable from an infinite set VAR of variables.
As usual, we consider the other logical operators ∨, → and ↔ and the other
temporal operators Fϕ := ꢁUϕ, F−ϕ := ꢁU−ϕ, Gϕ := ¬F¬ϕ and G−ϕ := ¬F−¬ϕ
as abbreviations. The operators X, U, F, G, X−, U−, F−, G− are called temporal op-
erators. We refer to the operators X, U, F, G as future operators and to the latter
four as past operators.
For a data word w with |w| = n an assignment is a mapping g : VAR →
{1, . . . , n}. For an assignment g, a variable x and a position i in w, gix denotes the
mapping defined by gix(x) := i and gix(y) := g(y) for all y = x. The semantics of a
P1
d1
· · · P over Σ, a
n
HTL formula over Σ is defined with respect to a data word w =
position i in w and an assignment g for w.
dn
•
•
•
•
•
•
w, g, i |= p if p ∈ Pi
w, g, i |= ↓x.ϕ if w, gix, i |= ϕ
w, g, i |= ∼x if di = dg(x)
w, g, i |= @x.ϕ if w, g, g(x) |= ϕ
w, g, i |= ¬ϕ if w, g, i |= ϕ
w, g, i |= x if g(x) = i
•
•
•
w, g, i |= ϕ ∧ ψ if w, g, i |= ϕ and w, g, i |= ψ
w, g, i |= Xϕ if i < n and w, g, i + 1 |= ϕ
w, g, i |= ϕUψ if there is a j with i ≤ j ≤ n and w, g, j |= ψ and
w, g, k |= ϕ for all k with i ≤ k < j
w, g, i |= X−ϕ if i > 1 and w, g, i − 1 |= ϕ
w, g, i |= ϕU−ψ if there is a j with 1 ≤ j ≤ i and w, g, j |= ψ and
w, g, k |= ϕ for all k with j < k ≤ i
•
•
If at most one variable x occurs in ϕ and g(x) = j, we also write w, j, i |= ϕ
instead of w, g, i |= ϕ. We say that a data word w satisfies a formula ϕ (denoted as
w |= ϕ) if w, g, 1 |= ϕ where g(x) := 1 for all x ∈ VAR.
The notions of bound and free variable occurrences and of closed formulas are
defined as usual. We say that two formulas ϕ1 and ϕ2 are equivalent (denoted
as ϕ1 ≡ ϕ2) if w, g, i |= ϕ1 if and only if w, g, i |= ϕ2 for all data words w, all

118
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
assignments g and all positions i of w. The formulas are initially equivalent if for
all data words w and assignments g it holds w, g, 1 |= ϕ1 if and only if w, g, 1 |= ϕ2.
For two logics L1 and L2 we write L1 ≤ L2 if for every closed formula ϕ1 of L1 there
is an equivalent formula ϕ2 in L2. Furthermore, L1 ≡ L2 if L1 ≤ L2 and L2 ≤ L1.
Freeze LTL (LTL↓) ([3]) is the fragment of HTL that does not allow (sub-)
formulas of the form x and @x.ϕ. The fragments of HTL and LTL↓ where at most
k variables are allowed, are denoted as HTLk and LTL↓k, respectively. For a set O
of temporal operators and a logic L, we denote by L(O) the fragment of L in which
only operators from O are used. The extension of LTL by past operators is denoted
as PLTL.
3 HTL with more than one variable
In this section, we consider HTL without a bound on the number of variables. We
first show that HTL is more expressive than LTL↓ and that it actually only needs
two variables to express a property that LTL↓ cannot express. Furthermore, we show
that the variable hierarchy for HTL is infinite and that HTL is non-elementarily
more succinct than LTL↓.
3.1 Expressiveness
The expressive power of HTL on data words coincides with the expressive power of
first-order logic (FO). Here, first-order formulas can use the atomic formulas p(x)
(stating that proposition p holds at position x), x < y (stating that position y is to
the right of position x) and x ∼ y (stating that x and y carry the same data value).
Theorem 3.1 HTL ≡ FO on data words.
Proof. For every k ≥ 1 every HTLk-formula can be translated into a first-order
formula with at most k + 3 variables by a standard translation (similarly as in,
e.g. [9]). The translation of first-order formulas into HTL-formulas is also along
standard lines. A first-order formula ϕ can be translated into a HTL-formula ϕꢀ as
follows (we omit the Boolean cases).
(∃xψ)ꢀ = FF−↓x.ψꢀ
(x = y)ꢀ = FF−(x ∧ y)
(x < y)ꢀ = @x.XFy
(p(x))ꢀ = @x.p
(x∼y)ꢀ = @x.∼y
•
•
•
•
•
2
It follows from existing results that HTL is strictly more expressive than LTL↓.
In [3] it was shown that every property of data words expressed by a LTL↓-formula
can be decided by a 2-way alternating register automaton. In [12], for every m ≥ 1,
a set L=m of data words was defined such that
(a) L=m is definable in first-order logic for every m, but
(b) for every m ≥ 4, there is no 2-way alternating register automaton for L=m.

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
119
Of course, (b) and [3] yield 5 that L=m cannot be defined by a LTL↓-formula, for
any m ≥ 4. By Theorem 3.1 and (a), every L=m can be expressed in HTL and thus
HTL is strictly more expressive than LTL↓. In Theorem 3.3 we show that, for every
m, there is a set Lm, similarly defined as L=m, such that Lm can be defined by a
HTL2(X, U)-formula, but there is no 2-way alternating register automaton for Lm
if m ≥ 4. Thus, HTL2(X, U) ≤ LTL↓.
A 1-hyperset over D is a finite subset of D. For m > 1, an m-hyperset over
D is a finite set of (m − 1)-hypersets over D. We assume for simplicity that D
is the set of natural numbers. We associate m-hypersets Hm(w) with data words
b1
d n1
z
z e1
w over {z, b1, e1, . . . , bm, em} as follows. A data word w =
· · · n , where d
dꢀ
j
and dꢀ are arbitrary data values, represents the 1-hyperset H1(w) = {n1, . . . , nj}.
If for some m ≥ 2 and ꢀ ≥ 0 every data word uj, 1 ≤ j ≤ ꢀ, represents an
bm
d
em
dꢀ
(m − 1)-hyperset, then the data word u = u1 · · · uꢀ
represents the m-hyperset
Hm(u) = {Hm−1(u1), . . . , Hm−1(uꢀ)}, e.g.,
ꢀ
ꢁ
b2 b1 z z e1 b1 z z z e1 b1 z z e1 e2
H2
= {{1, 2}, {7, 8, 9}, {2, 5}}.
2 1 1 2 2 3 7 9 8 2 1 2 5 9 3
If u does not represent any m-hyperset, we write Hm(u) = ⊥. For every m ≥ 1 we
define the set Lm (with the additional proposition s) as
Lm = {uds v | Hm(u) = Hm(v) = ⊥, d ∈ D}.
Proposition 3.2 ([12]) For m ≥ 4, Lm cannot be decided by a 2-way alternating
register automaton.
This proposition can be shown along the same lines as the above mentioned
results. Indeed, the result of [12] easily carries over to Lm and to the model of
2-way alternating register automata as defined in [3].
Theorem 3.3 For each m ≥ 1 the set Lm is definable in HTL2.
Proof. We define, for every m ≥ 1, a formula ϕm ∈ HTL2(X, U) such that w |= ϕm
if and only if w ∈ Lm for all data words w. The formula ϕm is a conjunction of
several subformulas. The following three subformulas together express that w is of
the form uds v with Hm(u) = ⊥ and Hm(v) = ⊥.
•
A straightforward formula χone expresses that “every position carries exactly one
proposition from {z, s, b1, . . . , bm, e1, . . . , em}.”
“w is of the form uds v, u and v start with a bm-position and end with a em-position
and there are no other positions carrying bm, em or s.”
•
χmain = bm ∧X[¬(bm ∨s∨em)U(em ∧X(s∧X(bm∧(¬(bm ∨s∨em)U(em ∧¬Xꢁ)))))]
5
Actually, the definitions of 2-way alternating register automata in [3] and [12] do not coincide completely.
However, it is not hard to see that the result of [3] also holds for the automata of [12] over data words
without propositions.

120
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
•
“Every bi-position is directly followed by a bi−1- or an ei-position, every z-position
is directly followed by a z- or an e1-position and, for i < m, every ei-position is
directly followed by a bi- or an ei+1-position.” Here, b0 denotes z.
m
m−1
ꢂ
ꢂ
χhyp = G(z → X(z ∨ e1)) ∧ (bi → X(bi−1 ∨ ei)) ∧
i=1
(ei → X(bi ∨ ei+1)).
i=1
Next, we construct a formula ψm that actually expressess Hm(u) = Hm(v).
•
The formula ψ1 checks that, if x and y are bound to b1-positions, the two 1-
hypersets whose encodings start at x and y, respectively, are equal.
ꢃ
ꢄ
ꢀ
ꢁ
ψ1 =@x.X ¬e1 ∧ ↓x.@y.X(¬e1U(¬e1∧ ∼ x)) Ue1
∧
ꢃ
ꢄ
ꢀ
ꢁ
@y.X ¬e1 ∧ ↓y.@x.X(¬e1U(¬e1∧ ∼ y)) Ue1
•
Likewise, for 2 ≤ i ≤ m the formula ψi expresses that, if x and y are bound to
bi-positions, the i-hypersets starting at x and y, respectively, are equal:
ꢃ
ꢄ
ꢀ
ꢁ
ψi = @x. bi−1 → ↓x.@y.(¬eiU(bi−1 ∧ ↓y.ψi−1)) Uei ∧
ꢃ
ꢄ
ꢀ
ꢁ
@y. bi−1 → ↓y.@x.(¬eiU(bi−1 ∧ ↓x.ψi−1)) Uei
Finally, the desired formula is ϕm = χone ∧ χmain ∧ χhyp ∧ ↓x.F(s ∧ X↓y.ψm).
Every word w = uds v ∈ Lm satisfies χone, χmain and χhyp, by construction. As
u and v represent the same hypersets, both parts of ψm are satisfied, too.
If a data word w satisfies ϕm, the formulas χone, χmain and χhyp ensure that
w is of the form uds v and that u and v encode m-hypersets. The two parts of ψm
make sure that every (m − 1)-hyperset encoded in u also occurs in v and vice versa.
Thus, the completeness and correctness of ϕm follow.
2
Corollary 3.4 HTL2 ≤ LTL↓.
A closer inspection of the proof of Theorem 3.3 gives further insights. First, the
formulas ϕm do not use any past operators and do not use atomic formulas of the
form x. On the other hand, as already observed in [15], formulas of the form @x.χ
can be replaced by formulas of the form FF−(x ∧ χ) and thus, in the presence of
past operators and atomic formulas x, there is no need for an @-operator. Thus,
we get the following corollary of the proof of Theorem 3.3.
Corollary 3.5 LTL↓ cannot express all properties expressible in
(a) HTL2(X, U) without atomic formulas of the form x, and in
(b) HTL2 without subformulas of the form @x.χ.
However, without past operators, the @-operator cannot be simulated any more.
Indeed, the future fragment of HTL without the @-operator is as expressive as the
future fragment of LTL↓ with respect to closed formulas.

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
121
Proposition 3.6 Every closed HTL(X, U) formula without the @-operator can be
translated into an equivalent LTL↓(X, U)-formula.
Proof. For k ≥ 1 let ϕ be a closed HTLk(X, U) formula without any occurrences of
@. Without loss of generality we assume that at most the variables x1, . . . , xk occur
in ϕ. The idea is that in a formula ↓x.ψ, atomic formulas x evaluate to true only
until some temporal operator has “moved” the “current position”. Thus, it suffices
is to keep track of whether a subformula of ϕ is evaluated on a position bound to a
variable or not. Depending on this, atomic formulas xi can be replaced by ꢁ or ⊥.
As an example, the formula ↓xi.Xxi is equivalent to the formula ↓xi.X⊥.
We define a mapping onS that translates, for every subset S of {x1, . . . , xk},
HTLk(X, U)-formulas ψ into LTL↓k(X, U)-formulas onS(ψ) such that for every data
word w, every assignment g and every position i of w it holds
w, g, i |= ψ ⇔ w, g, i |= onS(ψ),
if S is chosen as {xj | g(xj) = i}.
The transformation is defined as follows (we omit the Boolean operators).
•
•
•
•
•
onS(p) = p for propositions p
ꢅ
onS(∼xi) = ∼xi
onS(↓xi.χ) = ↓xi.onS∪{x }(χ)
ꢁ, if xi ∈ S
onS(xi) =
i
onS(Xχ) = Xon∅(χ)
⊥, otherwise
ꢀ
ꢁ
onS(χUχꢀ) = onS(χꢀ) ∨ onS(χ) ∧ X(on∅(χ)Uon∅(χꢀ))
•
Finally, formula ϕ is equivalent to the LTL↓k(X, U) formula on∅(ϕ).
2
We finally note that for HTL on data words similar observations can be made
as for HTL on linear frames in [9]. In particular, for k ≥ 1, every HTLk formula
can be converted into an initially equivalent HTLk+2 future formula. The idea is to
bind the first additional variable, say x, to the first position of the word. A similar
technique was used in [19] in the context of branching time logics.
Lemma 3.7 For k ≥ 1, every HTLk formula can be converted into an initially
equivalent HTLk+2(X, U) formula.
Proof. Let x and y be two additional variables. We use the following translation
of HTLk formulas ϕ into HTLk+2 formulas ϕꢀ.
(Xψ)ꢀ = Xψꢀ
(ψUχ)ꢀ = ψꢀUχꢀ
(X−ψ)ꢀ = ↓y.@x.F(Xy ∧ ψꢀ)
(ψU−χ)ꢀ: ↓y.@x.F(Fy ∧ χꢀ ∧ (y ∨ XG(Fy → ψꢀ)))
•
•
•
•
The trivial cases are omitted, here. Then, every HTLk formula ϕ is initially
equivalent to the HTLk+2(X, U) formula ↓x.ϕꢀ.
2

122
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
3.2 Hierarchy results
In this section, we show that both the HTL- and the LTL↓-hierarchy have infinitely
many levels. More precisely, there is no k > 0 such that for every i, HTLi ⊆ HTLk
or LTL↓i ⊆ LTL↓k. It turns out that this can be concluded from Rossman’s celebrated
theorem that the variable hierarchy for first-order logic on ordered graphs is strict
[14]. In the following, we denote the restriction of first-order logic to formulas with
at most k variables by FOk.
Theorem 3.8 (Rossman [14]) For every k ≥ 1, FOk ꢀ FOk+1 on finite undi-
rected, ordered graphs.
We define canonical encodings of finite undirected ordered graphs by data words
and show the following two lemmas.
Lemma 3.9 For every formula ϕ ∈ FOk there is a formula ϕꢀ ∈ LTL↓k+1 such that
for every undirected ordered graph G and every canonical encoding w of G it holds
G |= ϕ ⇔ w |= ϕꢀ.
Lemma 3.10 For every formula ϕꢀ ∈ HTLk there is a formula ϕ ∈ FO2k+6 such
that for every undirected ordered graph G and every canonical encoding w of G it
holds w |= ϕꢀ ⇔ G |= ϕ.
These two lemmas and Rossman’s result yield the following theorem.
Theorem 3.11 (a) The LTL↓k-hierarchy on data words is infinite.
(b) The HTLk-hierarchy on data words is infinite.
Proof. For the sake of a contradiction, let us assume that there is some i such that
for every j > i, LTL↓j = LTLi↓ or such that for every j > i, HTLj = HTLi. Let ϕ
be an arbitrary formula on ordered graphs from FO2i+7. By Lemma 3.9, there is a
formula ϕꢀ ∈ LTL2↓i+8 such that G |= ϕ ⇔ w |= ϕꢀ. By assumption, there is 6
a
formula ψꢀ ∈ HTLi such that for every data word w it holds w |= ψꢀ ⇔ w |= ϕꢀ. By
Lemma 3.10, there is a formula ψ ∈ FO2i+6 such that for every undirected ordered
graph G and every canonical encoding w of G it holds w |= ψꢀ ⇔ G |= ψ.
Thus, ϕ ≡ ψ. As ϕ was arbitrarily chosen from FO2i+7 we can conclude that
FO2i+7 = FO2i+6, the desired contradiction.
2
It only remains to define canonical encodings and to prove the two lemmas.
In the following, we only consider graphs without self-loops. This is consistent
with Rossman’s Theorem. We say that a data word w is a canonical encoding of a
finite ordered undirected graph G = (V, E, <) if the following conditions hold.
•
w has |V | + 2|E| positions,
· a node position p(u), for every u ∈ V and
· an edge position q(u, v), for every 7 edge (u, v).
If we assume that the LTL↓-hierarchy collapses then we get a formula ψꢀ ∈ LTL↓i at this point which is,
6
however, also in HTLi.
7
Every edge (u, v) gives rise to two positions, q(u, v) and q(v, u).

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
123
•
•
Node positions p(u) have a unique data value and carry the proposition p.
For every u, v, (u, v) ∈ E, the edge positions q(u, v) and q(v, u) have the same data
value (and this value does not occur otherwise) and do not carry any propositions.
The order of the positions obeys the following rules, for every u, uꢀ, v, vꢀ ∈ V :
•
· p(u) < p(v) if u < v in G.
· p(u) < q(uꢀ, vꢀ) if u ≤ uꢀ.
· q(u, v) < p(uꢀ) if u < uꢀ.
· q(u, v) < q(u, vꢀ) if v < vꢀ.
It should be noted that these rules define a unique order on every canonical
data string w.
a
c
b
Example 3.12 If in the undirected finite graph G =
p ∅ ∅ p ∅ ∅ p ∅ ∅ ∅ p ∅
the nodes are
d
ordered by a < b < c < d, then
is a canonical encoding of G. It
7 8 3 2 8 1 6 3 1 5 4 5
should be observed that the underlying linear order of data values (1 < 2 < 3 < · · · )
is not relevant for the encoding.
A maximal subword in a canonical encoding where only the first position is
labeled by p is called a variable block. As an example, the subword from the 4th to
the 6th position of the above encoding constitutes a variable block.
Proof of Lemma 3.9. We assume without loss of generality that formulas from
FOk only use variables x1, . . . , xk. The translation ϕ → ϕꢀ can be defined inductively
as follows.
(xi = xj)ꢀ = FF−(∼xi ∧ ∼xj)
•
(xi < xj)ꢀ = FF−(∼xi ∧ XF∼xj)
E(xi, xj)ꢀ = FF−(∼xi ∧ ¬pU↓y.FF−(∼y ∧ ¬pU−(∼xj ∧ ∼xi))
(∃xiψ)ꢀ = FF−↓xi.(p ∧ ψꢀ)
(¬ψ)ꢀ = ¬ψꢀ
(ψ ∧ χ)ꢀ = ψꢀ ∧ χꢀ
•
ꢀ
ꢁ
•
•
•
•
In ϕꢀ, variables xi are always only bound to first positions of variable blocks.
Whether two nodes bound to xi and xj are connected by an edge can then be
tested by checking whether the blocks starting at xi and xj, respectively, share
some data value.
2
Proof of Lemma 3.10. The proof consists of two steps. First, we construct, as
in the proof of Theorem 3.1, an FOk+3-formula ϕꢀꢀ that is equivalent to ϕꢀ on data
words.
Then we transform ϕꢀꢀ into ϕ by means of a quantifier-free logical interpretation
[6, Section 11.2] that defines, for every finite ordered undirected graph G = (V, E, <
), a (unique) representation of the canonical encodings of G on the set V × V .
However, the translation of ϕꢀꢀ into ϕ requires two variables, xi, xiꢀ, for every variable

124
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
xi of ϕꢀꢀ, thus resulting in a formula with 2k+6 variables. More precisely, the logical
interpretation Φ = (ϕU , ϕp, ϕ<, ϕ∼) is defined as follows.
•
ϕU (x1, x2) defines the set of pairs that are actual positions of the representation
of the canonical encodings. Thus, it is just x1 = x2 ∨ E(x1, x2).
•
ϕp(x1, x2) defines the positions that carry the proposition p and is thus just
x1 = x2.
•
ϕ<(x1, x2, y1, y2) defines the linear order on positions. It is
(x1 = x2 ∧ (x1 < y1 ∨ (x1 = y1 ∧ x2 = y2)))∨
(x1 = x2 ∧ (x1 < y1 ∨ (x1 = y1 ∧ x2 < y2))).
•
Finally, ϕ∼(x1, x2, y1, y2) defines the pairs of positions that have the same data
value. It is simply x1 = y2 ∧ x2 = y1.
It is not hard to see that Φ indeed defines, for every G, the unique representation
of the canonical encodings of G.
2
Remark 3.13 We conjecture that both hierarchies are even strict and that this can
be shown in a similar way as the strictness of the FOk-hierarchy can be concluded
from its infinity [14]. However, we did not have time to figure out the details before
the deadline for this submission.
3.3 Succinctness
We have seen before that HTL2 can express properties that cannot be expressed by
any LTL↓-formula. We show next that there are also LTL↓-expressible properties
that can be expressed non-elementarily more succinct in HTL2. This is basically a
corollary from results in [17], [16] and [15] and the observation that on data words
in which all positions carry the same data value, LTL↓ is expressively equivalent to
PLTL.
In [17] it is shown that there are star-free regular expressions (αn)n≥1, built from
union, concatenation, and negation, such that, there is no elementary function f
for which f(n) bounds the length of the size of the smallest string satisfying αn,
for every n ≥ 1. In [8] it is explained how for every star-free regular expression α
one can build an equivalent FO formula. Following a similar technique, [15] gives
a translation from star-free regular expressions to hybrid logic formulas. In our
setting, the translation yields HTL-formulas of linear size in |αn|. On the other
hand, [16] proves that every satisfiable LTL formula ψ can be satisfied by a string
of length at most exponential in |ψ|. Combining these results we get:
Proposition 3.14 HTL2(X, F) is non-elementarily more succinct than LTL↓.
4 One Variable
In this section, we show our main result, that HTL1 ≡ LTL↓1 on data words. Further,
we prove that HTL1(F) is exponentially more succinct than LTL↓.

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
125
4.1 Expressiveness
The translation of HTL1 to LTL↓1 relies on a kind of separation property. We
show that if ϕ = ↓x.χ then the “top level” of χ can be rewritten into a Boolean
combination of future and past formulas.
We introduce some new notation for the proof.
For a data word w, a position i of w and a set Φ of HTL1-formulas we denote by
(w, i)Φ the string that is obtained from w by removing the data values and adding
to each position j all propositions pψ, ψ ∈ Φ, for which w, i, j |= ψ.
A subformula ψ of a HTL1-formula ϕ is called a top-level subformula of ϕ if ψ
is not in the scope of any ↓x quantifier.
−→
For every HTL1-formula ϕ we let T (ϕ) be the set of all top-level subformulas of
ϕ that are of one of the forms ↓x.χ, ∼x or @x.χ and of all formulas @x.X−χ and
@x.χU−θ for which X−χ or χU−θ, respectively, is a top-level subformula of ϕ. We
−→
define Tx(ϕ) analogously, but with the additional atomic formula x.
If j is a position of a data word w we write w[j, . . .) for the subword of w starting
at position j.
−→
Lemma 4.1 For every HTL1-formula ϕ there is an LTL-formula ϕ such that for
every data word w and all positions i, ꢀ of w it holds
−→
−→
w, ꢀ, i |= ↓x.ϕ ⇔ (w, i)T (ϕ), i |= ϕ .
−→
The size of ϕ is at most triply exponential in |ϕ|.
Proof. We inductively define, for every top-level subformula ψ of ϕ, a PLTL-
ꢆ
formula ψ such that, for all positions i, j with j ≥ i, it holds
−→
w, i, j |= ψ ⇔ (w, i)T (ϕ), j |= ψ.
(1)
x
ꢆ
ꢆ
To this end, let ψ be
•
•
•
•
•
p if ψ is a proposition p;
pψ if ψ is of one of the forms x, ∼x, ↓x.χ, @x.χ;
Xχꢆ if ψ = Xχ;
ꢆ
χꢆUθ, if ψ = χUθ;
(¬px ∧ X−χꢆ) ∨ (px ∧ p@x.X−χ) if ψ = X−χ;
(¬px ∧ χꢆ)U ((¬px ∧ θ) ∨ (px ∧ p@x.χU−θ)) if ψ = χU−θ.
−
ꢆ
•
That is, the usual evaluation of past operators is restricted to positions ≥ i. If this
is insufficient then the new propositions are used. It is straightforward to show by
induction that Equation 1 indeed holds.
Let now ϕ1 be the formula that results from ϕꢆ by replacing every occurrence of
−→
px with ¬X−ꢁ. Clearly, for all data words w and positions i ≤ j, (w, i)T (ϕ), j |= ϕꢆ
x
−→
if and only if (w, i)T (ϕ)[i, . . .), (j − i + 1) |= ϕ1.

126
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
By [10, Theorem 2.4] the PLTL-formula ϕ1 can be effectively translated into an
−→
LTL-formula ϕ that is initially equivalent to ϕ1. Moreover, by [11] it follows that
−→
ϕ can be computed in triply exponential time. As the positions < i are irrelevant
−→
for the validity of ϕ at position i, altogether the lemma follows.
2
←−
Similarly, we let, for every HTL1-formula ϕ, T (ϕ) be the set of all top-level
subformulas of ϕ that are of one of the forms ↓x.χ, ∼x, @x.χ and of all formulas
@x.Xχ and @x.χUθ for which Xχ or χUθ, respectively, is a top-level subformula of
ϕ. Analogously we get the following lemma.
←−
Lemma 4.2 For every HTL1-formula ϕ there is a PLTL-formula ϕ which does
not use any future operator such that for every data word w and all positions i, ꢀ of
w it holds
←−
←−
w, ꢀ, i |= ↓x.ϕ ⇔ (w, i)T (ϕ), i |= ϕ .
←−
The size of ϕ is at most triply exponential in |ϕ|.
Theorem 4.3 Every closed HTL1 formula can be translated into an equivalent
LTL↓1 formula of at most triply exponential size.
Proof. It suffices to prove that for every HTL1 formula ϕ there is a LTL↓1 formula
ϕꢀ of triply exponential size with ↓x.ϕ ≡ ↓x.ϕꢀ. We show this by induction on the
size of ϕ. Thanks to the equivalences
•
•
•
•
•
•
↓x.p ≡ p,
↓x.x ≡ ꢁ,
↓x.∼x ≡ ꢁ,
↓x.¬ψ ≡ ¬↓x.ψ,
↓x.@x.ψ ≡ ↓x.ψ,
↓x.(ψ ∧ χ) ≡ ↓x.ψ ∧ ↓x.χ
we can assume that ϕ is of one of the forms (1) ψUχ, (2) Xψ, (3) ψU−χ, (4)
X−ψ.
−→
We first consider the cases (1) and (2). Let ϕ be as guaranteed by Lemma 4.1.
Thus, for every data word w and all positions i, ꢀ of w, it holds
−→
−→
w, ꢀ, i |= ↓x.ϕ ⇔ (w, i)T (ϕ), i |= ϕ .
−→
Clearly, replacing every atomic formula p∼x by ∼x in ϕ and evaluating the formula
−→
in the data word resulting from (w, i)T (ϕ)[i, . . .) by putting back the data values
−→
from w does not change the validity of ϕ . Likewise, replacing every atomic formula
p↓x.ψ by the formula ↓x.ψꢀ, where ψꢀ is a LTL↓1-formula equivalent to ψ obtained by
induction, does not change the validity either. We denote the resulting formula by
ϕ.
It only remains to eliminate atomic formulas of the kind p@x.ψ from ϕ. For every
−→
assignment α : T (ϕ) → {ꢁ, ⊥} let ϕα be the formula resulting from ϕ by replacing
every occurrence of an atomic formula p@x.ψ with α(@x.ψ). We finally let
ꢇ
ꢂ
ꢂ
ꢀ
ꢁ
ϕꢀ =
ϕα ∧
ψꢀ ∧
¬ψꢀ ,
−→
−→
−→
α: T (ϕ)→{ꢁ,⊥}
@x.ψ∈ T (ϕ)
α(@x.ψ)=ꢁ
@x.ψ∈ T (ϕ)
α(@x.ψ)=⊥

A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
127
where ψꢀ is again a LTL↓1-formula equivalent to ψ obtained by induction that does
not use any additional propositions anymore.
The cases (3) and (4) are completely analogous.
The size of the resulting formula is dominated by the (at most) triply exponential
−→
size of ϕ . The elimination of @ only contributes an exponential factor and we end
up with a formula of at most triply exponential size.
2
4.2 Succinctness
Even though HTL1 ≡ LTL↓1, HTL1 can express some properties exponentially more
succinct than LTL1↓ and, actually, even LTL↓.
Proposition 4.4 HTL1(F) is exponentially more succinct than LTL↓.
Proof. The proof essentially follows the proof of [8, Theorem 3 (1)] that FO2
is exponentially more succinct than unary LTL. Let En be the property “Any
two positions of the word that agree on propositions p1, p2, . . . , pn also agree on
proposition p0.” and let Ln be the set of data words fulfilling En in which all
positions have the same data value. For every n ≥ 1, Ln is expressed by the
following HTL1(F) formula of length O(n):
ꢈ
n
G↓x.G ∼ x ∧ G[↓x.G( i=1(pi ↔ @x.pi) → (p0 ↔ @x.p0))].
Let us assume now that, for every n, there is a LTL↓-formula ψn expressing Ln
and |ψn| = 2o(n). This formula can be translated into a formula χn of roughly the
same size that expresses En on words without data. Similarly as in [18], there is,
o(n)
for every n, a non-deterministic automaton for χn of size 2|χ | = 22 . However,
n
n
it can be shown as in [8] that every automaton for En requires at least 22 states,
the desired contradiction.
2
5 Discussion
In this paper, we compared the expressive power of hybrid temporal logic on data
words with LTL↓. Although HTL is more powerful in general, the two logics coincide
if only one variable is allowed.
The main results of this paper carry over to data words of infinite length. For
Corollary 3.4 and Theorem 3.11 this simply holds because the separating languages
can be easily turned into ω-languages by padding with an infinite number of posi-
tions. The generalization of Theorem 4.3 to infinite data words is also straightfor-
ward. Here, it is important that the result of [11] was already shown for ω-strings.
Clearly, all considered logics have an undecidable satisfiability problem (for LTL1↓
this was shown in [3]). However, the model checking remains largely unexplored,
especially for the case of infinite data words.
As already mentioned in Section 3, we conjecture that the variable-hierarchy for
HTL and LTL↓ are both strict.

128
A. Kara, T. Schwentick / Electronic Notes in Theoretical Computer Science 278 (2011) 115–128
References
[1] Carlos Areces, Patrick Blackburn, and Maarten Marx. The computational complexity of hybrid
temporal logics. Logic Journal of the IGPL, 8(5):653–679, 2000.
[2] Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-variable
logic on words with data. In LICS, pages 7–16. IEEE Computer Society, 2006.
[3] Stephane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. In LICS
’06: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, pages 17–26,
Washington, DC, USA, 2006. IEEE Computer Society.
[4] St´ephane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans.
Comput. Log., 10(3), 2009. Full version of [3].
[5] St´ephane Demri, Ranko Lazi´c, and David Nowak. On the freeze quantifier in constraint LTL:
Decidability and complexity. Inf. Comput., 205(1):2–24, 2007.
[6] Heinz-Dieter Ebbinghaus and J¨org Flum. Finite Model Theory. Springer, Heidelberg, 2005.
[7] E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume
B: Formal Models and Sematics (B), pages 995–1072. 1990.
[8] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary
temporal logic. Information and Computation, 179(2):279 – 295, 2002.
[9] Massimo Franceschet, Maarten de Rijke, and Bernd-Holger Schlingloff. Hybrid logics on linear
structures: Expressivity and complexity. In TIME, pages 166–173, 2003.
[10] Dov M. Gabbay. The declarative past and imperative future: Executable temporal logic for interactive
systems. In Temporal Logic in Specification, pages 409–448, 1987.
[11] Nicolas Markey. Temporal logic with past is exponentially more succinct, concurrency column. Bulletin
of the EATCS, 79:122–128, 2003.
[12] Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite
alphabets. ACM Trans. Comput. Log., 5(3):403–435, 2004.
[13] Arthur Prior. Past, Present, and Future. Oxford University Press, 1967.
[14] Benjamin Rossman. On the constant-depth complexity of k-clique. In STOC ’08: Proceedings of the
40th annual ACM symposium on Theory of computing, pages 721–730, New York, NY, USA, 2008.
ACM.
[15] Thomas Schwentick and Volker Weber. Bounded-variable fragments of hybrid logics. In STACS, pages
561–572, 2007.
[16] A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J.
ACM, 32(3):733–749, 1985.
[17] L. Stockmeyer. The complexity of decision problems in automata and logic, 1974. Ph.D. Thesis, MIT,
1974.
[18] Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification
(preliminary report). In LICS, pages 332–344. IEEE Computer Society, 1986.
[19] Volker Weber. Branching-time logics repeatedly referring to states. Journal of Logic, Language and
Information, 18(4):593–624, 2009.