Stéphane Demri
email: demri@lsv.ens-cachan.fr

Deepak D'souza
email: deepakd@csa.iisc.ernet.in

Régis Gascon
email: gascon@lsv.ens-cachan.fr

A Decidable Temporal Logic of Repeating Values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Introduction

Temporal logic with freeze. In logical languages, the freeze mechanism allows to store a value in a register and to test later the value in the register with a current value. This operator is useful to compare values at distinct states of Kripke-like structures. The freeze quantifier has found applications in realtime logics [START_REF] Th | Half-order modal logic: how to prove real-time properties[END_REF], in hybrid logics [START_REF] Goranko | Hierarchies of modal and temporal logics with references pointers[END_REF][START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF], in modal logics with predicate λ-abstraction [START_REF] Fitting | Modal logic between propositional and first-order[END_REF] and for the specification of computations of systems with unboundedly many locations as resources [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF]. Although it is known that the freeze operator can lead to undecidability (even with only equality on data [START_REF] Lisitsa | Temporal logic with predicate λ-abstraction[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]), many decidable temporal logics have a freeze mechanism, sometimes implicitly, see e.g. [START_REF] Alur | A really temporal logic[END_REF][START_REF] Laroussinie | Temporal logic with forgettable past[END_REF][START_REF] Kupferman | Memoryful Branching-Time Logic[END_REF]. Recent developments have shown the ubiquity of the freeze operator [LP05,tCF05,DLN07,Laz06,Seg06] and its high expressive power as witnessed by the Σ 1 1 -completeness results shown in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF].

The need to design decidable fragments of simple linear-time temporal logic LTL with the freeze quantifier stems from [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Lazić | Safely freezing LTL[END_REF] and most known decidable fragments in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Lazić | Safely freezing LTL[END_REF] does not allow unrestricted use of negation. Still, finitary and infinitary satisfiability for Boolean combinations of safety formulae (with a unique register) is decidable [START_REF] Lazić | Safely freezing LTL[END_REF]. Potential applications range from the verification of infinite-state systems [START_REF] Th | Half-order modal logic: how to prove real-time properties[END_REF][START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF] to querying XML documents or more modestly data strings [BMS + 06,Seg06]. In the paper, we are interested in studying fragments of LTL with the freeze operator that are decidable in the finitary and infinitary cases, that allow unrestricted use of negation (by contrast to the flat fragments in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF]) and that allow all standard past-time operators (by constrast to what is done in [BMS + 06,DL06]). Even in terms of expressive power, the fragment newly shown decidable in the paper can express the "nonce property" and its negation (all the values of a variable are different at every position). Moreover, in [WZ00, Sect. 7], the authors advocate the need to consider infinitary disjunction of the form i>0 x = X i y where X i y refers to the value of y at the i th next position. This states that a future value of y is equal to the current value of x. Our fragment can express this property, with the formula x = ♦y, as well as the dual one: i>0 x = X i y can be expressed by the formula ¬(x = ♦y). In the paper we introduce the constraint logic CLTL(N, =) with atomic formulae x = ♦y and past-time operators X -1 and S. This logic is denoted by CLTL ♦ . Hence, in CLTL ♦ , the freeze quantifier is only used to specify that some values are repeated. Even though CLTL ♦ does not enjoy first-order completeness, see e.g. [START_REF] Rabinovich | Decidability and expressive power of real time logics[END_REF], it satisfies interesting computational properties as shown below.

Our contribution. We show that finitary and infinitary satisfiability for CLTL ♦ with temporal operators {X, X -1 , S, U} is decidable. We provide a uniform proof for the finite and infinite cases based on some substantial extension of the automaton-based approach for (constraint) LTL from [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF]. The possibility to compare two values at unbounded distance requires a special class of counter automata for which finitary and infinitary nonemptiness is shown decidable. To do so, we take advantage of a deep result from [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF] establishing that verifying fairness properties based on the temporal operator GF ("always eventually") in Petri nets is decidable. By contrast model-checking for full LTL over Petri nets is undecidable [START_REF] Howell | Problems concerning fairness and temporal logic for conflict-free Petri nets[END_REF] (see also [START_REF] Esparza | On the decidability of model checking for several µ-calculi and Petri nets[END_REF] with lineartime mu-calculi). Observe that infinitary CLTL ♦ is the first decidable fragment of CLTL ↓ 1 (N, =) [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF] with an unrestricted use of negation and that contains all the temporal operators from {X, X -1 , S, U}. A nice by-product of our technique is that the extensions with temporal operators definable in Monadic Second Order Logic (MSOL) or with x = ♦ -1 y ("a value of y in the past is equal to the current value of x") are also decidable. Finally, we show that finitary and infinitary satisfiability for CLTL ♦ restricted to one variable is pspace-complete.

Because of lack of space, omitted proofs can be found in [START_REF] Demri | A decidable temporal logic of repeating values[END_REF].

Temporal Logic with Repeating Values

Let VAR = {x 1 , x 2 , . . .} be a countably infinite set of variables. The formulae of the logic CLTL ♦ are defined as follows:

φ ::= x = X i y | x = ♦y | φ ∧ φ | ¬φ | Xφ | φUφ | X -1 φ | φSφ
where x, y ∈ VAR and i ∈ N. Formulae of the form either x = X i y or x = ♦y are said to be atomic and an expression of the form X i x (i next symbols followed by a variable) is called a term. Given a set of temporal operators definable from those in {X, X -1 , S, U} and k ≥ 0, we write CLTL ♦ k (O) to denote the fragment of CLTL ♦ restricted to formulae with temporal operators from O and with at most k variables.

A valuation is a map VAR → N and a model σ is a non-empty sequence of valuations either finite or infinite. All the subsequent developments can be equivalently done with the domain N replaced by an infinite set D since only equality tests are performed. We write |σ| to denote the length of σ. The satisfaction relation is defined inductively as follows where σ is a model and 0 ≤ i ≤ |σ| -1:

-σ, i |= x = X j y iff i + j ≤ |σ| -1 and σ(i)(x) = σ(i + j)(y), -σ, i |= x = ♦y iff there exists j > 0 s.t. i+j ≤ |σ|-1 and σ(i)(x) = σ(i+j)(y), -σ, i |= φ ∧ φ iff σ, i |= φ and σ, i |= φ , σ, i |= ¬φ iff σ, i |= φ, -σ, i |= Xφ iff i + 1 ≤ |σ| -1 and σ, i + 1 |= φ, -σ, i |= X -1 φ iff i > 0 and σ, i -1 |= φ, -σ, i |= φUφ iff there is i ≤ j ≤ |σ| -1 s.t. σ, j |= φ and for every i ≤ l < j, σ, l |= φ. -σ, i |= φSφ iff there is 0 ≤ j ≤ i s.t. σ, j |= φ and for j ≤ l < i, σ, l |= φ.
We write σ |= φ if σ, 0 |= φ. We shall use the standard abbreviations about the temporal operators (G, F, F -1 , . . . ) and Boolean operators (∨, ⇒, . . . ). We use the notation X i x = X j y as an abbreviation for X i (x = X j-i y) (when i ≤ j).

The finitary [resp. infinitary] satisfiability problem consists in checking whether given a formula φ, there is a finite [resp. infinite] model such that σ |= φ. It is known that finitary satisfiability for LTL can be easily reduced in logspace to infinitary satisfiability by introducing for instance an additional propositional variable p and by requiring that pUG¬p holds true. In that way, p holds true at every state of a prefix and p does not hold on the complement suffix. The same principle does not apply to reduce finitary satisfiability for CLTL ♦ to infinitary satisfiability even by introducing additional variables in order to simulate a propositional variable. This is due to the additional atomic formulae of the form x = ♦y. That is why we distinguish the two problems in this paper.

We note that a constraint of the form x diff ♦y ("the value of x differs from some future value of y") can be expressed in CLTL ♦ :

x diff ♦y ⇔ (¬(x = Xy) ∧ X ) ∨ ((x = Xy) ∧ X(y = Xy)U((y = Xy) ∧ X ))) (1)
With infinite models, the conjunct X can be deleted. We could also introduce constraints of the form x = X -i y but this can be expressed in the language using the equivalence x = X -i y ⇔ X -i ∧ X -i (y = X i x). Similarly, CLTL ♦ can express whether a variable is a nonce by the formula G¬(x = ♦x). The formula below states a valid property when x and y are nonces:

(G¬(x = ♦x) ∧ G¬(y = ♦y)) ⇒ G(x = y ⇒ ¬(x = ♦y)).
Other properties witnessing the high expressive power of CLTL ♦ can be found in [LP05, Sect.3] about systems of pebbles evolving in time.

Apart from the above-mentioned problems, we could also consider standard model-checking problems that can be reduced to the satisfiability problem. Indeed, we can define a suitable class of automata such that the execution of any automaton of this class can be encoded into a CLTL ♦ formula.

Known extensions of CLTL ♦

In this section, we recall the definition of a few known extensions of CLTL ♦ which is useful for future comparisons. The logic CLTL ♦ is clearly a fragment of the logic CLTL ↓ (N, =) introduced in [DLN07] and restricted to one register. An equivalent logic of CLTL ↓ (N, =) is denoted by CLTL ↓ in this paper and it is defined as follows. We consider an additional set of registers REG = {r 1 , r 2 , . . .} and the formulae of CLTL ↓ are defined as those of CLTL ♦ except that we allow only atomic formulae of the form r = x where r ∈ REG and x ∈ VAR, and we add the inductive clause ↓ r=x φ. The satisfaction relation is parameterized by a register assignment ρ

: REG → N with σ, i |= ρ ↓ r=x φ iff σ, i |= ρ[r →σ(i)(x)] φ and σ, i |= ρ r = x iff ρ(r) = σ(i)(x).
Consequently, the atomic formula x = ♦y in CLTL ♦ can be naturally encoded in CLTL ↓ by ↓ r=x XF(r = y) and x = X i y by ↓ r=x X i (r = y).

We write CLTL ↓ (k,k ) (O) to denote the fragment of CLTL ↓ restricted to the temporal operators from O with at most k variables and k registers. Following the notation from [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], for α ≥ 0 we write LTL ↓ α (∼, O) to denote the fragment CLTL ↓

(1,α) (O) restricted to atomic formulae of the form r = x.

A decidable fragment of finitary satisfiability

It is shown in [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF] that CLTL ↓ is strictly more expressive than its freezefree fragment. The same argument applies to show that CLTL ♦ is strictly more expressive than its fragment without atomic formulae of the form x = ♦y. Observe also that CLTL ♦ is neither a fragment of the pure-future safety fragment in [START_REF] Lazić | Safely freezing LTL[END_REF] (where occurrences of U formulae are never in the scope of an even number of negations) nor a fragment of the flat fragment of CLTL ↓ . Unlike these fragments, CLTL ♦ contains past-time operators and negation can be used without any restriction. Infinitary satisfiability for safety LTL

↓ 1 (∼, X, U) is ex- pspace-complete [Laz06], for full LTL ↓ 1 (∼, X, U) is Π 0 1 -complete and, finitary
and infinitary satisfiability for flat CLTL ↓ are pspace-complete. By contrast, in this paper we show that finitary and infinitary satisfiability for CLTL ♦ (with full past-time temporal operators) are decidable problems. By taking advantage of [START_REF] Demri | On the freeze quantifier in constraint LTL: decidability and complexity[END_REF][START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF], it is already possible to establish decidability of finitary satisfiability for strict fragments of CLTL ♦ .

Theorem 1. (I) Finitary satisfiability for CLTL ♦ (X, U) is decidable.

(II) Finitary satisfiability for CLTL ♦ (X, X -1 , F, F -1 ) is decidable.

In the paper we shall show much stronger results: finitary and infinitary satisfiability for full CLTL ♦ even augmented with MSOL definable temporal operators are decidable. In the rest of the paper, we systematically treat the finitary and infinitary cases simultaneously. However, we provide the full technical details for the infinitary case only and we sketch the main ideas for the finitary case. This latter case cannot be reduced in the obvious way to the infinitary case but its solution is close to the one for the infinitary case.

Automata-based Approach with Symbolic Models

In this section we explain how satisfiability can be solved using symbolic models which are abtractions of concrete CLTL ♦ models. We provide the outline of our automata-based approach, and consider the technical details in Sects. 4 and 5.

Symbolic Models

Let φ be a CLTL ♦ formula with k variables {x 1 , . . . x k } and we write l (the "Xlength" of φ) to denote the maximal i such that a term of the form X i x occurs in φ. In order to define the set of atomic formulae that are helpful to determine the satisfiability status of φ, we introduce the set of constraints Ω l k that contains constraints of the form either X i x = X j y or X i (x = ♦y) and their negation with x, y ∈ {x 1 , . . . x k } and i, j ∈ {0, . . . , l}. Models are abstracted as sequences of frames that are defined as maximally consistent subsets of Ω l k . An l-frame is a set fr ⊆ Ω l k that is maximally consistent in that it satisfies the conditions below:

(F1) For every constraint ϕ ∈ Ω l k , either ϕ or ¬ϕ belongs to fr but not both. (F2) For all i ∈ {0, . . . , l} and x ∈ {x 1 , . . . x k }, X i x = X i x ∈ fr . (F3) For all i, j ∈ {0, . . . , l} and x, y ∈ {x 1 , . . . x k }, X i x = X j y ∈ fr iff X j y = X i x ∈ fr . (F4) For all i, j, j ∈ {0, . . . , l} and x, y, z ∈ {x 1 , . . . , x k }, {X i x = X j y, X j y = X j z} ⊆ fr implies X i x = X j z ∈ fr . (F5) For all i, j ∈ {0, . . . , l} and x, y ∈ {x 1 , . . . x k } such that X i x = X j y ∈ fr :

-if i = j, then for every z ∈ {x 1 , . . . , x k } we have

X i (x = ♦z) ∈ fr iff X j (y = ♦z) ∈ fr ; -if i < j then X i (x = ♦y) ∈ fr , and for z ∈ {x 1 , . . . , x k }, X i (x = ♦z) ∈ fr iff either X j (y = ♦z) ∈ fr or there exists i < j ≤ j such that X i x = X j z ∈ fr .
Conditions (F2)-(F4) simply encode that equality is an equivalence relation.

For an l-frame fr , x ∈ {x 1 , . . . , x k } and i ∈ {0, . . . , l}, we define -the set of future obligations for x at level i in fr as ♦ fr (x, i)

def = {y | X i (x = ♦y) ∈ fr }, -the equivalence class of x at level-i in fr as [(x, i)] fr def = {y | X i x = X i y ∈ fr }.
An l-frame fr can be represented as an annotated undirected graph G fr which has vertices (x, i) for x ∈ {x 1 , . . . , x k } and i ∈ {0, . . . , l}, and an edge between (x, i) and (y, j) iff the constraint X i x = X j y belongs to fr . A vertex (x, i) in the graph is annoted with an "open" arc labelled by the set of future obligations ♦ fr (x, i) for that vertex. Fig. 1 shows an example of a 3-frame over the variables {x, y, z}. For convenience we avoid showing transitively inferable edges. We denote by Frame l k the set of such frames built w.r.t. k and l. We say that a model σ satisfies a frame fr at position i (denoted σ, i |= fr ) iff σ, i |= ϕ for every constraint ϕ in fr .

Since a frame can be viewed as a set of constraints about l + 1 consecutive positions, for finitary satisfiability we need to add an information about the possibility to end the model before the end of the current window of length l + 1. This can be done with O(l) bits and then the conditions (F1)-(F5) need to be updated accordingly in order to take into account this possibility. Note that this method allows to handle the particular case where there exists a model whose size is smaller than the X-length of the formula.

Lemma 1. For all models σ with k variables and 0 ≤ i ≤ |σ| -1, there exists a unique frame fr ∈ Frame l k such that σ, i |= fr .

A pair of l-frames fr , fr is said to be one-step consistent

def ⇔ -for all 0 < i, j ≤ l, X i x = X j y ∈ fr iff X i-1 x = X j-1 y ∈ fr , -for all 0 < i ≤ l, X i (x = ♦y) ∈ fr iff X i-1 (x = ♦y) ∈ fr .
A symbolic model of X-length l is a (finite or infinite) sequence of l-frames ρ such that for 0 ≤ i < |ρ| -1, ρ(i), ρ(i + 1) is one-step consistent. We define the symbolic satisfaction relation ρ, i |= symb φ, for a formula φ of X-length l and a symbolic model ρ of X-length l, as done for CLTL ♦ except that for atomic formulas ϕ we have:

ρ, i |= symb ϕ def ⇔ ϕ ∈ ρ(i).
We say a model σ realizes a symbolic model ρ (or equivalently that ρ admits a model σ)

def ⇔ for every 0 ≤ i ≤ |σ| -1, we have σ, i |= ρ(i).
A symbolic model ρ of X-length l can also be represented as an annotated graph G ρ in a similar manner to l-frames. Thus the vertices of G ρ are of the form (x, i) with an edge between (x, i) and (y, j) with 0 ≤ ji ≤ l iff there was an edge between (x, 0) and (y, ji) in the frame graph G ρ(i) . The annotations for future obligations are added similarly. Fig. 1 shows the graph representation of a symbolic model ρ of X-length 3, and a model it admits. By a path p in G ρ we will mean as usual a (finite or infinite) sequence of vertices v 0 , v 1 . . . in G ρ such that each v i , v i+1 is connected by an edge in G ρ . We call p a forward path if each v i+1 is at a level strictly greater than v i .

Automata for Symbolic Models

In order to check whether a CLTL ♦ formula is satisfiable we use Lemma 2 below based on the approach developed in [START_REF] Demri | An automata-theoretic approach to constraint LTL[END_REF].

Lemma 2. A CLTL ♦ formula φ of X-length l is satisfiable iff there exists a symbolic model ρ of X-length l such that ρ |= symb φ and ρ admits a model.

In order to take advantage of Lemma 2, we use the automaton-based approach from [START_REF] Vardi | Reasoning about infinite computations[END_REF]. We build an automaton A φ as the intersection of two automata A symb and A sat such that the language recognized by A symb is the set of symbolic models satisfying φ and the language recognized by A sat is the set of symbolic models that are realized by some models.

We define the automaton A symb by adapting the construction from [VW94] for LTL. We define cl (φ) the closure of φ as usual, and an atom of φ is a maximally consistent subset of cl (φ). For the infinitary case, A symb is the generalized Büchi automaton (Q, Q 0 , →, F ) such that:

-Q is the set of atoms of φ and Q 0 = {At ∈ Q | φ ∈ At, X -1 ∈ At},
-At fr -→ At iff (atomic constraints) for every atomic formula ϕ in At, ϕ ∈ fr , (one step) for every Xψ ∈ cl (φ), Xψ ∈ At iff ψ ∈ At , and for every

X -1 ψ ∈ cl (φ), ψ ∈ At iff X -1 ψ ∈ At -let {ψ 1 Uφ 1 , .
. . , ψ r Uφ r } be the set of until formulae in cl (φ). We pose F = {F 1 , . . . , F r } where for every i ∈ {1, . . . , r},

F i = {At ∈ Q : ψ i Uφ i ∈ At or φ i ∈ At}.
For the finitary case, the finite-state automaton A symb accepting finite words is defined as above except that F is a set of states At such that no atomic formula of the form x = ♦y occurs in At and no formula of the form either Xφ or x = X i y with i > 0 occurs in At. Moreover, such final states can only be reached when the frame labelling the last transition contains proper information about the end of the model.

In the next section, we explain how one can build the automaton A sat that recognizes the set of satisfiable symbolic models. Since A φ is the automaton recognizing the intersection of the languages accepted by A symb and A sat , the following result is a direct consequence of Lemma 2.

Theorem 2. A CLTL ♦ formula φ is satisfiable iff the language recognized by A φ is nonempty.

Note that we separate the temporal logic part and the constraint part by defining two different automata. This allows to extend the decidability results to any extension of LTL that induces an ω-regular class of models. We only need to change the definition of A symb .

Characterization of Satisfiable Symbolic Models

In order to determine whether a symbolic model ρ is "satisfiable" (i.e. it admits a model), we introduce counters that remember the satisfaction of constraints x = ♦y. If x = ♦y 1 ∧ • • • ∧ x = ♦y n needs to be satisfied at the current position, then we shall increment a counter indexed by {y 1 , . . . , y n } that remembers this set of obligations. In a finite model, all the obligations need to be fulfilled before the last position whereas in an infinite model either no more unsatisfied obligations arise after a point, or they are essentially fulfilled infinitely often. The exact conditions will be spelt out soon.

Counting Sequence

For each X ∈ P + ({x 1 , . . . , x k }) (set of non-empty subsets of {x 1 , . . . , x k }), we introduce a counter that keeps track of the number of obligations that need to be satisfied by X. We identify the counters with elements of P + ({x 1 , . . . , x k }). A counter valuation c is a map c : P + ({x 1 , . . . , x k }) → N. For instance, we write c({x, y}) to denote the value of the counter {x, y}, which will stand for the number of obligations to repeat a distinct value in x and y.

We will define a canonical sequence of counter valuations along a symbolic model. We introduce some definitions first. For an l-frame fr and X ∈ P + ({x 1 , . . . , x k }), we define a point of increment for X in fr to be an equivalence class of the form [(x, 0)] fr such that ♦ fr (x, 0) = X and (x, 0) is not connected by a forward edge to a node in fr (i.e. there is no edge between (x, 0) and (y, j) for any j ∈ {1, . . . l}). A point of decrement for X in fr is defined to be an equivalence class of the form [(x, l)] fr such that ♦ fr (x, l) ∪ [(x, l)] fr = X, and (x, l) is not connected by a backward edge to another node in fr (i.e. there is no edge between (x, l) and (y, j) for any j ∈ {0, . . . l -1}). Let u + fr denote a counter valuation which records the number of points of increment for each counter X, in fr . Similarly let u - fr denote the counter valuation which records the number of points of decrement for each counter X in fr . Now let ρ be a symbolic model of X-length l. We carry over the notations for the set of future obligations and the equivalence class for x at level i to symbolic models as well. Thus ♦ ρ (x, i) is equal to ♦ ρ(i) (x, 0) and [(x, i)] ρ is [(x, 0)] ρ(i) . For X ∈ P + ({x 1 , . . . , x k }), a point of increment for X in ρ is an equivalence class of the form [(x, i)] ρ such that [(x, 0)] ρ(i) is a point of increment for X in the frame ρ(i). Similarly, a point of decrement for X in ρ is an equivalence class of the form [(x, i)] ρ such that i ≥ l + 1 and [(x, l)] is a point of decrement for X in the frame ρ(il).

We can now define a canonical counter valuation sequence α along ρ, called the counting sequence along ρ, which counts the number of "unsatisfied" points of increments for each counter X. Let + denote the "proper addition" of integers, defined by n + m = max(0, n + m). We define α inductively for each X ∈ P + ({x 1 , . . . , x k }) and 0 ≤ i < |ρ| as: α(0)(X) = 0; and

α(i + 1)(X) = α(i)(X) + (u + ρ(i) (X) -u - ρ(i+1) (X)).

Sequences for Satisfiable Symbolic Models

We characterize satisfiable symbolic models using their counting sequences.

Lemma 3. A finite symbolic model ρ is satisfiable (i.e. admits a model) iff the final value of the counting sequence α along ρ has value 0 for each counter X (i.e. α(|ρ| -1)(X) = 0) and in the last frame f r of ρ, there are no "unsatisfied"obligations -i.e. no node (x, i) in G f r and variable y ∈ ♦ f r (x, i), with no edge between (x, i) and (y, j) for j > i.

An infinite symbolic model ρ is satisfiable iff the following conditions are satisfied:

(C1) There does not exist an infinite forward path p in ρ and a counter X, such that every node in the path has future obligation X, and there is a variable y in X which is never connected by a forward edge from a node in p (i.e. no node in p is connected by a forward edge to a node of the form (y, i)). (C2) In the counting sequence along ρ, each counter X satisfies one of the condtions: (a) there is a point after which the value of counter X is always zero and after which we never see a point of increment for X, (b) infinitely often we see a point of decrement for X of the form [(x, i)] with ♦ ρ (x, i) ⊂ X, or, (c) for each x ∈ X, we infinitely often see a point of decrement for X, which is connected by a forward path to an x node (i.e a node of the form (x, i)).

In Sect. 5 we show that we can check these conditions on counting sequences using counter automata with a decidable nonemptiness problem.

We introduce a class of counter automata with a disjunctive variant of generalized Büchi acceptance condition in which, along any run, a zero test is performed at most once for each counter.

Simple Counter Automata

A simple counter automaton A is a tuple Σ, C, Q, F, I, → such that -Σ is a finite alphabet, C is a finite set of counters, -Q is a finite set of locations, I ⊆ Q is the set of initial locations, -F = {F 0 , F 1 , . . . , F K } for some K ≥ 0 where F i ⊆ P(Q) for each i = 1 . . . K, -→ is a finite subset of Q × P(C) × Z C × Σ × Q.
Elements of → are also denoted by q Y,up,a ---→ q where Y is interpreted as zero tests on all counters in Y . A configuration q, c is an element of Q × N C and, q, c → q , c iff there is a transition q Y,up,a ---→ q in A s.t. for c ∈ Y , c(c) = 0 and for c ∈ C, c (c) = c(c) + up(c). As usual, a run is a sequence of configurations ruled by the transitions of A. An infinite run is accepting iff there exists a set F ∈ F such that every set Y ∈ F is visited infinitely often. Elements of Σ ω labeling accepting runs define the language accepted by A. In order to accept finite words, we suppose that F defines a single set of final states and a finite run is accepting iff it ends at a final state with all the counters equal to zero.

However, we require additional conditions on the control graph of A to be declared as simple. We require that there is a partition {Q 0 , . . . , Q K } of Q and corresponding sets of counters C 0 , C 1 , . . . , C K with C 0 = ∅ such that I ⊆ Q 0 and for i ∈ {1, . . . , K}, a transition from a location in Q 0 to a location in Q i can be fired only if the counters of C i are equal to zero and all the transitions from a location in Q i go to another location of Q i . Moreover every transition from a location of Q i does not modify the value of the counters in C i . As a consequence, when we enter in the component made of the locations of Q i the counters in C i are equal to zero forever. Finally, for i ∈ {0, . . . , K}, F i ⊆ P(Q i ). Let us summarize the conditions:

1. Q = Q 0 • • • Q K and I ⊆ Q 0 , 2. F = {F 0 , F 1 , . . . , F K } where each F i ⊆ P(Q i ), 3. there exist K + 1 sets of counters C 0 , . . . , C K ⊆ C with C 0 = ∅ such that the transition relation →⊆ Q × P(C) × Z C × Σ × Q verifies the
conditions below: for all i, i ∈ {0, . . . , K}, q ∈ Q i and q ∈ Q i , the transitions from q to q are of the form q Y,up,a ---→ q where (a

) i = i implies i = 0 and Y = C i , (b) i = i implies Y = ∅, (c) for c ∈ C i , up(c) = 0.
In the sequel we consider simple counter automata with C = P + ({x 1 , . . . , x k }), K = 2 k -1 and each set F i contains sets of states reached by decrementing the counters in C i . Lemma 4 below states that simplicity implies decidability of the nonemptiness problem thanks to [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF].

Lemma 4. The nonemptiness problem for simple counter automata is decidable.

Automata recognizing satisfiable counting sequences

Now, we can build a simple counter automaton A l k recognizing the set of satisfiable symbolic models of X-length l. We describe the construction for the infinite case and the automaton that recognizes finite satisfiable symbolic models can be defined similarly.

The simple counter automaton A l k is defined to be the intersection of the automata A 1 and A 2 which check conditions (C1) and (C2) respectively. Automaton A 1 is a Büchi automaton and is easy to define. We focus on defining the counter automaton A 2 . We define

A 2 = Σ, C, Q, F, s, → , where Σ = Frame l k , C = P + ({x 1 , . . . , x k }), Q = {s} ∪ Frame l k ∪ Z⊆C Q A Z ,
where Q A Z is the set of states of the automaton A Z which we define below, → is given by

-s ∅,up 0 ,fr ----→ fr -fr ∅,up,fr ----→ fr -fr Z,up,fr ----→ s A Z
where up 0 is the zero update (i.e. up 0 (X) = 0 for each X ∈ C), u + fr (X) ≤ up(X) ≤ u + fr (X)u - fr (X) for each X ∈ C, and s A Z is the start state of automaton A Z . Moreover, we require in the last rule that for every counter X ∈ Z (i.e. every counter that is tested to zero) we have up(X) = 0.

The Büchi automaton A Z is given by:

A Z = A 2a Z ∩ X∈C\Z (A 2b X ∪ A 2c X ) A 2c X = x∈X A X,x
where the automaton A 2a Z accepts symbolic models in which there are no points of increment for any X in Z; the automaton A 2b X checks that infinitely often there is a point of decrement for X of the form [(x, i)] such that the set of future obligations of (x, i) is a strict subset of X; and the automaton A X,x checks condition C2(c) for X and a variable x ∈ X. The automaton A X,x is the complement of the Büchi automaton B X,x which accepts symbolic models in which there is a point after which we never see an x-node reachable by a forward path from a point of decrement for X. The automaton B X,x has states of the form (fr , S) where fr is a frame and S is a subset of nodes in fr . We have a transition from (fr , S) to (fr , S ) iff S is the set of nodes in fr which are either a point of decrement for X in fr or are connected by a forward edge to a node in S in fr . The automaton non-deterministically moves to a second copy where it allows the above transitions only if S does not contain a node of the form (x, i). All states in the second copy are final.

We can easily check that all the properties of simple counter automata are verified by this construction. For the finite case, A l k is similar to A 2 above, except that a word is accepted when the run ends with all the counters equal to zero.

Lemma 5. Let ρ be a symbolic model of X-length l. Then ρ is accepted by A l k iff ρ is satisfiable.

We are now in position to state the main result of the paper.

Theorem 3. Finitary and infinitary satisfiability for CLTL ♦ is decidable.

Proof. Let φ be a CLTL ♦ formula over k variables with X-length l. Let A φ be the simple counter automaton built as the intersection of A symb , A l k and A lc that accepts sequences in which consecutive frames are one-step consistent. We can check whether the language accepted by A φ is non-empty (Lemma 4). Thus, by Theorem 2, checking the satisfiability of φ is decidable.

According to the acceptance condition of A l k in the finite case, finitary satisfiability reduces to the reachability problem in Petri nets.

Theorems 2 and 3 entail that this decidability result can be extended to any extension of LTL as soon as the temporal operators as definable in MSOL, see for instance [START_REF] Gastin | Satisfiability and model checking for MSO-definable temporal logics are in PSPACE[END_REF].

Corollary 1. Finitary and infinitary satisfiability for CLTL ♦ augmented with MSOL definable temporal operators is decidable.

A PSPACE fragment of CLTL ♦

In this section, we consider the fragment CLTL ♦ 1 with a unique variable x. The models are sequences of natural numbers and the only counter in counting sequences α is {x} (we identify α(i)({x}) with α(i)). Given a symbolic model ρ over the alphabet Frame l 1 and the counting sequence α along ρ, for every 0

≤ i < |ρ|, α(i + 1) = α(i) + u + i -u - i+1 with u + i , u - i+1 ∈ {0, 1}
. By Lemma 3, when ρ is satisfiable, in the counting sequence along ρ either the unique counter remains equal to zero after a finite number of steps or it is decremented infinitely often. Moreover, the value of the unique counter in the counting sequence is nicely bounded unlike in general with strictly more than one variable. Lemma 6. Let ρ be a symbolic model and α be the counting sequence along ρ. For 0 ≤ i < |ρ|, α(i) ≤ l.

Boundedness entails the possibility to use automata without counters. Lemma 7. The set of satisfiable symbolic models over the alphabet Frame l 1 can be recognized by a standard Büchi automaton A l 1 for the infinite case, or by a finite-state automaton for the finite case.

The automaton A l

1 has an exponential size and can be built in polynomial space in l. Checking nonemptiness for this automaton can be done in non deterministic logarithmic space which allows to establish Theorem 4 below. Theorem 4. Finitary and infinitary satisfiability for CLTL ♦ 1 is pspace-complete.

The models for CLTL ♦ 1 corresponds to models of LTL ↓ (∼, X, U). Therefore, finitary and infinitary satisfiability for LTL ↓ 1 (∼, X, X -1 , U, S) restricted to formulae such that the freeze operator is restricted to subformulae of the form ↓ r=x XF(r = x) and ↓ r=x X i (r = x) is decidable in polynomial space (r is the unique register and x the unique variable).

Repeating values in the past is still decidable

In this section we explain why we can allow the constraints of the language to state properties about past repetitions of a value without loosing decidability. Let CLTL ♦,♦ -1 be the extension of CLTL ♦ with atomic formulae of the form x = ♦ -1 y. The satisfaction relation is extended as follows: σ, i |= x = ♦ -1 y iff there is j > 0 s.t. x = σ(ij)(y) and 0 ≤ ij. Similarly to what is done in Section 2.1, x diff ♦ -1 y can be omitted since it can be defined from x = ♦ -1 y (a variant of the equivalence (1)).

In order to deal with satisfiability for CLTL ♦,♦ -1 we need to extend the symbolic representation of models. In addition of the conditions(F1)-(F5) defined in Sect. 3.1, a frame fr has to verify the following property (the finitary case admits a similar update): (F6) for all i, j ∈ {0, . . . , l} and x, y ∈ {x 1 , . . . x k }, if X i x = X j y is in fr then -if i = j, then for every z ∈ {x 1 , . . . , x k } we have X i (x = ♦ -1 z) ∈ fr iff X j (y = ♦ -1 z) ∈ fr (we extend the notion of frames); -if i > j then X i (x = ♦ -1 y) ∈ fr , and for every z ∈ {x 1 , . .

. , x k }, X i (x = ♦ -1 z) ∈ fr iff either X j (y = ♦ -1 z) ∈ fr or there exists i > j ≥ j such that X i x = X j z is in fr . We pose ♦ - fr (X i x) def = {y | X i (x = ♦ -y) ∈ fr }.
Since we need to deal with past obligations, a counter is a pair X p , X f in P + ({x 1 , . . . , x k }) × P + ({x 1 , . . . , x k }) where X p is for past obligations and X f for future obligations. We update the notion of counter valuations accordingly. A value n for X p , X f is the number of values that occurred in a past state of every variable of X p and that have to be repeated in a future state of every variable in X f . We extend some earlier definitions. For an l-frame fr and counter X p , X f , we define a point of increment for X p , X f in fr to be an equivalence class of the form [(x, 0)] fr such that ♦ fr (x, 0) = X f , (x, 0) is not connected by a forward edge to a node in fr and [(x, 0)] fr ∪ ♦ -1 fr (x, 0) = X p . A point of decrement for X p , X f in fr is defined to be an equivalence class of the form [(x, l)] fr such that ♦ fr (x, l) ∪ [(x, l)] fr = X f , (x, l) is not connected by a backward edge to another node in fr and ♦ -1 (x, l) = X p . Let u + fr denote a counter valuation which records the number of points of increment for each counter X p , X f , in fr . Similarly let u - fr denote the counter valuation which records the number of points of decrement for each counter X p , X f in fr . We can now define a canonical counter valuation sequence α along ρ, called the counting sequence along ρ, which counts the number of "unsatisfied" points of increments for each counter X p , X f with X p = ∅. We define α inductively: α(0)( X p , X f ) = 0 and for 0 ≤ i < |ρ|, α(i+1)( X p , X f ) = α(i)( X p , X f )+(u + ρ(i) ( X p , X f )-u - ρ(i+1) ( X p , X f )). Note that decrementations are this time compulsory and we allow α(i)( X p , X f ) to be negative (but not in the acceptance condition). Though we need more counters, dealing with past repeating values, does not introduce real complications. This is analogous to the passage from LTL to LTL with past-time operators since past is finite and information about past can be accumulated smoothly.

Lemma 8. A symbolic model ρ for the logic CLTL ♦,♦ -1 is satisfiable iff the counting sequence along ρ satisfies the conditions from Lemma 3 for the future part of the counters and for 0 ≤ i < |ρ|, α(i)( X p , X f ) ≥ 0.

The proof is similar to the proof of Lemma 3. We just need more registers to store the different values that have to be repeated.

As a consequence, we can easily update the construction of A φ in order to deal with past repeating values. The definition of the automata A symb and A l k are just extended by considering the new definition for frames. It is also important to observe that the automaton A φ obtained by synchronization of these automata still belongs to the class of simple counter automata and the decidability result also holds for CLTL ♦,♦ -1 satisfiability problem.

Theorem 5. Finitary and infinitary satisfiability for CLTL ♦,♦ -1 [resp. CLTL ♦,♦ -1 1 ] is decidable [resp. pspace-complete].

Concluding Remarks

We have shown that satisfiability for CLTL ♦ with operators in {X, X -1 , S, U} is decidable by reduction into the verification of fairness properties in Petri nets [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF]. The proof is uniform for the finitary and infinitary cases and it can be extended to atomic constraints of the form x = ♦ -1 y and to any set of MSOL definable temporal operators. Moreover, satisfiability for CLTL ♦ restricted to one variable is shown pspace-complete. Hence, we have defined and studied a well-designed decidable fragment of LTL with the freeze quantifier answering some question from [START_REF] Wolter | Spatio-temporal representation and reasoning based on RCC-8[END_REF] and circumventing some undecidability results from [START_REF] Demri | LTL with the freeze quantifier and register automata[END_REF]. Finally, as done also in [DL06,Laz06,BMS + 06], we show relationships between fragments of LTL with freeze and counter automata.

The main question left open by our work is the complexity of satisfiability for CLTL ♦ and more precisely we do not know whether CLTL ♦ satisfiability has elementary complexity. Similarly, are there natural fragments of CLTL ♦ that are of lower complexity, for instance the one involved in Theorem 1? Another promising extension consists in considering other concrete domains as R, <, = and to allow atomic formulae of the form x < ♦y. The decidability status of such a variant is still open.

Fig. 1 .

 1 Fig. 1. Example 3-frame graph, concrete model σ, and its induced 3-frame graph G ρ .

Acknowledgements: We are grateful to Petr Jančar (TU Ostrava) for pointing us to [Jan90] in order to solve the nonemptiness problem for simple counter automata and for suggesting the proof of Lemma 4 and Ranko Lazić (U. of Warwick) for remarks about a preliminary version.

Work supported by the Indo-French project "Timed-DISCOVERI" (P2R/RNP scheme).


Junji Yuhara1
email: j-yuhara@energy.nagoya-u.ac.jp

Guy Le Lay2

Beyond silicene: synthesis of germanene, stanene and plumbene

Twenty five years after the first theoretical prediction of two-dimensional (2D) honeycomb-like silicon and germanium, now coined silicene and germanene, the last Group 14 artificial cousin of graphene has been synthesized, thus terminating the lineage from silicene (2012) to germanene (2014), stanene (2015), and finally plumbene (2019). Here, we describe the realizations and review the tantalizing properties of these outstanding novel 2D materials.

Introduction

The recent realization of epitaxial plumbene 1) has ended the quest for the challenging synthesis of all Group 14 cousins of graphene with elemental monolayer honeycomb structure, as originally theoretically predicted. Indeed, ending this quest, does not mean halting research; instead, it will give a new impetus and launch many new studies on fundamental and applied aspects. At variance with graphene, these cousins have no parent crystal like graphite in nature, from which they could be possibly peeled off. Since the first realizations of silicene in 2012, [2][3][4] showing that the initial theoretical predictions 5,6) could be effectively materialized, a gold rush has started to obtain elemental two-dimensional (2D) materials analogs, especially at present from element B in Group 13 to make borophene 7) to element Bi in Group 15 to make bismuthene. 8)

A very recent article has comprehensively spanned all these novel 2D materials (except for plumbene, which had not yet appeared in reality at the moment of submission). 9) Several books (see, e.g. Refs. 10 and 11), book chapters (see, e.g. Refs. 12 and 13), and review articles (see, e.g. Refs. [START_REF] Dávila | 2D Semiconductor Materials and Devices[END_REF][START_REF] Zhang | [END_REF][16] have been published, especially highlighting silicene, graphene's first cousin, whose realization has further engen-dered many offsprings and a huge number of theoretical and experimental studies. In this respect it is worth mentioning that the "growth and properties of silicene" has been ranked 4th topic (among 10 selected) in the Hot Research Fronts in physics, as determined following a Thomson-Reuters cita-tion-based study covering years 2011-2014. 17) The next 10 Hot Research Fronts, issued in 2019, identifying the hottest and emerging specialty areas in scientific research in physics from 2013 to 2018, have placed "2D Group-VA materials: antimonene, arsenene and bismuthene" also at the 4th rank, a clear marker of the direct parentage. 18) Hence, we will rather focus, here, on our post-silicene achievements, obtained in recent years at Nagoya University in Japan, where specific growth methods have yielded a new arrangement of epitaxial germanene by segregation, 19) as well as large-area planar stanene 20) and plumbene, 1) which developed above surface alloys initially formed. Germanene, stanene and plumbene, are especially exciting because they inherently possess large spin-orbit couplings (SOCs), which can make them robust topological insulators and may favor a Quantum Spin Hall effect near, or at RT and even above, which is highly promising for future devices and quantum information applications.

Germanene

Already in 1994, 10 years before the advent of graphene, two pioneers, K. Takeda and K. Shiraishi, predicted from density functional theory (DFT) calculations the "Theoretical possibility of stage corrugation in Si and Ge analogs of graphite". 5) In other words, they demonstrated the possible existence of standalone atom-thin sheets of silicon and germanium, now coined silicene and germanene. Their article remained essen-tially unnoticed until 2009, when S. Cahangirov et al. resurrected it and confirmed the findings, further demon-strating the dynamical stability and underlining the appearance of Dirac fermions at the K and K' points of the surface Brillouin zone (SBZ). 6) However, it was only after 2012, when silicene had been truly synthesized under ultra-high vacuum (UHV) conditions, either by Si deposition onto (111) surfaces of silver single crystals, 2,4) the reversed process of growing silver on Si(111) to form the prototypical Si(111)(√3 × √3)-Ag surface reconstruction, [START_REF] Matsuda | [END_REF] or by segregation of silicon through a zirconium diboride thin film grown on a piece of silicon wafer, 3) that their citations started to rise quickly. Two years later, germanene was synthesized in Marseille (France) by Ge deposition onto a gold (111) surface, 21) again the reverse fashion of forming the Ge(111)(√3 × √3)-Au surface reconstruction. 22) This birth initiated the lineage down column 14 of novel elemental artificial 2D materials beyond graphene, from silicene to plumbene, as shown in Fig. 1. Compelling evidence of the synthesis of germanene was obtained, especially for a nearly flat phase forming large domains in scanning tunneling microscopy (STM) imaging. Advanced DFT calculations confirmed its atomic geometry, i.e. a (√3 × √3) germanene superstructure matching a (√7 × √7)R19.1° Au(111) supercell. However, other 2D phases were simultaneously co-existing, making the situation somewhat complex. Instead, a highly desirable single phase of germanene, technically very important for the easy synthesis and transfer of this promising 2D electronic material, was recently prepared by a segregation procedure through a thin Ag (111) film epitaxially grown on a Ge(111) piece of wafer. This method, described in Fig. 2, is different from the molecular beam epitaxy (MBE) one used previously, but bears resemblance with the preparation of silicene by segregation through a ZrB 2 thin film, as mentioned above. From the STM images, which clearly reveal an internal honeycomb arrangement with low buckling within 0.01 nm, the surface is completely covered with a self-limiting atom-thin layer showing a highly ordered long-range superstructure in wide scale. Two types of protrusions, named hexagon and line, form a (7√7 × 7√7)R19.1° supercell with respect to Ag(111), with a very large periodicity of 5.35 nm, which corresponds to a (3√21 × 3√21)R10.9° germanene superstructure. Interestingly, this shows that the two preparation methods, either by deposition or by segregation are asymmetric, leading to different final situations. Figure 3 displays the sharp low energy electron diffraction (LEED) pattern obtained after segregation with incommensurate "(1.35 × 1.35)"R30° spots, corresponding to a lattice constant of 0.39nm, in good agreement with the theoretical lattice constant of freestanding germanene; it also shows a typical STM image and the derived atomic model.

As aluminum has essentially the same lattice parameter as gold and silver, germanene has been also prepared in 2015 by deposition onto Al(111) single crystal surfaces, where it appeared as a (3 × 3) reconstruction in LEED patterns. 23) However, other phases are also simultaneously formed. 24) A well-defined Dirac cone remained elusive but a clear metallic behavior was observed in initial scanning tunneling spectro-scopy measurements, which evolved in a diversity of spectra explained by the erratic modifications of the tip apex occurring during the scans. 25) By deposition of Ge onto Ag(111) surfaces kept at 150°C two distinct phases associated with low-buckled germanene have been observed by STM, LEED and angle-resolved photoemission spectroscopy (ARPES); ab initio calculations helped in their understanding. 26) At lower coverage a first phase exhibits an atom-resolved tensile strained honeycomb lattice, partially commensurate with the substrate to form a striped phase (SP). At higher coverage, a second one consistent with a honeycomb lattice with a lattice constant incommensurate with the substrate but very close to the theoretical value for freestanding germanene, is a quasi-freestanding phase (QP). The SP can be driven into the QP by additional Ge deposition. Band mapping along with first-principles calculations with proposed atomic models for both phases reveal that the SP is subjected to significant band renormalization and develops an interface state due to its partial commensuration with the substrate. Instead, only the QP possesses the characteristic σ band of freestanding germanene because the incommensurate structure leads to a weaker and smoothed interfacial interaction. These results indicate that Ag(111) provides a relatively gentle support for the formation and transformation of the dual germanene phases, similarly to the formation of silicene phases on the same support. They further illustrate how the competitive formation of Ge-Ge covalent and Ge-Ag interfacial bonds and adlayersubstrate commensurability play a key role in the electronic structure of the dual germanene phases.

Still upon deposition onto Ag( 111), but at a slightly higher temperature of 177 °C, Du and coll., 27) fabricated thick germanium nanosheets, starting from an initial Ag 2 Ge surface alloy. 28) Strikingly, these silver films supported semiconducting nanosheets were terminated by a germanene monolayer dis-playing a (√3 × √3) superstructure. A linear-like energy-momentum dispersion, and a large Fermi velocity were derived from pronounced quasiparticle interference patterns, pointing to Dirac fermion characteristics. Furthermore, theoretical simula-tions revealed the opening of a sizeable band gap corresponding to RT, at the center Γ of the SBZ because of the (√3 × √3) reconstruction. Clearly, the high charge carrier mobility, the sizable band gap, and the semiconducting character of the Ge (111) nanosheets with tunable thickness acting as a dielectric layer, may favour nanotechnology applications of this out-standing material. With the introduction of a thin h-AlN buffer layer the growth of 2D germanene sheets is preserved at a substrate temperature of 450 °C, which is also promising for future applications. 29) Here, it is worth mentioning that multilayer germanene sheets harboring Dirac fermions have been grown in situ for the first time on Au(111) surfaces. 30)

Concerning potential applications, it is worth mentioning here that besides the results obtained in situ under UHV reviewed in this article, wet chemical preparation methods yield highly promising Ge-based synthetic materials. 9) This is the case of bulk germanane (van der Waals bonded stacks of fully hydrogenated germanene), which can be easily exfo-liated down to a monolayer, leading to a direct band gap opening at the Γ point, 31) as well as functionalized germananes. 32) A fascinating aspect is that ultra-small germanene quantum dots, 33) like silicene nanosheets, 34) promise high clinical potential in nanomedicine.

Stanene

As silicene and germanene, stanene (rarely written as stannene, and sometimes called tinene) shows a quantum spin Hall effect due to the SOC: at the Dirac points fundamental band gaps open up, which can be tuned by applying a perpendicular electric field, inducing a topological phase transition. 35,36) The gap is 73 meV in stanene compared to 23 meV, 1.55 in germanene and silicene, but negligible (only 8 μeV) in graphene. This means that stanene can be a 2D topological insulator above RT, while germanene can be slightly below.

In 2015, Zhu et al. reported the first synthesis of single-layer stanene upon growth by MBE on a metallic Bi 2 Te 3 (111) surface; it presented no signature of a topolo-gical state. 37) Due to compressive strain, it was strongly buckled, the growth fashion of tin on this surface actual following an islands mode.

At variance, a nearly planar stanene structure in large domains was realized by Yuhara et al. on a Ag(111) surface after growth of an initial Ag 2 Sn surface alloy, acting as a template, where the growth fashion is indicated in Fig. 4 (a). 20) To the best of our knowledge, this is the first evidence of a 2D elemental Xene generated in such a way. The crystalline structure was ascertained synergetically by STM, high-resolution synchrotron radiation photoemission valence band and spectroscopies, and advanced first-principles calculations. As displayed in Figs. 4(b) and 4(c), the STM images show that stanene forms a nearly planar structure in large domains. A detailed core-level spectroscopy analysis as well as DFT calculations [see Fig. 4(d)] revealed that the stanene sheet overlays an ordered Ag 2 Sn 2D surface alloy, not directly residing on a bulk-terminated Ag(111) surface. However, the electronic structure measured in ARPES does not reveal a non-trivial behavior; instead, it exhibits a characteristic 2D band with parabolic dispersion due to the non-negligible interaction with the underlying surface alloy. Soon after this first realization of nearly flat stanene, 2D high-quality ultraflat stanene has been fabricated on Cu(111) by low-temperature MBE 38) Due to the epitaxial effect of the substrate, its lattice constant is as high as 0.51 nm and it shows an in-plane s-p band inversion together with a SOC-induced topological gap at the Γ point of ∼0.3eV, far exceeding the RT thermal fluctuation energy. Hence, this ultraflat monolayer stanene displays clear non-trivial features in ARPES experiments, while topologically derived boundary states were observed by STM measurements. As superconductivity in few-layer stanene has been recently discovered, 39) further exploration of 2D superconductivity or even Majorana fermions could be envisaged. Furthermore, first-principles calculations predicted that ultraflat plumbene could also be fabricated on Cu(111), with also an s-p band inversion together with a SOC-induced gap at the Γ point. 38) All these striking findings open tantalizing prospects for further exploring 2D topological physics and device applications.

Stanene was also grown on other substrates, with promises of many exciting properties. We refer to Ref. However, with the smart choice of a palladium single crystal substrate, Yuhara and co-workers at Nagoya University in Japan could provide compelling evidence of the epitaxial growth of large-area plumbene sheets. The synthesis has been achieved on the (111) surface of a Pd (1-x) Pb x dilute alloy thin film, using a segregation method from the Pd(111) substrate, as depicted in Fig. 5(a). This dilute alloy thin film exhibits in STM imaging a unique surface morphology resembling the famous Weaire-Phelan bubble structure of the Olympic "WaterCube" in Beijing. 41) The "soap bubbles" of this "Nano Water Cube" are adjustable with their average sizes (in-between 15 and 80 nm) related to the Pb concentration (x < 0.2) dependence of the lattice parameter of the Pd (1-x) Pb x (111) alloy surface. Angle-resolved core-level spectroscopy measurements demonstrate that a lead sheet overlays the Pd (1-x) Pb x (111) alloy. The atomic-scale STM images of this Pb sheet show a planar honeycomb structure with a unit cell in accordance to that of freestanding plumbene.

High band gaps are predicted in decorated plumbene, which could lead to a quantum spin hall insulator behavior and fascinating high-temperature applications. 42) Indeed, synthesizing such sheets while keeping their non-trivial characteristics remains a non-easy challenge.

Summary and outlook

All the Group 14 2D honeycomb materials beyond graphene, the lineage from silicene, first realized in 2012, to plumbene, realized in 2019, have been now synthesized. The virtual possibilities opened by Takeda and Shiraishi in 1994, 10 years before the advent of graphene, have now materialized. This puts an end to a long Holy Grail quest, but opens tantalizing prospects for the practical implementation of non-trivial emergent phenomena in nanoelectronics, and nano-photonics, in spintronics, and, last but not least, in quantum computing with the search for Majorana fermions.

These novel 2D materials share the optimum geometry, which has intrigued mankind for millennia, that is, the honeycomb array structure constructed by bees upon mas-sively parallel working under natural collective intelligence. Noteworthy, is that it is only in 2001 that the socalled classical honeycomb conjecture, namely, the intuition that the best way to partition a surface into regions of equal areas with the smallest total perimeter, 12) has been mathematically solved by Thomas Hales. 42) Strikingly, the realization of plumbene relies also on a template, a thin Pd (1-x) Pb x dilute alloy, 1) reminiscent of the special 3D foam geometry derived in 1994 by Weaire and Phelan, who found a counter-example to the famous Kelvin's conjecture that a b.c.c. arrangement of minimal tetrakaideca-hedron divides space into equal cells of minimum surface area. 41) This conjecture, which had stood for over one hundred years, has thus been ruined, but the mathematical problem remains entirely open.

Here, nanoarchitectonics meets mathematics and real archi-tecture: the Weaire-Phelan construction has inspired the 2008 Olympics "Water Cube" in Beijing, while, conversely, the soccer ball atomic geometry of the C 60 fullerene, has been inferred from the geodesic dome of the 1967 Montreal Expo, designed by famous architect Buckminster Fuller.

Fig. 1 :

 1 Fig.1: The lineage of artificial Group 14 elemental novel 2D materials from silicene to plumbene.

Fig. 2 :

 2 Fig. 2: Preparation of germanene by segregation through a silver (111) thin film.

Fig. 3 :

 3 Fig. 3: Diffraction pattern and real space images of germanene obtained by segregation. (A) LEED pattern recorded at 63eV. (B) STM image recorded in a constant current mode with tunneling current of 200 pA and sample bias voltage of +0.3 V. The unit cell of "(1.35 × 1.35)"R30° is indicated by the small lozenge. (C) Ball model of the germanene sheet on Ag(111), locally keeping a germanene unit cell of (1.35×1.35)R30°. The germanene (3√21×3√21)R10.9° superstructure matches a Ag(111) (7√7 × 7√7)R19.1° supercell, indicated by the lozenge. The areal positions corresponding to the hexagon and line protrusions are marked by a solid yellow line.

Fig. 4 :

 4 Fig. 4: Synthesis of nearly planar stanene on Ag(111). (A) Scheme of the growth fashion. (B) Large scale STM image showing stanene and a partly uncovered zone of the Ag2Sn template. (C) Honeycomb aspect of the stanene layer in STM imaging; inset: ball model of its atomic geometry. (D) Structural models (side and top views) and their simulated STM images of (a) the Ag2Sn surface alloy and (b) stanene on the Ag2Sn surface alloy.

  9, and especially to the most recent review by Lyu et al. for new electronic and spintronic applications. 40) 4. Plumbene Beginning of January 2020, a search in the Web of Science with plumbene in topic yields only 10 results, the first paper having been published only in 2016. Nine papers are based on theoretical calculations; just the most recent one in July 2019 by Yuhara et al. reports the first experimental realiza-tion of plumbene. 1) This reflects the initial skepticism of the 2D material community about the possibility to synthesize the heaviest cousin of graphene with the highest intrinsic SOC.

Fig. 5 :

 5 Fig. 5: First experimental realization of plumbene on a "Nano WaterCube". (A) Scheme of the growth method. (B) Large scale STM image showing the bubblelike aspect of the Pd (1-x) Pb x dilute alloy thin film-coined a "Nano WaterCube"-because of its resemblance with the facade of the swimming pool (nick-name, the "Water Cube") of the 2008 Olympics in Beijing. (C) Honeycomb structure of the plumbene overlayer in STM imaging.

Acknowledgments

The authors are grateful to Nagoya University Synchrotron Radiation Research Center for financial support for CLS measurements, which were conducted at the BL7U of Aichi Synchrotron Radiation Center, Aichi Science & Technology Foundation, Aichi, Japan (No. 2018001). J.Y. acknowledges financial support from the Murata Science Foundation in 2019. G.L.L. acknowledges support from Nagoya University thanks to an "Eminent Foreign Scientist" Invitation Award in 2015/ 2016, and a "Principle Investigator" Award in 2019/2020, as well as an Invitational Fellowship for Research in Japan by the Japan Society for the Promotion of Science (JSPS) in 2017.


Tsuyoshi Ogikubo

Hiroki Shimazu

Yuya Fujii

Koichi Ito

Akio Ohta

Masaaki Araidai

Masashi Kurosawa

Guy Le Lay

Junji Yuhara

Continuous Growth of Germanene and Stanene Lateral Heterostructures

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Group 14 elemental 2D materials with honeycomb struc-ture beyond graphene have attracted considerable interest recently. At variance with graphene, for which the opening of a band gap in its electronic structure is difficult, these novel 2D materials are expected to possess sizeable band gaps, making them typically suitable for elec-tronic applications. Furthermore, theory predicts that they are robust topological insulators, even up to about room tem-perature (RT) and above for germanene and stanene.

In experiment, these artificial 2D materials were firstly realized in situ by molecular beam epitaxy (MBE) for silicene in 2012, [1,2] germanene in 2014, [3] stanene in 2015, [4] and finally plumbene in 2019. [5] One of the next targets is the growth of in-plane heterostructures because abrupt lateral interfaces promise controlled heterojunction functionali-ties. Lateral heterostructures of graphene and hexagonal boron nitride (h-BN) were grown on Cu(110) in 2014. [6] First-princi-ples calculations on the electronic proper-ties of graphene quantum dots embedded in monolayer h-BN sheets typically indi-cate that the h-BN band gap shrinks upon increasing the diameter of the graphene dots. [7] Besides lat-eral graphene/h-BN heterostructures, fabrication of several in-plane heterostructures of transition metal dichalcogenides has also been reported. [8] Very recently, vertical heterostruc-tures have been prepared by boron intercalation underneath graphene, while, more strikingly, lateral integration of boro-phene with graphene has been realized. [9] At variance, there is no experimental report of the realization of such monolayer in-plane heterostructures for the group 14 post-graphene 2D materials, although each of them typically possesses very high hole and electron mobilities. [10] As stressed in Ref. [9], compared to vertical junctions with essentially van der Waals bonding, generally fabricated by mechanical stacking, 2D lat-eral heterostructures with covalent lateral stitching require bottom-up synthesis, which explains why such realizations are rare. However, the covalent in-plane bonding of lateral heterointerfaces for imperfect lattice matching often results in wide interfaces, where disorder and intermixing can reduce the structural and electronic abruptness. As a consequence, finding appropriate 2D materials and identifying synthetic conditions that yield nearly atomically sharp heterostructures is of major interest.

The energy gaps for silicene, germanene, and stanene are not so large, ranging from 0.002 to 0.03, and 0.1 eV, respectively. [11] Yet, 2D pseudomorphic heterostructures, for example, of silicene and germanene ribbons, might be used to control the electronic band structures, because the band gaps are made tunable by adjusting the widths of the respective nanoribbons. [12,13] Nevertheless, the realization of post-graphene lateral heterostructures based on group 14 elements, which is crucial for the future fabrication of heterojunctionembedded 2D devices compatible with conventional Si-based technology, remains a daunting challenge.

Silicene has been initially synthesized in situ on Ag(111), ZrB 2 (0001), and Ir(111) [1,2,14] Next, the growth of germanene by MBE has been reported on Au(111), [3] Pt(111), [15] Al(111), [16] Sb(111), [17] Cu(111), [18] Ag(111), [19] Ge(110), [20] MoS 2 , [21] graphite, [22] and Ge(111). [23] Recently, germanene has been also prepared on Ag(111) thin films by atomic segregation epitaxy (ASE). [24] For the MBE growth of stanene, Bi 2 Te 3 (111), [4] Sb(111), [25] Ag(111), [26] and Cu(111) [27] substrates have been adopted. Up to now, the Ag(111) surface appears as the most promising template for the heterostructure growth of all group 14 post-graphene materials. According to the phase diagram, Ge and Sn are immiscible at any ratio, [28] while Ge and Si can make all proportional solid solutions. [29] Therefore, germanene and stanene appear as a promising combination for realizing a lateral heterostructure on Ag(111).

In this work, we achieved lateral in-plane heterostructures of monolayer germanene and stanene on a silver (111) thin film epitaxially grown on a Ge(111) substrate, as shown in Figure 1. With a synergetic combination of in situ ASE for germanene and MBE for stanene, we found the appropriate kinetic conditions to realize simultaneously their lateral growths. Typically, after initial annealing of the sample at 500 °C, during slow cooling Ge segregates at the top surface of the Ag(111) thin film, which favors 2D germanene islanding at about 200 °C, the temperature where we per-formed the simultaneous deposition of 0.3 monolayers of Sn. By this procedure we obtained remarkably precise ger-manene/stanene heterojunctions without significant replace-ment of Ge atoms in stanene and vice versa. In experiments, the atomic and electronic structures have been determined by low-energy electron diffraction (LEED), scanning tun-neling microscopy (STM), and scanning tunneling spectros-copy (STS).

Figure 1. Illustration of the sequential formation of lateral heterostructures of germanene and stanene, prepared on a Ag(111) thin film grown on a Ge(111) substrate after annealing at 500 °C, followed by slow cooling. A Sn deposition is performed at 200 °C during the Ge segregation and germanene formation processes while cooling, resulting in the growth of lateral heterostructures of germanene and stanene observed at room temperature.

Results and Discussion

Figure 2a displays the LEED pattern for a stanene sheet formed at 200 °C by MBE over a Ag 2 Sn initial surface alloy grown on a Ag(111) single crystal, in conditions sim-ilar to those used in our previous work on the synthesis of stanene. [26] It shows the primitive spots of epitaxial stanene with a unit cell 0.50 nm in size (see Figure 2e), corresponding to a Ag(111)(√3 × √3)R30° super periodicity. The corresponding STM image, revealing the honeycomb atomic arrangement of epitaxial monolayer stanene having a 0.50 nm unit cell, in perfect match with the underlying Ag 2 Sn surface alloy with (√3 × √3)R30° superstructure with respect to Ag(111), is displayed in Figure 2b. Figure 2c shows the LEED pattern for a complete germanene sheet formed also at 200 °C on top of a Ag(111) thin film previously grown on Ge(111) upon segregation of germanium during slow cooling, after initial heating of the specimen at 500 °C. The primitive spots originating from the honeycomb lattice of germanene, which correspond to Ag(111)"1.35 × 1.35"R30° with 0.39 nm size (see Figure 2e), are clearly observed. Additional spots originate from the prominent characteristic 2D (3√21 × 3√21) R10.9° germanene superstructure observed in STM imaging (shown in Figure 2d), matching a Ag(111)(7√7 × 7√7)R19° superstructure. Here, we emphasize that these LEED pat-terns and STM images are in perfect accordance with those obtained in previous papers. [24,26] For direct comparison, Figure 2f shows the LEED pattern for the heterostructure built up on a Ag(111) thin film grown on a Ge(111) substrate, following the recipe described above. No other spots, besides those in Figure 2a,c are seen, which indi-cates that no ordered new structure composed of intermixed Sn and Ge atoms is formed. Furthermore, within the resolu-tion limits, the positions of the LEED spots are identical to a superposition of those stemming from the sole germanene and stanene overlayers, shown in Figure 2a,c. It indicates that pure germanene and stanene domains are obtained by our methodology, which may possibly point to the realization of lateral heterojunctions.

Actually, this is effectively confirmed in STM micro-scopy observations. Figure 3a shows the STM image corre-sponding to the LEED pattern shown in Figure 2f. On the (111) terraces of the silver thin film, the characteristic 2D (3√21 × 3√21)R10.9° germanene superstructure, matching a Ag(111)(7√7 × 7√7)R19° superperiodicity, [24] is easily recog-nized upon comparison with Figure 2d. It surrounds, two rounded 2D islands, with diameters of several tens nm. One is observed on a single terrace, while the other one carpets the straight step. From the section profile along A-B, the height difference of the two successive germanene covered terraces is 0.23 nm (Figure 3b), corresponding to the mono-atomic step height of Ag(111). The embedded island is only 0.04 nm higher than the surrounding germanene covered terrace, as determined from the C-D section profile shown in Figure 3c. This is just the difference between the Sn and Ge atomic diameters. We stress that no 3D islands are observed in the wide-scale STM images. Furthermore, as the areal ratio of the observed stanene islands is rather smaller than the one which could be expected for the Sn 0.3 monolayer (ML) deposition, therefore, some Sn atoms might have con-currently dissolved into the Ag(111) thin film.

A zoom-in at atomic-scale of the STM image of the island shown in Figure 3d (red square in Figure 3a) reveals the clear honeycomb structure of epitaxial stanene, matching a Ag(111) (√3 × √3)R30° superstructure initially formed by a Ag 2 Sn sur-face alloy underneath, as discussed above, and precisely char-acterized earlier. [26] The honeycomb structure appears highly perfect, exhibiting no specific distortion, defects or protrusions that could have originated from substituted or on-top Ge atoms. It means that monolayer stanene is prepared without any replacement or adsorption of Ge atoms.

Similarly, a zoom-in at atomic-scale of the surrounding germanene area (Figure 3e) reveals the specific features, namely hexagons and double protrusions constitutive of the 2D (3√21 × 3√21)R10.9° germanene superstructure, which char-acterize the STM images of the perfectly oriented germanene sheet formed by germanium segregation and ordered assembly on the silver thin film initially grown on Ge(111), [24] as already displayed in Figure 2d.

We now underline that if instead of the pure Ag(111) tem-plate, the Ag 2 Sn surface alloy with (√3 × √3)R30° periodicity with respect to Ag(111)1 × 1 was lying beneath the germanene sheet, the (7√7 × 7√7)R19° superstructure with respect to silver (111) could not have formed, because of the crystallographic incompatibility between (7√7 × 7√7)R19° and (√3 × √3)R30° super periodicities. When the temperature chosen for Sn deposition during the cooling process of the Ag(111) thin film on the Ge(111) substrate is higher than about 220 °C, for example 260 °C, the surface is completely covered by germanene and no stanene phase is observed: the STM images look like the one shown in Figure 2d. Furthermore, as no 3D Sn islands appear, all deposited Sn atoms have dissolved into the silver film.

At variance, as shown above in Figure 3a, Sn atoms form large atom-thin 2D stanene islands upon deposition at 200 °C.

We note that most often more or less rounded stanene islands are formed, although elongated ones are also present. This points to rather isotropic on-surface diffusion processes, as well as similar lateral growth velocities along the main crystal-lographic directions, consequently indicating not markedly dif-ferent edge energies. Now, if instead, the deposition temperature chosen during the cooling process is too low, for example, 150 °C or less, on the contrary, 3D Sn islands are formed over the germanene sheet, as shown in Figure 3f. These results indicate that once a full germanene sheet overlays the Ag(111) surface, Sn atoms cannot kick away Ge atoms from germanene; instead, they just form 3D Sn islands on top of the germanene overlayer.

Hence, if Sn is deposited before the germanene sheet fully covers the entire surface upon cooling the substrate, Sn atoms can form stanene and/or a Ag 2 Sn surface alloy on the remaining bare areas. In other words, the heterostructures can be realized only in a narrow temperature window because of the competitive, kinetically driven processes, namely, on the one hand, Ge atom diffusion through the thin Ag(111) film, segregation on top, and surface diffusion to permit 2D germanene nucleation and lateral spreading, and, on the other hand, enough Sn atoms diffusing on the surface to nucleate 2D stanene islands on areas not yet covered by germanene. Said differently, if the Sn deposition temperature is too high, tin dissolves into the Ag thin film, if it is too low, a complete ger-manene overlayer has enough time to form, on top of which tin cannot form a stanene wetting layer, which results in 3D growth. Hence, the temperature chosen for the deposition of tin plays a crucial role.

A close-up STM image of the stanene island of Figure 3a, is shown in Figure 4a to examine the boundaries of the ger-manene and stanene domains of the lateral heterostructures. Red solid lines indicate some preferential directions for the domain boundaries. They are 30° clockwise rotated toward the Ag(111) <112> direction, which is the germanene zig-zag direction, and 19° anti-clock-wise rotated from a unit vector of the Ag(111)(7√7 × 7√7)R19° superstructure. Figure 4b displays the boundary region between stanene and germanene (for a different preparation) at atomic resolution. Although it is dif-ficult to image both sides in the same tunneling conditions, one clearly recognizes a zig-zag edge for the stanene island on the left side, and the fingerprint protrusions of the germanene sheet on the right side, also pointing to a zig-zag termination. If not truly atomically perfect, as one could desire, neverthe-less, the interface appears very narrow, with minimal disorder, pointing to a fairly abrupt junction. A schematic illustration of perfect zig-zag and armchair junc-tions between germanene and stanene on Ag(111) is displayed in Figure 5. The unit cells of the honeycomb structures of ger-manene and stanene with sides 1.35a Ag and √3a Ag along the Ag<112> and equivalent directions are rotated by 30° from that of Ag(111), whose a Ag sides are along the Ag<110> and equiva-lent directions.

From the STM image of Figure 4a, the domain boundary of germanene is rotated by 19° toward the anti-clock-wise direction from the Ag(111)(7√7 × 7√7)R19° superstructures; a germanene armchair edge is thus formed. The STM images also indicate that the domain boundaries for stanene are rotated 30° toward the clock-wise direction from the Ag(111)(√3 × √3)R30° superstructures. Hence, a stanene armchair edge is also formed. Therefore, the domain boundary, which is along the Ag(111) <1-10> direction, has armchair edges for both domains. Because the orientations of the honeycomb structures of germanene and stanene are identical to each other, the domain boundary has the same edge structure, but with different atom spacings. We notice that most domain boundaries share armchair edges, signaling minimum energy equilibrium configuration, but zigzag edges are also observed in the STM images, as shown in Figure 4b. Figure 6 shows (dI/dV)/(I/V) STS spectra for the lateral het-erostructure of stanene embedded in germanene recorded on the germanene and stanene domains, and over a region span-ning a zig-zag domain boundary. Clearly two characteristic peaks emerge at the domain boundary at -0.5 and +0.15 eV sample biases. We relate these features to a characteristic elec-tron density of states for filled and empty edge states.

The fabrication of the first silicene transistor operating at RT in 2015 [30] has opened exciting prospects for future 2D electronics. [33,34] Compatible with the current Si-based tech-nology, germanene and stanene, which are 2D topological insu-lators with significantly stronger spinorbit couplings [31] are highly promising new contenders. [34] The realization of a lateral inplane heterostructure between germanene and embedded stanene nanodots is unprecedented. To the best of our knowl-edge, until now, such heterostructures have been obtained, on the one hand, only between graphene and h-BN since 2012 [32][33][34] and with transition metal dichalcogenides since 2014, on the other hand. [8] These novel heterostructures will further boost fundamental studies, not only in electronics, but also, typically, in spintronics and optoelectronics. [37] Progress in engineering, for example, to tailor nanoribbons and lateral superlattices, and use such effects as negative differential resistance, can be [35][36][37][38] anticipated. Recently, multilayers of germanene, stanene, and antimonene have been grown directly on semiconducting molybdenum disulfides; [39] indeed, an exciting prospect would be the lateral growth of heterostructures between them.

To summarize, revolutionary developments can be foreseen, none the least in quantum science, but also for new tantalizing functional nano-devices.

Conclusion

We have successfully prepared at the nanoscale nearly atomi-cally precise lateral monolayer heterostructures of stanene embedded in germanene on a silver (111) thin film epitaxially grown on a Ge(111) substrate thanks to a synergetic combina-tion of germanium segregation from the Ge(111) substrate and tin deposition from a Sn evaporation source. The combined STM and LEED observations testify that the lateral structures on either side of the heterojunctions are pure germanene and pure stanene monolayers, respectively. The domain boundaries have mostly armchair edges, but zigzag edges are also formed. From the STS spectra, 1D edge states are revealed. To the best of our knowledge this is the first realization of a lateral hetero-junction between group 14 elemental post-graphene 2D mate-rials, whose outstanding electronic properties open exciting prospects for disruptive technologies, such as the future fabri-cation of functional 2D nano-devices compatible with conven-tional Si-based technology.

Experimental Section

The experiments were performed using an ultrahigh-vacuum (UHV) system at Nagoya University. The system consisted of a preparation chamber with a base pressure below 5 × 10 -10 mbar, and an analysis chamber with a base pressure below 10 -10 mbar.

Silver thin films (100 nm thick) were prepared on a Ge(111) substrate by conventional thermal evaporation. The details of the sample preparation of Ag thin films on Ge(111) and segregation phenomena of the Ge atoms by subsequent annealing under N 2 atmosphere are described in previous reports. [40][41][42] Clean Ag(111) surfaces were prepared by 2 keV Ar + ion sputtering at RT, followed by annealing the sample at the temperature of 400 °C. Annealing was performed by electron bombardment of the sample holder at an emission current of 5 mA and a voltage of -650 V. The sample temperature was monitored with a radiation thermometer and a type K thermocouple mounted on the base plate of the sample holder. The cleanliness of the surface was measured by Auger electron spectroscopy after sputtering and annealing; no contaminants, such as C and O, were observed within the detection limits, and a sharp (1 × 1) LEED pattern was observed.

After annealing the sample at 500 °C, tin was deposited onto the Ag(111) surface during the cooling process at various temperatures from 300 °C down to RT in UHV from a well degassed quartz crucible evaporator operating at a deposition rate of approximately 0.1 ML min -1 , as measured by placing a quartz crystal microbalance at the sample position. 1 ML was defined as a Sn overlayer with the atomic density of a Ag(111) plane: 1.38 × 10 15 atoms cm -2 . The deposition rate was accurately calibrated in advance by Rutherford backscattering spectroscopy (RBS). For the RBS measurement, a graphite substrate with an ultra-thin tin film on the surface was prepared. Details of the experimental setup for RBS have been published elsewhere. [43,44] The amounts of deposited tin were about 0.3 ML; errors in mentioned coverage ratios were less than 5%.

The system was equipped with a rear-view LEED system operating with a LaB 6 filament and a UHV STM system (Omicron STM-1). All STM images presented were acquired at RT with W tips, electrochemically etched in a KOH solution, in a constant current mode. All apparatuses were situated on an air damper with an active vibration isolation system (Kurashiki). STS spectra were obtained together with the simultaneous STM measurements by numerical derivative of tunneling current (I) versus sample bias voltage (V) and averaging over 20 equivalent sites to reduce noise.

Figure 2 .

 2 Figure 2. LEED patterns at 36 eV incident electron energy and STM images of a-b) stanene grown by deposition on a Ag 2 Sn surface alloy and c-d) germanene grown by segregation on a Ag(111) thin film in epi-taxy on a Ge(111) substrate. e) Ball models of the oriented stanene and germanene sheets. f) LEED pattern at 36 eV incident electron energy of the lateral heterostructures of germanene and stanene grown in synergy on a Ag(111) thin film in epitaxy on a Ge(111) substrate.

Figure 3 .

 3 Figure 3. Lateral heterostructures of germanene and stanene observed at RT. They were prepared on a Ag(111) thin film grown on a Ge(111) substrate after annealing at the substrate temperature of 500 °C. During the cooling process, where Ge segregation takes place, a Sn deposition of 0.3 ML at 200 °C was performed. a) Large-scale STM image (U s = +1.5 V, I = 200 pA). b) Section profile along the A-B black line in (a). c) Section profile along the C-D black line in (a). d) Atomic-scale STM image of the embedded stanene island within the red square in (a) (U s = +0.4 V, I = 200 pA). e) Atomic-scale STM image of the surrounding germanene sheet within the green square in (a) (U s = +1.0 V, I = 200 pA). f) Wide-scale STM image prepared on a Ag(111) thin film grown on a Ge(111) substrate after annealing at the substrate temperature of 500 °C with a Sn deposition of 0.3 ML at 150 °C during the cooling process. (U s = +1.5 V, I = 200 pA), showing Sn 3D islanding at this too low temperature.

Figure 4 .

 4 Figure 4. a) STM image of the lateral in-plane heterostructure of stanene and germanene (U s = +1.5 V, I = 200 pA). The solid yellow and red lines represent domain boundaries with zigzag and armchair edges. b) High-resolution STM image of a zig-zag boundary of the lateral inplane hetero-structure of germanene and stanene (U s = +1.5 V, I = 200 pA).

Figure 5 .

 5 Figure 5. Structural model of the lateral heterostructure of germanene and stanene on Ag(111) with armchair (marked by a red line) and zig-zag (marked by a yellow line), keeping the unit cell of germanene and stanene, namely, 1.35 × 1.35R30° and (√3 × √3)R30°, respectively. The areal positions corresponding to the hexagonal and double-dotted protrusions in Figure 3e are marked by white circles and ovals.

Figure 6 .

 6 Figure 6. STS spectra of a germanene zone, a zigzag domain boundary region, and a stanene zone of the heterostructure on the same terrace of the Ag(111) thin film.

Acknowledgements

J.Y. acknowledges financial support from Toyoaki Scholarship Foundation and the Murata Science Foundation in 2017 and 2019, respectively. G.L.L. acknowledges support from Nagoya University thanks to two "Eminent Foreign Scientist" Invitation Awards in 2015-2016 and in 2019-2020, as well as an Invitational Fellowship for Research in Japan by the Japan Society for the Promotion of Science (JSPS) in 2017.