Juraj Kolčák
email: kolcak@lsv.fr

Jérémy Dubut
email: dubut@nii.ac.jp

Ichiro Hasuo
email: hasuo@nii.ac.jp

Shin-Ya Katsumata
email: s-katsumata@nii.ac.jp

David Sprunger
email: sprunger@nii.ac.jp

Akihisa Yamada
email: akihisayamada@nii.ac.jp

Relational Differential Dynamic Logic

Keywords: hybrid system, cyber-physical system, formal verification, theorem proving, dynamic logic

In the field of quality assurance of hybrid systems, Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as "an earlier engagement of the emergency brake yields a smaller collision speed." A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

Introduction

Hybrid Systems Cyber-physical systems (CPSs) have been studied as a subject in their own right for over a decade, but the rise of automated driving in the last few years has created a panoply of challenges in the quality assurance of these systems. In the foreseeable future, millions of cars will be driving on streets Thanks are due to Stefan Mitsch, André Platzer, and Yong Kiam Tan for useful tips on the KeYmaera X source code; and to Kenji Kamijo, Yoshiyuki Shinya, and Takamasa Suetomi from Mazda Motor Corporation for helpful discussions. The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. I.H. is supported by Grant-in-Aid No. 15KT0012, JSPS. J.D. is supported by Grant-in-aid No. 19K20215, JSPS. The work was done during J.K.'s internship at the National Institute of Informatics, Tokyo, Japan.

with unprecedented degrees of automation; ensuring the safety and reliability of these automated driving systems is a pressing social and economic challenge.

The hybridity of cyber-physical systems, the combination of continuous physical dynamics and discrete digital control, poses unique scientific challenges. To address these challenges, two communities have naturally joined forces: control theory whose traditional application domain is continuous dynamics and formal methods that have mainly focused on the analysis of software systems. This has been a fruitful cross-pollination: techniques from formal methods such as bisimilarity [START_REF] Girard | Approximate bisimulation: A bridge between computer science and control theory[END_REF] and temporal logic specification [START_REF] Fainekos | Robustness of temporal logic specifications[END_REF] have been imported to control theory, and conversely, control theory notions such as Lyapunov functions have been used in formal methods [START_REF] Takisaka | Ranking and repulsing supermartingales for reachability in probabilistic programs[END_REF].

Deductive Verification of Hybrid Systems In the formal methods community, two major classes of techniques are model checking (usually automatabased and automatic) and deductive verification (based on logic and can be automated or interactive). Model checking techniques rely on exhaustive search in state spaces and therefore cannot be applied per se to hybrid systems with infinite state spaces. This has led to the active study of discrete abstraction of hybrid dynamics; see e.g. [START_REF] Girard | Approximate bisimulation: A bridge between computer science and control theory[END_REF].

In contrast, nothing immediately rules out the use of the deductive approach for hybrid systems. Finitely many variables in logical formulas can represent infinitely many states, and proofs in suitably designed logics are valid even when the semantic domain is uncountable. That said, designing such a logic, proving the soundness of its rules, and showing that logics is actually useful in hybrid system verification is a difficult task.

Platzer's differential dynamic logic dL [START_REF] Platzer | Logical Foundations of Cyber-Physical Systems[END_REF] is a remarkable success in this direction. Its syntax is systematic and intuitive, extending the classic formalism of dynamic logic [START_REF] Harel | Dynamic Logic[END_REF] with differential equations as programs. Its proof rules encapsulate several essential proof principles about differential equations, including a differential invariant (DI) rule for universal properties and side deduction for existential properties. The logic dL has served as a general platform that accommodates a variety of techniques, including those which come from real algebraic geometry [START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF]. Furthermore, dL comes with sophisticated tool support: the latest tool KeYmaera X [START_REF] Mitsch | The keymaera X proof IDE -concepts on usability in hybrid systems theorem proving[END_REF] comes with graphical interface for interactive proving and a number of automation heuristics.

Relational Reasoning on Hybrid Systems

In this work, we introduce proof-based techniques for relational reasoning to the deductive verification of hybrid systems. In particular, we aim to provide logical support for reasoning about differences in outcomes between similar scenarios based on some known differences in their parameters. As a simple example, consider the following example distilled from our collaboration with an industrial partner. Example 1 (leading example: collision speed). Consider two cars C and C, whose positions and velocities are real numbers denoted by x, x and v, v, respectively. Their dynamics are governed by the following differential equations:

ẋ = v, v = 1; ẋ = v, v = 2. ( 1
) 1 √ 2 √ 2 2 v = 2 v = 1 t v
The two hatched areas designate the traveled distances (x = x = 1). We can compute the collision speeds (v = √ 2 and v = 2) via the closed-form solutions of the differential equations (1), concluding v ≤ v when x = x = 1. Both cars start at the same position at rest (x = x = 0 ∧ v = v = 0), and both drive towards a wall at position 1. We consider this question: which car is traveling faster when it hits the wall?

The second car, C, has strictly greater acceleration all the time, so we can imagine that C hits the wall harder. This hypothesis turns out to be correct, but we are more interested in how this claim could be proven.

A simple proof would be to solve the differential equation exactly and notice C has greater velocity at the end of its run. However, it is known that closed-form solutions are scarce for ODEs-we want a proof method that is more general.

Another possible argument is based on the relationship between the accelerations. Since the second car's acceleration is greater at every point in time, we might be tempted to conclude that the second car's velocity must always be greater than the first car's, based on the monotonicity of integration: a

(t) ≤ a(t) ⇒ v(t) = T 0 a(t) dt ≤ T 0 a(t) dt = v(t)
. However, this reasoning has a flaw. C reaches the wall at an earlier point in time than C, and therefore C has more time to accelerate. In the end, we have to compare T 0 a(t) dt and T 0 a(t) dt where a(t) ≤ a(t) for all t ∈ [0, T ] but T > T , as depicted in figure 1.

Our solution, roughly stated, is to compare the two cars at the same points in space by reparametrizing time for one of the two cars. This parametrization is specially chosen to ensure the two cars pass through the same points in space at the same points in time.

Our current work is about a logical infrastructure needed to support this kind of relational reasoning comparing two different dynamics, based on dL. Our semantical theory, as well as the resulting syntactic extension of dL by what we call the synchronization rule, generalizes the kind of reasoning in Example 1 using the notion of time stretching.

Technical Contributions

We make the following technical contributions.

1. Formulation of relational reasoning in dL. We find that relational properties are expressible in dL, using disjoint variables in a sequential composition. This representation, however, does not allow the use of the rich logical infrastructure of dL (such as the (DI) rule). 2. Time stretching, semantically and syntactically. To abbreviate this difficulty, we first develop the theory of time stretching, so that we can compare two dynamics at different timepoints (cf. Example 1). Accommodating this semantical notion in dL and KeYmaera X is not possible per se. We introduce an indirect syntactic alternative, which turns out to be better suited in fact to many case studies (where we compare the two dynamics at the same "position," much like in Example 1). The resulting synchronization rule in dL has a clean presentation (Theorem 24), owing to the syntactic Lie derivative operator in dL. 3. Implementation and case studies. We implemented the new synchronization rule as an extension of KeYmaera X. We used it successfully for establishing nontrivial relational properties in case studies taken from the automotive domain.

Relational Reasoning in Practice We contend relational reasoning has practical significance based on our collaboration with an industry partner. Relational properties, especially with an aspect of monotonicity, abound in real-world examples. In particular, we have often encountered situations where we have a parametrized model M (p) and need to show a property like:

p 1 < p 2 implies M (p 2 ) is less safe than M (p 1 ). ( 2
)
These properties occur especially in the context of product lines, where the same model can come in many slight variants. Example 1 is such a situation.

Relational statements (such as monotonicity) are easy to state and interpret. Intuitions about the direction of the change in a behavior of a system resulting from the change of a parameter are more often valid than intuitions about the amount of such a change. These kinds of simple statements are often used by engineers to establish the basic credibility of a model. Qualitative, relational properties also tend to be easier to prove than exact, quantitative properties.

Finally, monotonicity can serve as a powerful technique in test-case reduction. If a safety property is too complex to be deductively verified, one usually turns to testing. It is often still possible to establish a simple monotonicity property of the form (2). This can still powerfully boost testing efforts: one can focus exclusively on establishing safety for the extreme case M (p max ).

Related Work Since this work is about its relational extension, the works we mentioned on dL are naturally relevant. We discuss other related works here.

Simulink (Mathworks, Inc.) is an industry standard in modeling hybrid systems, but unfortunately Simulink models do not come with rigorously defined semantics. Therefore, while integration with Simulink is highly desirable any quality assurance methods for hybrid systems, formal verification methods require some work to set up the semantics for Simulink models. The recent work [START_REF] Liebrenz | Deductive verification of hybrid control systems modeled in simulink with keymaera X[END_REF] tackles this problem, identifying a fragment of Simulink, and devising a translator from Simulink models to dL programs. Their translation is ingenious, and their tool is capable of proving rather complicated properties when used in combination with KeYmaera X [START_REF] Mitsch | The keymaera X proof IDE -concepts on usability in hybrid systems theorem proving[END_REF].

Relational extensions of the Floyd-Hoare logic-which can be thought of as a discrete-time version of dL-have been energetically pursued especially in the context of differential privacy [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF][START_REF] Aguirre | A relational logic for higher-order programs[END_REF][START_REF] De Amorim | Metric semantics for probabilistic relational reasoning[END_REF].

In deductive verification of hybrid systems, an approach alternative to dL uses nonstandard analysis [START_REF] Robinson | Non-standard analysis[END_REF] and regards continuous dynamics as if they were discrete due to the existence of infinitesimal elements [START_REF] Suenaga | Programming with infinitesimals: A while-language for hybrid system modeling[END_REF][START_REF] Suenaga | Hyperstream processing systems: nonstandard modeling of continuous-time signals[END_REF]. The logic used in that framework is exactly the same as the classic Floyd-Hoare logic, and the soundness of the logic in the hybrid setting is shown by a model-theoretic result called the transfer principle. Its tool support has been pursued as well [START_REF] Hasuo | Exercises in Nonstandard Static Analysis of hybrid systems[END_REF]. This is not the first time that relational reasoning-in a general sensehas been pursued in dL. Specifically, Loos and Platzer introduce the refinement primitive β ≤ α, which asserts a refinement relation between two hybrid dynamics, meaning the set of successor states of β is included in that of α [START_REF] Loos | Differential refinement logic[END_REF]. This kind of relation is inspired by the software engineering paradigm of incremental modeling (supported by languages and tools such as Event-B [START_REF] Abrial | Modeling in Event-B -System and Software Engineering[END_REF][START_REF] Butler | Modelling and refining hybrid systems in event-b and rodin[END_REF]); the result is a rigorous deductive framework for refining an abstract model (with more nondeterminism) into a more concrete one (with less nondeterminism). In contrast, we compare one concrete model (not necessarily with nondeterminism) with another. Thus, our notion of relational reasoning builds more on relational extensions of the Floyd-Hoare logic [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF][START_REF] Aguirre | A relational logic for higher-order programs[END_REF][START_REF] De Amorim | Metric semantics for probabilistic relational reasoning[END_REF] than on Event-B. Combining these two orthogonal kinds of relational extensions of dL is important future work.

Organization In Section 2, we recall some basics of differential dynamic logic dL: its syntax, semantics and some proof rules. Our main goal, relational reasoning, is formulated in Section 3, where we identify difficulties in doing so in the original dL. In Section 4 we introduce the semantical notion of time stretching, and turn its theory into the new synchronization rule. After introducing our implementation in Section 5, we describe our three case studies in Section 6.

Some proofs and details are deferred to the appendix. It is found at http: //group-mmm.org/ ~ayamada/rddl_tacas_2020/.

Preliminaries: Syntax and Semantics of the Logic dL

We recall some of the basics of differential dynamic logic (dL). The interested reader is referred to [18,[START_REF] Platzer | A complete uniform substitution calculus for differential dynamic logic[END_REF] for full details.

Definition 2 (language). We fix a set V of variables, denoted by x, y, . . . . The set of terms is defined by the following grammar: e, f, g, . . .

::= x | n | -e | e + f | e • f | e/f
where x ∈ V and n ∈ N. First-order formulas are defined by

P, Q, . . . ::= e ≤ f | ¬P | P ∧ Q | ∀x. P
A state is a function sending each variable to a real number, ω : V → R. We denote the set of all states by R V . Given a state, each term has a valuation in the reals, and each formula has a valuation in Booleans defined by the usual induction. We denote these by e ω ∈ R and P ω ∈ {true, false}, respectively. The models of a first-order formula P are the states satisfying P ,

P := {ω ∈ R V | P ω = true}.
We use classical shorthands, including e = f := e ≤ f ∧ f ≤ e, P ∨ Q := ¬(¬P ∧ ¬Q), ∃x. P := ¬(∀x. ¬P ), and := 0 ≤ 0. We denote a vector (e 1 , . . . , e n ) of terms (or variables) by e when the length n is irrelevant or clear from the context.

We now introduce the syntax of hybrid programs.

Definition 3 (hybrid programs). The set HP(V) of hybrid programs over variables V is given by the following grammar:

α 1 , α 2 , . . . ::= ?P | x := e | ẋ1 = e 1 , . . . , ẋn = e n & Q | α 1 ; α 2 | α 1 ∪ α 2 | α *
We may also abbreviate ẋ1 = e 1 , . . . , ẋn = e n by ẋ = e. Hybrid programs of the form ẋ = e & Q are especially important in this work. We call such a program differential dynamics, where ẋ = e is its differential equation and the first-order formula Q is its evolution domain constraint. The intuitive meaning of such a program is that the values of the variables x evolve continuously in time according to ẋ = e, as long as Q is satisfied at the current value of x. If we see differential dynamics as a continuous analog of loops, then Q plays the role of guard and ẋ = e plays the role of body. 5 We write ẋ = e instead of ẋ = e & .

Definition 4 (solutions). A mapping

ψ : [0, T ) → R V with T ∈ [0, ∞]
is called a solution of a differential equation ẋ1 = e 1 , . . . , ẋn = e n if ψ is differentiable in [0, T ) and, whenever t ∈ [0, T ), ψ(t)(x i ) = e i ψ(t) for i ∈ {1, . . . , n} and ψ(t)(y) = 0 for any y ∈ V \ {x 1 , . . . , x n }.

According to the Picard-Lindelöf theorem [15], for each differential equation ẋ = e and each state ω, there is a unique maximal solution Definition 6 (dL formulas). Modal formulas extend first-order formulas and are defined by the following grammar:

ψ ω : [0, T ω ) → R V of the differential equation satisfying ψ ω (0) = ω. Definition 5 (semantics of hybrid programs). The semantics of a hybrid program α is a relation -α → ⊆ R V × R V on states, defined by: 1. -?P → = {(ω, ω) | ω ∈ P }, 2. -x := e → = {(ω, ω ) | ω (x) = e ω and ω (y) = ω(y) for all y = x}, 3. -ẋ = e & Q → = {(ω, ψ ω (t)) | ω ∈ R V , t ∈ [0, T ω ), ψ ω ([0, t]) ⊆ Q }, 4. -α 1 ∪ α 2 → = -α 1 → ∪ -α 2 →, 5. -α 1 ; α 2 → = -α 1 →; -
ϕ, ϕ 1 , ϕ 2 , . . . ::= e ≤ f | ¬ϕ | ϕ 1 ∧ ϕ 2 | ∀x. ϕ | α ϕ.
As usual, we write α ϕ to abbreviate ¬ α ¬ϕ. We will also call modal formulas "dL formulas" since these are the widest class of formulas in dL.

The Boolean valuation ϕ ω of a modal formula ϕ in a state ω is defined the same way as for first-order formulas, with the addition of α ϕ ω = true if and only if ϕ ω = true for all ω such that ω -α → ω .

We take the sequent-calculus style proof system for dL, following [START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF]. It has judgments of the form Γ ϕ, where Γ is a set of modal formulas and ϕ is a single modal formula. One of the most fundamental axiom is

ẋ = e & Q φ ⇐⇒ ∀t ≥ 0. (∀v ∈ [0, u]. [x := f (v)]Q) ⇒ [x := f (u)]φ (solve)
where f (t) is a term with a fresh variable t such that f is a solution of ẋ = e and f (0) = id.

Some other rules of dL, such as the differential invariant rule (DI) that is central in many proofs, are introduced later in Definition 13.

Relational Differential Dynamic Logic

Intuitively, we want a way to describe two dynamics that are executed in parallel, and compare their outputs. In terms of (nondeterministic) transition systems, parallel composition is available via tensor products.

Definition 7 (tensor product). Given two transition systems (S, R) and (S , R ), their tensor product (S × S , R ⊗ R ) is defined to be the transition system whose transition relation is given by

R ⊗ R := {(s, s ), (t, t ) | (s, t) ∈ S, (s , t ) ∈ R }.
No extension of the dL syntax is needed to model tensor products: disjointness of the variables of the two systems suffices. From now on we split variables into two disjoint sets: V = V V. We denote variables in V by x, y, . . . and those in V by x, y, . . . . Terms in T (V), first-order formulas in Fml (V), and programs in HP(V) are denoted by e, f , . . . , P , Q, . . . , and α, β, . . . , and similarly for the corresponding constructs with V.

An easy proof of the following fact can be found in the appendix.

Proposition 8. -α → ⊗ -α → = -α; α →
Scenarios with two parallel differential dynamics are the main focus of this work. We formalize an assertion relating two dynamics using the following format. It is a syntactic counterpart of Proposition 8.

Definition 9 (relational differential dynamics). We call hybrid programs of the following form relational differential dynamics (RDD)

ẋ = e & Q ; ẋ = e & Q (3)
Now that we have ways to express separate systems evolving in parallel, we turn to the construction of proofs which reason about their relationships.

Example 10. Using RDD, the problem in Example 1 is expressed as

Γ C δ C ; δ C φ C where δ C := ẋ = v, v = 1 , δ C := ( ẋ = v, v = 2), Γ C := {x = x = 0, v = v = 0} is the precondition, and φ C := (x = x = 1 ⇒ v ≤ v) is the postcondition.
Let us prove, in KeYmaera X, the RDD sequent

Γ C δ C ; δ C φ C .
In KeYmaera X, the only applicable rule to this sequent turns it into Γ C δ C δ C φ C . We then explicitly "solve" the second dynamics, yielding the following goal:

Γ C δ C ∀t ≥ 0. x = x + v • t + t 2 = 1 ⇒ v ≤ (v + t) (4)
where x and v in φ C are replaced by their explicit solutions with respect to the freshly introduced time variable t. Again differential invariant rules do not apply to (4), so one must solve the first dynamics, too, yielding

Γ C ∀t ≥ 0. ∀t ≥ 0. x + v •t + t 2 /2 = x + v • t + t 2 = 1 ⇒ (v + t) ≤ (v + t)
Since this goal is first order, the quantifier elimination, a central proof technique in KeYmaera X [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF], proves the goal.

The above example worked out since it admits explicit solutions expressible in dL. This is not always the case as the following example demonstrates.

Example 11. We consider two objects moving through fluids subjected to different kinds of drag. One object moves through a viscous fluid and is therefore subject to linear drag; its dynamics are δ

F := ( ẋ = v, v = -v).
The other object moves through a less viscous fluid and is subject to turbulent drag; its dynamics are δ F := ( ẋ = v, v = -v 2 ). Our goal is to show that the latter has higher speed when both objects reach a certain point in space (x = x = l).

The following functions v * , x * , v * and x * are solutions of the dynamics.

v * (t) = v 0 • e -t x * (t) = x 0 + v 0 • (1 -e -t ) v * (t) = v 0 1 + v 0 •t x * (t) = x 0 + log(1 + v 0 •t)
where v 0 etc. denote the initial values. Unfortunately, we cannot express exponentiations and logarithms in KeYmaera X, and thus the "solve" rule that we used in Example 10 cannot be applied here.

One obvious solution to this would be to add support for exponentiations and logarithms in KeYmaera X, but this would break the decidability of the underlying first order logic, which is a major feature of dL [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF]. In fact, the same issue occurs even in standard use cases of KeYmaera X, and motivated the introduction of proof rules which do not demand explicit solutions to differential dynamics [START_REF] Platzer | A complete uniform substitution calculus for differential dynamic logic[END_REF][START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF] using the Lie derivative.

Definition 12 (formal Lie derivative in dL from [START_REF] Platzer | A complete uniform substitution calculus for differential dynamic logic[END_REF][START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF]). The formal Lie derivative of a term f along dynamics δ

≡ ( ẋ = e & Q) of dimension n is a dL term L δ f ∈ T (V) given by 6 L δ f := ∂ ∂x1 f • e 1 + • • • + ∂ ∂xn f • e n Definition 13
(proof rules from [START_REF] Platzer | A complete uniform substitution calculus for differential dynamic logic[END_REF][START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF]). The following rules are sound:

Γ, Q f ∼ 0 Γ δ L δ f 0 Γ δ f ∼ 0 DI Γ p ∼ 0 Q L δ p g • p Γ δ p ∼ 0 Dbx
where δ ≡ ( ẋ = e & Q), (∼, ) ∈ { (=, =), (>, ≥), (≥, ≥) }, and g is any term without division.

The differential invariant rule (DI) is the central rule for proving safety properties [START_REF] Platzer | A complete uniform substitution calculus for differential dynamic logic[END_REF][START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF]: it reduces a global property of the dynamics to local reasoning by means of Lie derivatives. The Darboux inequality rule (Dbx) is derived from real algebraic geometry; see e.g. [START_REF] Platzer | Differential equation axiomatization: The impressive power of differential ghosts[END_REF].

Example 14. Consider an example differential dynamics in one variable, ẋ = 2. Suppose we want to show that x ≥ 0 holds after following these dynamics for any amount of time, starting from x = 1. One way to do this is to show that (1) this predicate holds initially (1 ≥ 0) and (2) the time derivative of x is always nonnegative. These are precisely the two premises of the (DI) rule: to show the sequent x = 1 [ ẋ = 2]x ≥ 0 (DI) requires us to prove (1) x = 1 x ≥ 0 and (2) x = 1 [ ẋ = 2]L ẋ=2 x ≥ 0, where L ẋ=2 x = 2. Note that we give an initial condition x = 1 in the precedent of this sequent.

Synchronizing Dynamics

The intuitive explanation of the RDD construction of Definition 9 is a "serialization" of two dynamics. This construction however does not match the (DI) and (Dbx) rules, as they accept only one dynamics followed by a comparison. In order to make use of these rules in our relational reasoning, we introduce another proof method. It "synchronizes" two dynamics.

After some theoretical preparations we define the new rule and prove its soundness. We will illustrate the usefulness of this rule in Section 6, through some case studies that are inspired by our collaboration with the industry.

Time Stretching

A key theoretical tool towards the soundness of our synchronization rule is called time stretching. Its idea is very much like the technique of time-reparametrization for ODEs [START_REF] Chicone | Ordinary Differential Equations with Applications[END_REF].

Definition 15 (time stretch function). Let T ∈ R ≥0 . A function K : [0, T ] → R ≥0 is a time stretch function if K(0) = 0, K is continuously differentiable and K(t) > 0 for each t ∈ [0, T ].
Remark 16. The condition K(t) > 0 ensures that K is strictly increasing and is a bijection from [0, T ] to [0,

K(T )]. The inverse of K is K -1 : [0, K(T )] → [0, T ],
and it is straightforward to check K -1 is another time stretch function.

The next results tell us how to turn an ODE into another, given a time stretching function K, so that a time-stretch ψ•K of a solution ψ of one becomes a solution of the other.

Lemma 17. Suppose f : R V → R V is a vector field and K : [0, T ] → [0, K(T )] is a time stretch function. If ψ : [0, K(T )) → R V satisfies ψ(s) = f (ψ(s)) for all s ∈ [0, K(T )), then the function ρ = ψ • K : [0, T ) → R V satisfies ρ(t) = K(t) • f (ρ(t)) for all t ∈ [0, T ). Proof. We have ρ(t) = K(t)• ψ(K(t)) = K(t)•f (ψ(K(t))) = K(t)•f (ρ(t))
, where the first equality is by the definitions and the chain rule, the second equality is by the assumption on ψ, and the last equality is by the definition of ρ.

Since the inverse of a time stretch function is another time stretch function, we obtain the following corollary of Lemma 17.

Corollary 18. Let K : [0, T ] → [0, K(T )] be a time stretch function. Let ρ : [0, T ) → R V satisfy ρ(t) = K(t) • f (ρ(t)) whenever 0 ≤ t < T . Then the function ψ : [0, K(T )) → R V , defined by ψ(s) := ρ(K -1 (s)), satisfies ψ(s) = f (ψ(s)) whenever 0 ≤ s < K(T ).

Towards a Syntactic Representation

So far our time-stretch function K has been a semantical object. Here we introduce a syntactic way of reasoning via time-stretch functions. Since a desired time-stretch function is not necessarily expressible in dL, our syntactic reasoning uses an indirect method that exploits a pair of functions called a synchronizer. We will be eventually led to a syntactic reasoning rule (Sync) (Thm. 24).

Given a term g ∈ T (X) and a mapping ψ : [0, T ) → R X , we define

g ψ : [0, T ) → R by g ψ (t) := g ψ(t) . (5)
Intuitively, g ψ (t) is the value of g at time t when we follow the dynamics whose solution is ψ.

Definition 19 (synchronizers). Let (δ, δ) be a pair of dynamics, (ω, ω) ∈ R V × R V be a pair of states, and ψ : [0, T ) → R V and ψ : [0, T ) → R V be the unique solutions of δ and δ from ω and ω, respectively. We say a pair of dL terms (g, g) ∈ T (V) × T (V) synchronizes (δ, δ) from (ω, ω) if the following hold.

g ψ (0) = g ψ (0) -The derivatives of g ψ and g ψ are both strictly positive.

The following lemma ensures that, for any synchronizer, a corresponding time stretch function exists.

Lemma 20. In the setting of Definition 19, let t ∈ [0, T ) and t ∈ [0, T ) be such that g ψ (t) = g ψ (t). Then the function K, defined by K(s)

:= g ψ -1 (g ψ (s)), is a time stretch function from [0, t] to [0, t]. Moreover we have K(s) = ġ ψ (s) ġ ψ (K(s)) .
Proof. Since g ψ is strictly monotonic on [0, t], it has an inverse g ψ -1 defined from g ψ ([0, t]) to [0, t]. By assumption we have g ψ (0) = g ψ (0), and thus

K(0) = g ψ -1 (g ψ (0)) = g ψ -1 (g ψ (0)) = 0. Also since g ψ (t) = g ψ (t), we see that g ψ -1 is defined from g ψ ([0, t]) to [0, t]. Thus K = g ψ -1 • g ψ is defined from [0, t] to [0, t]. K(s) = ġ ψ (s) • ˙ g ψ -1 (g ψ (s)) derivative of K = g ψ -1 • g ψ = ġ ψ (s) ġ ψ (g ψ -1 (g ψ (s))) derivative of g ψ -1 = ġ ψ (s) ġ ψ (K(s))
whose value is positive by assumptions on the derivatives of g ψ and g ψ .

We remark that time stretch functions we obtain in Lemma 20 are not necessarily expressible as a dL term, as exemplified by the following example.

Example 21. Consider two dynamics δ

F := ( ẋ = v, v = -v 2 ) and δ := ( ẋ = 1). Their solutions ψ, ψ : R ≥0 → R 2 from initial value x = 0, v = 1 are ψ(s) = log(1 + s), (1 + s) -1 ψ(s) = (s, 0)
Now let g = x and g = x. Then g ψ (s) = log(1 + s), g ψ = g ψ -1 = id and thus K(s) = g ψ -1 (g ψ (s)) = log(1 + s). This is not rational and not expressible in dL.

Using the syntactic Lie derivative (Definition 12), we state a sound inference rule that does not need K to be represented explicitly. We note that there is strong support for Lie derivatives in the tool KeYmaera X, as a key syntactic operation behind the differential invariant (DI) rule (Definition 13).

Definition 22. Let δ := ẋ = e & Q and δ := ẋ = e & Q be two dynamics and let (g, g) ∈ T (V)×T (V) (which is supposed to be a synchronizer). We define the synchronized dynamics of (δ, δ) with respect to (g, g) as follows:

δ ⊗ (g,g) δ := ẋ = e, ẋ = L δ g L δ g • e & Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0
Lemma 23. Let (g, g) be a synchronizer of (δ, δ) from (ω 0 , ω 0 ). The following are equivalent, where the semantical transition relations are from Definition 5.

1.

(ω 0 , ω 0 ) -δ; δ → (ω, ω) and (ω, ω) ∈ g = g 2. (ω 0 , ω 0 ) -δ ⊗ (g,g) δ → (ω, ω)
Proof. We first prove (1 ⇒ 2). In the proof of Lemma 20, we can observe that ġ ψ (s) = L δ g ψ(s) , and analogously, ġ ψ (s) = L δ g ψ(s) . Hence we obtain

K(s) = L δ g ψ(s) L δ g ψ(K(s)) = L δ g L δ g ρ(s) (6)
where

ρ : [0, t) → R V V is defined by ρ(s) := ψ(s), ψ(K(s)) . We note that K : [0, t] → [0, K(t)
] is a time-stretch function, and that ψ is a solution of ẋ = e, that is, ψ(u) = e ψ(u) whenever 0 ≤ u < t = K(t). Combined with Lemma 17, we obtain

˙ ψ • K (s) = K(s) • e ψ(K(s)) = K(s) • e ρ(s) whenever 0 ≤ s < t.
Hence, with the fact that ψ is a solution of ẋ = e, we obtain

ρ(s) = ψ(s), ˙ ψ • K (s) = e ρ(s) , K(s) • e ρ(s) = e, L δ g L δ g • e ρ(s) whenever 0 ≤ s < t.
Here the last equality is from [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF]. This concludes that ρ is a solution of the dynamics δ ⊗ (g,g) δ. It remains to prove that for all τ ∈ [0

, t], Q ∧ Q ∧ L δ g > 0 ∧ L δ g > 0 ρ(τ )
is true. This is an easy consequence of item 1, and the fact that (g, g) is a synchronizer of (δ, δ) from (ω 0 , ω 0 ).

For the direction (2 ⇒ 1), let (ξ, ξ)

: [0, T ) → R V × R V be the unique solution of δ ⊗ (g,g) δ from (ω 0 , ω 0 ). Then there is t ∈ [0, T ) such that (ξ(t), ξ(t)) = (ω, ω). Let us prove that (ω, ω) ∈ g = g . The function h : s ∈ [0, T ) → g ξ(s) - g ξ(s)
is equal to 0 at s = 0 and its derivative is given by:

ḣ(s) = L δ g ξ(s) -L δ g ξ(s) . L δ g ξ(s) L δ g ξ(s) = 0
Consequently, h is the constant function equal to 0, which implies that (ω, ω) ∈ g = g . By definition, ξ is a solution of δ, so ω 0δ → ω. Furthermore, by Corollary 18, ξ • K -1 is a solution of δ. Thus ω 0δ → ω and (ω 0 , ω 0 )δ; δ → (ω, ω).

The above lemma is a key observation in the current work. It allows us to turn the relational dynamics δ; δ-expressed as a sequential composition in dLinto a combined dynamics δ ⊗ (g,g) δ. Moreover, we can do so in a way that the two dynamics are synchronized in a reparametrized manner, as specified by (g, g). Such combination of two dynamics is crucial in exploiting the logical infrastructure of dL and KeYmaera X-we emphasize again that the (DI) rule does not support invariant reasoning about the relationship between δ and δ, when the relational dynamics is expressed in the original form δ; δ.

The following is an incarnation of Lemma 23 as a proof rule. We assume that a postcondition is a conditional form E ⇒ ϕ; E is called an exit condition. By assuming that E implies g = g, we enforce the second condition (ω, ω) ∈ g = g in item 1 of Lemma 23. The first three premises are there to ensure that (g, g) is a synchronizer. Under these premises (the first four), the rule allows one to transform its conclusion (about δ; δ) into one about the combined dynamics δ ⊗ (g,g) δ, which is amenable application of the (DI) rule, for example.

Theorem 24 (synchronization rule). The following inference rule is sound:

Γ [δ]L δ g > 0 Γ g = g Γ [δ]L δ g > 0 E g = g Γ [δ ⊗ (g,g) δ](E ⇒ ϕ) Γ [δ; δ](E ⇒ ϕ) (Sync)
Recall the definition of δ ⊗ (g,g) δ (Definition 22), where time stretching for the second dynamics δ is expressed syntactically by Lie derivatives. We call the for premises Γ g = g, E g = g, Γ

[δ]L δ g > 0, and Γ [δ]L δ g > 0 the synchronizability conditions. These obligations are usually easy to discharge. The last premise, which we call the synchronized formula, is typically the core remaining obligation.

Remark 25 (choice of (g, g)). In applying the (Sync) rule, one still has to find a suitable synchronizer (g, g). This turns out to be straightforward in many examples. In all the case studies in Section 6 and in Example 1, the exit condition E is of the form x = x = C where C is a constant. This suggests the use of g = x, g = x. Indeed, all our proofs use this choice of (g, g).

Implementation

KeYmaera X [START_REF]Keymaera X homepage[END_REF] is an interactive theorem prover based on the sequent calculus formulation of dL. It is implemented in Scala, replacing its former system KeYmaera [START_REF]Keymaera homepage[END_REF]. It has a web-based GUI environment, and a support of automated theorem proving using computer algebra systems such as Mathematica [START_REF] Inc | Mathematica, Version 12.0[END_REF].

For the formalization of case studies in Section 6, we extended KeYmaera X version 4.7 (available at [START_REF]Keymaera X homepage[END_REF]) with the (Sync) rule. This extension of KeYmaera X, together with our proofs in case studies, are currently available at http: //group-mmm.org/ ~ayamada/rddl_tacas_2020/.

The KeYmaera X implementation is structured in a flexible manner, from which we benefited. To add a rule to KeYmaera X, one has to implement a Scala program that take the conclusion of the rule and generate the premises of the rule as subgoals. The fact that any Scala program is allowed here enabled us to implement complex algorithms, such as inductive translation of formulas.

In implementing the (Sync) rule, the functions in KeYmaera X called helpers helped us, such as in the Lie derivative computation and the functionality to simplify formulas into equivalent ones. The bulk of our effort regarded the ⊗ (g,g) operator. There we did a bit more general than we stated in the paper: not only taking dynamics of form ẋ = e & Q, we also allow sequences of dynamics possibly interleaved by guards and nondeterministic choices. This feature was utilized in the case study that will be described in Section 6.3.

Case Studies

We describe three case studies where we proved relational properties of hybrid dynamics. We did so formally in our extension of KeYmaera X described in Section 5. In all the examples, we apply the (Sync) rule as a main proof step, in conjunction with the existing rules in dL. Below, we describe our example systems and outline the important steps in the formal proofs.

Collision Speed with Constant Acceleration

In this section we apply the (Sync) rule to the running Example 1. For this example we consider two dynamics δ C := ẋ = v, v = a and δ C := ( ẋ = v, v = a). Both dynamics represent a car with constant acceleration. Our claim is that if acceleration is larger in the first system, then the first car is necessarily faster than the second car after traveling the same distance l; formally,

Γ δ C ; δ C (x = l ∧ x = l ⇒ v ≤ v) (7)
where

Γ := {0 = x = x, 0 < v = v 0 , v = v 0 , v 0 ≤ v 0 , 0 ≤ a ≤ a}
We apply the (Sync) rule, where g := x and g := x. The first two synchronizability conditions are Γ x = x and x = l, x = l x = x, which are trivial. The last two synchronizability conditions are

Γ δ C L δ C g = v > 0 Γ δ C L δ C g = v > 0
which are proved using differential invariants (DI). The synchronized formula is

Γ δ C , ẋ = v •(v/v), v = a •(v/v) & v > 0 ∧ v > 0 (x = l ∧ x = l ⇒ v ≤ v)
One might try to show the inequality vv ≥ 0 by the differential invariant (DI) rule, but the Lie derivative of the term vv is aa • (v/v), which is not obviously nonnegative. Instead, a trickier expression a

•(v 2 -v 2 0 )-a•(v 2 -v 2 0 ) = 0 turns out to be an invariant. Its Lie derivative is a • (2v) • a • (v/v) -a • (2v) • a,
which is clearly 0, since we also know v > 0.

We do not have an intuitive explanation for this invariant, but it was found by a template-based search, like many other invariants in dL. By positing the existence of a polynomial invariant of a certain degree, we can find conditions on the coefficients by requiring its Lie derivative and initial value are zero. Solving these conditions for a second-degree invariant on the velocities in the system yielded the invariant above.

After finding our invariant, we additionally have to show the invariant entails our desired result, v ≤ v. This can be shown with a standard monotonicity property of modal logics: from φ ψ and Γ [α]φ, we can conclude Γ [α]ψ, where φ states the expression above is an invariant and the velocities are always greater than their initial value, and ψ is our goal: v ≤ v.

Collision Speed with Different Kinds of Friction

Here we continue Example 11, where we consider two dynamics δ

F ≡ ( ẋ = v, v = -v 2 ) and δ F ≡ ( ẋ = v, v = -v). Our goal is Γ F [δ F ; δ F ](x = x = l ⇒ v ≤ v), with Γ F := {x = x = 0, 0 < v ≤ v ≤ 1}.
First, we establish the fact that the objects in this example always have positive velocity. We show this by the (Dbx) rule (Definition 13), where

L δ F v = -v 2 and L δ F v = -v.
This allows us to infer v > 0 and v > 0 hold at all times.

We apply the (Sync) rule along x = x, yielding the synchronized dynamics

ẋ = v, v = -v 2 , ẋ = v •(v/v), v = -v • (v/v) & v > 0 ∧ v > 0
Note that the new evolution domain condition v > 0 allows us to rewrite v • (v/v) to v. The synchronizability conditions follow immediately from the fact that v > 0 and v > 0. For the synchronized formula, we apply the (DI) rule, so the desired inequality v ≥ v is reduced to v 2 ≤ v, that is, v ≤ 1. To this end, v > 0 tells us that the derivative of v, that is, -v 2 , is always negative, therefore v ≤ 1.

Model Refinement

In this example, we consider two abstract models of cars. The first car is able to provide a high amount of constant acceleration a at low velocities, but at a certain velocity v cut the engine switches to a different mode and then provides a lesser, but still constant acceleration a cut . The second car is an abstracted version of the first, which ignores this mode change and provides the same constant amount of acceleration a at all velocities. Our aim in this example is to establish a safety envelope around the first car's behavior using the more simply stated second car's dynamics. Hence we show that the second car's velocity is greater than the first's at any position x = x = l.

More formally, the behavior of the first car is expressed as a hybrid program α := (δ 1 ; ?v = v cut ; δ 2 ) with two modes: δ 1 := ( ẋ = v, v = a & v ≤ v cut ) and δ 2 := ( ẋ = v, v = a cut ). The second car follows the simple dynamics δ := ( ẋ = v, v = a).

Our goal is to prove the sequent

Γ α; δ (x = x = l ⇒ v ≤ v),
where the initial conditions are given by Γ := (x = x = 0, 0

< v = v = v 0 , 0 < v cut , 0 < a cut ≤ a).
Technically, the (Sync) rule merges one differential dynamics with another, but the program the first car executes is a more complicated composition of dynamics and testing. However, it is possible to synchronize piecewise, first synchronizing δ with δ 1 until the first car changes modes, then synchronizing δ with δ 2 for the remainder of their runs. This slightly generalized synchronization procedure means we can instead show

Γ δ 1 ⊗ (x,x) δ; ?v = v cut ; δ 2 ⊗ (x,x) δ (x = x = l ⇒ v ≤ v)
There are also now two sets of synchronizability conditions to satisfy, but both are again straightforward. Since δ 1 and δ are nearly identical (except for the evolution domain constraint), their synchronization δ 1 ⊗ (x,x) δ basically identifies the two dynamics. The synchronization of δ 2 and δ is exactly the synchronization performed above in Section 6.1, and proceeds in the same way.

Conclusions and Future Work

In this paper, we presented a relational extension of the differential dynamic logic based on time stretching of dynamics. This reparametrization enables us to enforce comparisons between two systems occur when certain conditions are satisfied, such as ensuring that two cars are compared when they are passing through the same position. Reparametrization can be thought of as stretching or compressing time for one of the dynamics, but we have also shown this transformation can be effected by a transformation of the dynamics themselves based on Lie derivatives, which we call synchronizing the dynamics (Definition 19). This led us to a new dL proof rule, the (Sync) rule (Theorem 24). We then implemented this rule in the KeYmaera X tool, and used our extension to demonstrate several nontrivial relational properties of dynamical systems.

In the future, we think it would be interesting to combine our relational logic with orthogonal relational extensions of dL [START_REF] Loos | Differential refinement logic[END_REF] which focus on refinement relations with varying levels of nondeterminism. We also hinted in our last case study that it is possible to synchronize wider classes of hybrid programs than just two differential dynamics. We also think that the level of automated proof search available in KeYmaera X may enable the automatic detection of monotonic properties in product lines. This may be useful in industry both to provide sanity checks on formalized models of products, as well as enabling strong guarantees to be more easily obtained for those models.

Fig. 1 .

 1 Fig. 1. An ad-hoc proof for Example 1

  α 2 → where ; denotes relation composition, and 6.α * →= (-α →) * where * denotes the reflexive transitive closure.

This analogy is not perfect: a typical while loop can only exit when its guard is false, whereas a hybrid program can exit the differential dynamics while Q is satisfied.

It is easy to see that the derivative of a term t ∈ T (V) with respect to x ∈ V can be given as a dL term ∂ ∂x e ∈ T (V) such that ∂ ∂x e = ∂ ∂x e . The definition of ∂ ∂x e is inductive with respect to the term e.


D Tournier
email: tournier@cnm.es

Ph Godignon

J Montserrat

D Planson

C Raynaud

J P Chante

F Sarrus

C Bonhomme

J F De Palma

Characterization of a 4H-SiC High Power Density Controlled Current Limiter

Keywords: Current limiter, JFET, serial protection device, high voltage, electrical characterization

Critical steps for the fabrication of SiC devices are thermal annealing and metal ohmic contact formation. Metal annealing effect on the electrical characteristics of the current limiter underlines the necessity to control this device fabrication step. Measurements of contact resistivity as a function of temperature demonstrate the stability of the N type Ni/SiC contact in the range of 175 K -450 K as its value remains constant around 40 µΩ.cm 2 . Post implantation annealing effect on the sheet resistance (Rsh) shows that a 1700°C/30 min annealing gives better trade off in terms of dopant activation and surface roughness. High power density has been measured up to 600 V. Current thermal stability has been measured for an applied drain to source voltage of 100 V and exhibits high power density capabilities of SiC VJFET as a controlled current limiter.

Introduction.

Considering fault current limiters for serial protection, a lot of structures exist, from regulation to other complex systems such as circuit breakers, mechanical switches or more conventional fuses. Up to now, only few silicon [START_REF] Sze | Physics of semiconductors[END_REF][START_REF]Current Regulative Diode distributor[END_REF] or silicon carbide [START_REF] Siemens Corp | Current limiter circuit[END_REF][START_REF] Nallet | Electrical and Electrothermal 2D simulation of a 4H-SiC High Voltage Current limiting Device for serial protection application[END_REF] semiconductor current limiter structures were described in papers. This device was designed for serial circuit protection in order to limit I²t value. Although SiC semiconductor based devices are very suitable for high current and high voltage systems [START_REF] Sugawara | 12 19kV 4H-SiC pin Diodes with Low Power Loss[END_REF][START_REF] Matsunami | Progress in Wide Bandgap Semiconductor SiC for Power Devices[END_REF], a promising application of SiC-based devices are the fault current limiters for power system protection, which benefit from its high thermal conductivity (l = 4.9 W×cm -1 ×K -1 ) and wide band gap energy (E g = 3 eV). This work is devoted to the design, fabrication and characterization of a new etched VJFET [START_REF][END_REF], which implements both gate and source in buried layers. As in steady state the voltage drop across the component must be as low as possible, in the active state (limiting phase) a current limiter must sustain a high current, under high voltage bias. The resulting high power density must not cause the failure of the component. In this paper, ohmic contact formation and their thermal stability are presented. Then the device thermal stability under constant voltage is shown.

4H-SiC VJFET contact characterization

The key parameter for high power devices is ohmic contact formation in order to reach high current densities using silicon carbide. The dependence of VJFET channel specific resistance on metal annealing temperature is presented in Figure 1. A value of 120 mW.cm² is reached for 950°C metal annealing condition, close to the value of 90 mW.cm² expected from simulations.

(T ) = µ 0 T T 0 ⎛ ⎝ ⎜ ⎞ ⎠ ⎟ -α ⎡ ⎣ ⎢ ⎢ ⎤ ⎦ ⎥ ⎥
. Coefficient variation extracted from R sh measurement (made on TLM) gives a coefficient α=1,54. This low value compared to the value of 2 generally found [START_REF] Ruff | SiC devices: Physics and Numerical Simulation[END_REF] may be due to the presence of defects or to the effective mass dependence on temperature. Two post implantation thermal annealing conditions have been investigated. Considering R sh measurement (Table 1), a 1700°C / 30 min post implantation annealing leads to the best results (in term of electrical activation and global process cost). The roughness is the same for both conditions tested.

Tab. 1. R sh for two post implantation annealing setup

Considering previous results, we can consider that ohmic contacts for N-type layer are good and thermally stable in the range of temperature from 200 K to 450 K. The temperature was limited to 450 K, the highest temperature reached by the VJFET during the limiting state (estimated by simulation).

VJFET power capability analyses.

Using VJFET as a current limiter for high voltage application involves high power density in the device. Self heating effect is important as the carrier mobility of electrons (i.e. the current) strongly depends on temperature).

(a) (b) Fig. 4. VJFET thermal characterization: I(V) (a) and specific resistance (b)

The variation of the specific channel resistance ρch with temperature is extracted from I-V pulsed measurements between VJFET drain-to-source (Figure 4(a)), at VDS = 2 V, for temperature varying from 200 K up to 550 K. As ρch is directly proportional to µn, the coefficient α was extracted. The obtained value (α = 2.04) presents a good agreement with parameter used is simulation as illustrated in figure 4(b). Current time dependence measurements underline thermal capabilities of the VJFET as presented in Figure 5. The current was normalized to the current I0 at t = 0 s for several voltages (VDS). Current stabilization shows the ability of VJFET to sustain short circuit current for long time.

Considering for example a voltage VDS = 100 V, current reduction due to self heating is around 12% and current remains constant during more than 100 s.

Fig.5. VJFET current time dependence under constant Drain to Source bias

Repetitive measurements were done and no degradation of the electrical characteristics has been noticed. Highest breakdown in "current limiting state" for 0.5 s pulsed mode bias was measured to be around to 811 V, corresponding to a high power density of 140 kW/cm 2 .

Conclusion:

This work underlines the fabrication requirement of good ohmic for high power density device. Both lowest value and thermal stability versus temperature is needed. Temperature measurements exhibit ohmic contact stability from 200K up to 450K. A post implantation thermal annealing and metal process have been setup and lead to optimistic results for the fabrication of higher capabilities devices (a rising up in terms of cells current). This device could be used in application such as current limitation in case of a short circuit of an electrical system. It could permit an elevation of the current ratings of classical mechanical switch with the serial addition of this controlled device.

Fig 1 .Fig. 3 .

 13 Fig 1. Ohmic contact formation (a) and specific resistance variation (b)for different metal annealing temperature

Acknowledgment.

We would like to thank Ferraz-Shawmut Company for their financial support of this work and the European Community for the Access to Research Infrastructure action of the improving Human Potential Program. The realization of this device has been achieved at the CNM (Barcelona).


Stefan Knecht
email: stefan.knecht@phys.chem.ethz.ch

Hans Jørgen

Aagaard Jensen

Trond Saue

Relativistic quantum chemical calculations show that the

come

Understanding the nature of a chemical bond [START_REF] Lewis | The atom and the molecule[END_REF] and how it relates to the chemical reactivity of a molecule is of central interest in chemistry. Despite recent efforts, [START_REF] Neidig | Covalency in f-element complexes[END_REF][START_REF] Kaltsoyannis | Chemical bonding of lanthanides and actinides[END_REF][START_REF] Cary | Emergence of californium as the second transitional element in the actinide series[END_REF][START_REF] Ferrier | Spectroscopic and computational investigation of actinium coordination chemistry[END_REF][START_REF] Dutkiewicz | Reduction chemistry of neptunium cyclopentadienide complexes: from structure to understanding[END_REF][START_REF] Windorff | Identification of the formal +2 oxidation state of plutonium: synthesis and characterization of {Pu II [C 5 H 3 (SiMe 3 ) 2 ] 3 }[END_REF][START_REF] Jung | Ab initio ligand-field theory analysis and covalency trends in actinide and lanthanide free ions and octahedral complexes[END_REF][START_REF] Cross | Covalency in americium(III) hexachloride[END_REF][START_REF] Formanuik | Actinide covalency measured by pulsed electron paramagnetic resonance spectroscopy[END_REF][START_REF] Vitova | The role of the 5f valence orbitals of early actinides in chemical bonding[END_REF][START_REF] Wilson | Protactinium and the intersection of actinide and transition metal chemistry[END_REF] insight into the bonding of the 5f elements is still limited, in particular with respect to a basic understanding of which atomic orbitals contribute and the degree of covalency in actinide-ligand bonding. [START_REF] Editorial | The bottom line[END_REF] Concerning the most prominent 5f element uranium, [START_REF] Monreal | The riches of uranium[END_REF] recent works have explored the nature of supported U-U [START_REF] Li Manni | Assessing metal-metal multiple bonds in Cr-Cr, Mo-Mo, and W-W compounds and a hypothetical U-U compound: A quantum chemical study comparing DFT and multireference methods[END_REF][START_REF] Penchoff | Metal-metal bonding in the actinide elements: Conceptual synthesis of a pure two-electron U-U f δ single bond in a constrained geometry of U 2 (OH) 10[END_REF][START_REF] Foroutan-Nejad | Unwilling U-U bonding in U 2 @C 80 : cage-driven metal-metal bonds in di-uranium fullerenes[END_REF][START_REF] Qu | Metal-metal multiple bond in low-valent diuranium porphyrazines and its correlation with metal oxidation state: A relativistic DFT study[END_REF][START_REF] Zhang | U 2 @I h (7)-C 80 : Crystallographic characterization of a long-sought dimetallic actinide endohedral fullerene[END_REF][START_REF] Scheibe | The [U 2 F 12 ] 2anion of Sr[U 2 F 12[END_REF] as well as uranium-ligand (multiple) bonds [START_REF] Lyon | Formation of unprecedented actinide≡carbon triple bonds in uranium methylidyne molecules[END_REF][START_REF] Hu | On the maximum bond multiplicity of carbon: unusual C-U quadruple bonding in molecular CUO[END_REF][START_REF] Hayton | Recent developments in actinide-ligand multiple bonding[END_REF][START_REF] Hlina | Metal-metal bonding in uranium-group 10 complexes[END_REF][START_REF] Ephritikhine | Molecular actinide compounds with soft chalcogen ligands[END_REF] and their implications on the physical and chemical properties of the corresponding complexes. [START_REF] Fox | Towards uranium catalysts[END_REF][START_REF] Liddle | The renaissance of non-aqueous uranium chemistry[END_REF][START_REF] Halter | Uranium-mediated electrocatalytic dihydrogen production from water[END_REF][START_REF] Arnold | Carbon oxygenate transformations by actinide compounds and catalysts[END_REF] In contrast, still today comparatively little is known about the chemical bonding in the fundamental, naked diuranium molecule U 2 [START_REF] Bursten | Xα-SW calculations for naked actinide dimers: on the existence of φ bonds between metal atoms[END_REF][START_REF] Pepper | Ab initio studies of the electronic structure of the diuranium molecule[END_REF][32][START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] which was experimentally first observed in the early 1970s. [START_REF] Gorokhov | Mass-spectroscopic investigation of stability of gaseous U 2 O 2 and U 2[END_REF] In 2005 Laura Gagliardi and Björn Roos presented a computational study which concluded that diuranium is a stable molecule with a very complicated bonding pattern, featuring all known covalent bonding types and leading to a quintuple bond. 32 Although their study did include relativistic effects, Gagliardi and Roos did not fully explore the effect of spin-orbit (SO) interaction on the nature of the ground state and bonding.

What makes the early actinides and in particular uranium so unique within the periodic table of elements is the extended set of valence electronic shells that are available for bonding. The key valence atomic orbitals (AOs) of uranium are the seven 5f , the five 6d and the 7s orbitals which are all (partially) occupied in the ground state [Rn]5f 3 6d 1 7s 2 electronic configuration of the U atom. However, as illustrated by Fig. 1, the availability of the 5f orbitals and an increased availability of the 6d orbitals for bonding is very much a relativistic effect. Two kinds of relativistic effects are commonly distinguished, [START_REF] Pyykkö | Relativity and the periodic system of elements[END_REF][START_REF] Reiher | Relativistic quantum chemistry: the fundamental theory of molecular science[END_REF][START_REF] Dyall | Introduction to Relativistic Quantum Chemistry[END_REF] namely scalar-relativistic effects and SO interaction. The former arises from the high speed and associated relativistic mass increase of electrons in the vicinity of heavy nuclei, whereas the latter originates from the interaction of electron spin with the magnetic field induced by charged particles (nuclei and other electrons) in relative motion and leads to a coupling of spin and spatial degrees of freedom. [START_REF] Saue | Relativistic Hamiltonians for chemistry: a primer[END_REF] Both relativistic effects profoundly modify energetics (see Figure 1) and the spatial extent of AOs and hence molecular bonding and structure, [START_REF] Dyall | Introduction to Relativistic Quantum Chemistry[END_REF] with spin-orbit effects becoming particularly noticeable from sixth-row elements and onwards due to second-order effects (orbital relaxation). [START_REF] Christiansen | Electronic structure and dissociation curves for the ground states of Tl 2 and Tl + 2 from relativistic effective potential calculations[END_REF][START_REF] Saue | Relativistic effects on the bonding of heavy and superheavy hydrogen halides[END_REF] As summarized in Supplementary Table 1, the spatial extent of the frontier AOs -measured by the root-mean-square (rms) radius of the associated radial function -is, similar to the energetic considerations above, subject to distinct relativistic effects. Scalar-relativistic effects are most pronounced, leading to an increase of the rms values for the 5f (6d) orbitals by 15% (14%), thus allowing for better spatial overlap upon bond formation in the molecule, in particular since the 7s undergoes a significant contraction with inclusion of scalar-relativistic effects, as underlined by a decrease in the rms value by 14%. SO effects then further increase/decrease the rms radii of the radial functions for the spin-orbit split 6d and 5f orbitals by approximately ±2%.

In their seminal work, Gagliardi and Roos 32 presented the first computational evidence that U 2 is a stable molecule with a binding energy of 40.2 kcal/mol at the scalar-relativistic 2nd-order complete active space perturbation theory (CASPT2) level, being reduced to 30.5 kcal/mol upon the perturbative inclusion of SO interaction. Interestingly, a promotion energy of 17.9 kcal/mol is required per atom to go from the 5f 3 6d 1 7s 2 5 L 6 ground state to the excited 5f 3 6d 2 7s 1 7 M 6 state, [START_REF] Blaise | Selected constants energy levels and atomic spectra of actinides[END_REF] the lowest excited level with unpaired 7s electrons, thus making 7s available for bonding and avoiding Pauli repulsion between closed 7s shells. Excitations out of the 5f orbitals takes considerably more energy; the first such state, a 5f 2 6d 2 7s 2 5 L 6 state, lies 32.9 kcal/mol above the atomic ground state. The calculated binding energies for U 2 may be compared to the much larger energy of 52±5 kcal/mol obtained from experimental mass spectrometry data. [START_REF] Gorokhov | Mass-spectroscopic investigation of stability of gaseous U 2 O 2 and U 2[END_REF] However, the experiment was carried out at high temperature (2500 -2700 • C) and the dissociation energy was extracted assuming an equilibrium U-U internuclear distance of R e = 3.0 Å and a vibrational

frequency ω e = 100 cm -1 , leading the authors themselves to suggest that their value is somewhat overestimated.

In their first paper, Gagliardi and Roos report a spin-free electronic ground state [START_REF] Windorff | Identification of the formal +2 oxidation state of plutonium: synthesis and characterization of {Pu II [C 5 H 3 (SiMe 3 ) 2 ] 3 }[END_REF] O g , which corresponds to a septet state (S = 3) with projection Λ = 11 of the total electronic angular momentum on the internuclear axis, and suggest that the Ω = 14 component will be the ground state upon inclusion of SO coupling. However, in a subsequent publication an excited state of Ω = 9 g (Λ = 12) was reported a mere 80 cm -1 above a Ω = 8 g (Λ = 11)

ground state, such that it was not possible to unequivocally determine the ground state of U 2 . [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] Note that the main text of Ref. 33 reports on page 17004 the calculated first excited state as Ω = 8 g (Λ = 12) but we base our designation Ω = 9 g (Λ = 12) on Table 6 in the same paper. The bonding picture in the electronic ground state as determined from their scalar-relativistic complete-active space self-consistent field (CASSCF) calculations 32,33 can be summarized as follows: Three "normal" two-electron two-center bonds, one of σ g and two of π u symmetry, are formed with predominant 7s and 6d atomic character, respectively, together with four one-electron two-center bonds, of symmetries σ g , π u , and δ g (2) comprising contributions from 6d and 5f AOs. In addition, two ferromagnetically coupled 5f φ -electrons are localized in nonbonding molecular orbitals (MOs)

on each U center. Interestingly, exchange stabilization effects arising from interactions of the localized 5f φ -electrons with the one-electron bonds are found to exceed the energetic benefits of an antiferromagnetically coupling of the localized 5f φ -electrons. The proposed bonding picture in U 2 corresponds undoubtedly to one of the most complex electronic structures hitherto known for any two atoms in a molecule.

Discussing chemical bonding in U 2 requires the definition of an intuitive and stable measure that allows us to characterize possible multiple bonds in a distinct manner. Many such quantities to describe a chemical bond exist and have been applied to explorations of the chemical bonding in f -element complexes, see for example Ref. 3. One such scheme is based on the concept of bond order, defined as half the difference between the number of bonding and anti-bonding electrons in a molecule [START_REF] Herzberg | Zum Aufbau der zweiatomigen Moleküle[END_REF] . It was extended to multiconfigurational wave functions by Roos and co-workers 32,33,43 through the introduction of an effective bond order (EBO)

EBO = 1 2 p η bp -η abp , (1)
based on the occupation numbers η of bonding (b) and anti-bonding (ab) natural orbitals (NOs). Equation ( 1) allows for fractional bond orders as the orbital contributions per bond in general will be non-integer. Hence, the multiplicity of a bond is best determined by the lowest integer value larger than the EBO. [START_REF] Roos | Reaching the maximum multiplicity of the covalent chemical bond[END_REF] In the case of U 2 , an EBO of 4.2 was obtained and interpreted as a quintuple bond. [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] Such a translation of an EBO into integer bond multiplicity remains subject to debate as a recent discussion of the bond order in C 2 clearly illustrates, see for example Refs. 44 and 45 and references therein.

It is known that not only scalar-relativistic effects, but also SO interactions are expected to strongly influence the chemical bonding and reactivity in heavy-element containing molecular systems. [START_REF] Schwerdtfeger | Relativity and chemical bonding[END_REF] Recent examples include mercury-47 and gold-catalyzed [START_REF] Gaggioli | Dioxygen insertion into the gold(I)-hydride bond: spin orbit coupling effects in the spotlight for oxidative addition[END_REF] reactions where significant SO coupling effects make accessible catalytic pathways which would otherwise be closed for energetic and/or symmetry reasons. Given the complex nature of the chemical bond in U 2 , obvious questions that remain are: (i) Whether a variational inclusion of SO interaction in the wave function optimization could lead to a change of the bonding picture, i.e., is the U-U bond a quintuple bond or not? (ii)

What is the impact of the SO interaction on the nature of the electronic ground state?

A detailed understanding of the electronic structure and the chemical bond in U 2 will be helpful to gain further insight into the chemical bonding properties of the 5f -elements, and in particular the role of SO interaction. To address these questions, we carried out multiconfigurational CASSCF with the same active space as in Refs. 32 and 33 as well as extended restricted active space (RASSCF) calculations with a variational inclusion of scalar-relativistic effects and SO interaction, using the exact 2-component Hamiltionian (X2C) framework in the Dirac program package [START_REF] Dirac | a relativistic ab initio electronic structure program, Release DIRAC17[END_REF] (see Supplementary Information for computational details). It is worthwhile to note that our RAS model comprises the full set of valence molecular orbitals arising from the 5f , 6d and 7s manifold of each uranium atom. In addition to the CAS model, it includes all excitations from the strongly bonding σ g and π u orbitals into the anti-bonding σ * u and π * g orbitals (scalar-relativistic notation) plus singles-doubles to the CAS model space for a partial description of dynamic correlation. The RAS model can correctly describe the atomic states at dissociation. Supplementary Figure 1 summarizes both active space models in terms of the actual, considered valence orbitals. By comparison with the corresponding scalar-relativistic CASSCF data reported previously 32,33 differences in the bonding picture of U 2 can unambiguously be ascribed to a variational account of SO interaction.

RESULTS AND DISCUSSIONS Effective bond order: generalization

The calculation of the EBO (cf. equation ( 1)) hinges on being able to distinguish bonding, anti-bonding and non-bonding orbitals. Without variational account of SO interaction bonding and anti-bonding MOs are easily identified from symmetry in a homonuclear dimer such as U 2 , as illustrated on the left-hand side in Supplementary Fig. 3. Upon in-clusion of SO interaction bonding and anti-bonding orbitals will mix [START_REF] Balasubramanian | Relativity and chemical bonding[END_REF] , as shown on the right-hand side in Supplementary Fig. 3. For instance, the bonding spin orbital σ g α and anti-bonding π g β may mix, since they have the same value m j of the projection of total angular momentum on the internuclear axis. This makes a definite characterization of a given MO as bonding or anti-bonding impossible. Obviously the same considerations hold for NOs. Maurice et al. noted that an alternative to equation ( 1) is to multiply the bond order of individual spin-free configuration state functions (or determinants), obtained by simple counting of bonding and anti-bonding orbitals, by their weight in the total wave function [START_REF] Maurice | Effective bond orders from two-step spin-orbit coupling approaches: the I 2 , At 2 , IO + , and AtO + case studies[END_REF] . This allowed them to extend the definition of EBO to multireference calculations starting from a set of molecular orbitals optimized at the scalar relativistic level and with SO interaction only added at the correlated level. Since SO interaction in our case is also present in the orbital optimization step a further generalization of the EBO is required. Hence, we propose a generalized EBO (gEBO),

gEBO = 1 2 p η p (w b -w ab ) , (2)
where we introduced the difference of the weights w b and w ab of the bonding and antibonding contribution to the p-th NO, respectively, to be multiplied with the occupation number η p . Without SO coupling the weights are either zero or one and equation (2) reduces to the EBO definition given in equation (1).

Nature of low-lying electronic states

In Fig. 2, we present our calculated CASSCF potential energy curves for the lowest electronic states of U 2 around the equilibrium structure. The inset in Fig. 2 focuses on internuclear U-U distances near the equilibrium of the lowest three electronic states obtained with a larger basis set (dyall.cv3z). These electronic states have term symbols Ω = 9 g , 8 g , and 7 g (Hund's case (c)) with Ω = 9 g being the lowest state, separated by approximately 2200 cm -1 from the first two excited Ω = 8 g and Ω = 7 g states. Its calculated equilibrium distance and harmonic vibrational frequency are R e = 2.57 Å

and ω e = 190 cm -1 , respectively. Inclusion of more dynamic electron correlation through RASSCF calculations (see Supplementary Fig. 2) confirmed the Ω = 9 g state as electronic ground state of U 2 . Compared to the CASSCF data, the spectroscopic constants change very little (∆R e = -0.01 Å and ∆ω e = -4 cm -1 ). In contrast, the Ω = 8 g state, which was reported as electronic ground state in previous works 32, [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] , comes out as a low-lying excited state about 3500 cm -1 (2200 cm -1 ) vertically above the Ω = 9 g state, according

to our RASSCF (CASSCF) calculations. Moreover, from the RASSCF data we calculated a dissociation energy of 21.0 kcal/mol from the Ω = 9 g state to two separated U atoms.

Although being approximately 10 kcal/mol lower than the corresponding ground-state bond energy obtained from SO CASPT2 calculations 32 , this result still supports a bound U 2 molecule with a sizable bond energy. It should be noted that, in contrast to the SO CASPT2 approach, our RASSCF model only partially takes into account dynamical electron correlation effects, which could to a large extent explain the observed discrepancy in the dissociation energy.

Bonding in U 2

An analysis of the electronic configuration of the excited Ω = 8 g state (see Table 1) shows excellent agreement with the corresponding data for the spin-free 7 O g ground state reported in Refs. 32 and 33. As discussed by the latter authors, the 7 O g spin-free state is the main component of their SO coupled Ω = 8 g state. Our analysis in Table 1 confirms that the chemical bond in the Ω = 8 g state can be regarded as consisting of four (weak) one-electron two-center bonds with contributions from 6d and 5f AOs as well as two non-bonding 5f MOs 32 . The reorganization of the electronic valence configuration of each U atom in the molecule is shown by the Mulliken atomic orbital populations given in Supplementary Table 2. Each U atom has a 7s population around 1.0 and a 6d population somewhat above 2.5, suggesting the 7s → 6d promotion discussed above. By contrast, each U atom retains to a large extent its atomic 5f 3 ground state occupation such that any 5f → 7s promotion is modest, as would be expected from a consideration of promotion energies (cf. Ref. 33).

The Mulliken atomic orbital populations per U atom for the Ω = 9 g ground state are qualitatively similar to those of the Ω = 8 g excited state. In contrast, the NO occupation numbers listed in Table 1 reveal a notable difference between the electronic configurations of these states. Irrespective of the active space models, distinctive features of the Ω = 9 g state in comparison to the Ω = 8 g state are its singly occupied orbitals of predominantly 5f δ -type and empty orbitals with mainly 5f π -character, originating from distinctively different leading determinants at the spin-free level. Table 2 summarizes the decomposition of the exact total angular momentum Ω on the internuclear axis into its averaged angular momentum Λ and spin momentum Σ contributions (see Supplementary Information for computational definitions). Considering first the Ω = 8 g state, we note that the spin projection expectation value Σ for either active space model --2.51 (-2.60) for CASSCF (RASSCF) -is non-integer and close to halfway between the possible non-or scalarrelativistic integer values (in absolute terms) of two and three. For the Ω = 9 g state, we observe a decrease of the total spin projection Σ to -2.67 (-2.79) for the CASSCF (RASSCF) active space model. These non-integer values are consistent with a mixing of spin-free states with M S =-2 and M S =-3 both originating from septet (S=3) states, or, alternatively, with a mixing of quintet and septet spin-free states. The latter case would imply that SO coupling reduces the ferromagnetic character of the coupling of the six unpaired electrons in both states [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] . We can, however, not provide a sound confirmation of this since our calculations do not contain intermediate spin-free states. Interestingly, a full antiferromagnetic coupling of the unpaired electrons was reported for the electronic ground state configuration of metastable U 2+ 2 . [START_REF] Gagliardi | A very short uranium-uranium bond: the predicted metastable U 2+ 2[END_REF] We have confirmed this picture in U 2+ 2 for our Ω = 1 g ground (Σ = -0.08) and Ω = 0 + g (Σ = 0.00) excited states whereas other electronically excited states shown in Supplementary Fig. 5 with Ω > 1 exhibit larger departures from integer Σ values.

In Table 2 we also report gEBOs for the Ω = 9 g and Ω = 8 g states obtained according to equation (2). They are lower than four for either electronic state (and active orbital space model employed) at their respective equilibrium structures with a common lowering of the gEBO by approximately 0.1 in going from our CAS-to RASSCF active orbital space model. These findings strongly suggest the presence of a quadruple rather than the quintuple bond proposed in previous works 32, [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] . As shown in Supplementary Fig. 4, these conclusions even hold for a larger range of U-U distances, thus a change in bond lengths by full account of dynamic correlations will not change the conclusions.

CONCLUSIONS

We have calculated and characterized the low-lying electronic spectrum of U 2 by means of a genuine relativistic multiconfigurational quantum chemical approach with full variational inclusion of spin-orbit effects. In summary, our best calculations predict an Ω = 9 g ground state separated by 3500 cm -1 from the first excited state, which we identified as an Ω = 8 g state, which is the lowest in a manifold of many low-lying excited states, as illustrated in Fig. 2. Furthermore, the ground state is predicted to have an equilibrium distance of R e = 2.56 Å, a harmonic vibrational frequency of ω e = 186 cm -1 , and a dissociation energy of D e > 21 kcal/mol.

Our calculated data reveal essential differences compared to previous calculations in the description of the complex electronic structure of U 2 , differences that ultimately call for a revision of the proposed chemical bond picture for the U 2 ground state established in previous works 32,33 : (i) the electronic ground state has term symbol Ω = 9 g and is characterized by a generalized effective bond order of 3.8 which translates into a quadruple bond. (ii) The Ω = 8 g state which was proposed to be the electronic ground state of U 2 with an effective bond order of 4.2 (corresponding to a quintuple bond) 32,33 is in fact a low-lying electronically excited state with a quadruple bond (generalized effective bond order of 3.9) at its equilibrium structure. Our analysis shows that the chemical bond in the Ω = 9 g electronic ground state consists of three electron-pair bonds, one σand two π-bonds, two one-electron bonds of approximate σ-and δ-type as well as four predominantly ferromagnetically coupled 5f electrons localized on one U atom each. This distinctly simplifies not only the originally proposed bonding picture 32 but also emphasizes the value of a genuine relativistic multiconfigurational electron correlation approach that facilitates an unambiguous prediction of the electronic structure and molecular properties of molecules containing heavy elements such as uranium. of uranium, 5f , 6d and 7s orbitals are (partially) occupied in the electronic ground-state configuration. Relativistic effects are substantial for the heavy element U, leading to an energetic reordering of the 7s (red lines) and 6d shells (blue lines) while bringing the 5f shell (green lines) energetically closer to the remaining valence shells. The importance of spin-orbit coupling is readily seen by the notable energetic splitting of the valence orbitals with angular momentum number l > 0, i.e., the 5f and 6d orbitals, leading to their increased availability for bonding.

Orbital energies were obtained from atomic average-of-configuration Hartree-Fock calculations (see Supplementary Information for further computational details). [START_REF] Dyall | Relativistic double-zeta, triple-zeta, and quadruple-zeta basis sets for the actinides Ac-Lr[END_REF] with identical color and symbol codes for the electronic states as in the main figure. The lowest-lying electronic states have term symbols Ω = 9 g (red circles), 8 g (green circles), and 7 g (purple circles) (term designation in accordance with Hund's case (c)). In both cases, Ω = 9 g is the lowest state with a notable vertical separation of more than 2000 cm -1 from the remaining states. The Ω = 8 g state, reported as electronic ground state in previous works 32, [START_REF] Roos | Exploring the actinide-actinide bond: theoretical studies of the chemical bond in Ac 2 , Th 2 , Pa 2 , and U 2[END_REF] , is found to be among the first excited states. Electronic states with an Ω quantum number lower than 7 and those with ungerade inversion symmetry are even higher-lying in energy in comparison to the Ω = 9 g state. An exception is the Ω = 7 u state which becomes the lowest-lying excited state at larger U-U internuclear distances. Absolute energies are reported with an offset of -56075 Hartree.

Figure 1 .

 1 Figure 1. Frontier atomic valence orbital energies of uranium in nonrelativistic (left), scalarrelativistic (middle), and fully relativistic (right) molecular orbital theories. All valence orbitals

Figure 2 .

 2 Figure 2. CASSCF potential energy curves for the lowest electronic states of U 2 around the equilibrium structure calculated with the uncontracted [26s21p17d12f 3g] deJong+3g basis set 53 . The inset shows the CASSCF potential energy curves for the first three electronic states of U 2 around the equilibrium structure calculated with the uncontracted [33s29p20d15f 6g2h] dyall.cv3z basis set 54 with identical color and symbol codes for the electronic states as in the main figure. The

Acknowledgements

We thank the Danish Center for Scientific Computing for ample computational resources. We thank Trygve Helgaker and Einar Uggerud (U Oslo) for help with Ref. 34.

We thank Camilla Kottum Elmar for preparing the graphical abstract. SK acknowledges fruitful discussions with Pekka Pyykkö (U Helsinki) on numerous occasions. SK thanks Markus Reiher (ETH Zürich) for his continuous support. We dedicate this paper to the memory of Björn Roos, an outstanding quantum chemist.

Data availability

Supplementary information is available as a separate file. All relevant data that are not included in this Article and its Supplementary Information are available from the corresponding author upon reasonable request.

Author contributions

SK ran all calculations reported in this paper, whereas the interpretation of results as well as preparation of the manuscript was a joint effort by all three authors. The generalized effective bond order (equation ( 2)) was developed by SK and TS.

Competing interests

The authors declare no competing financial interests.

Tables Table 1. Electronic configurations for U 2 in different electronic states at their respective equilibrium structure. For the relativistic results including spin-orbit coupling, the natural orbitals are labeled according to their main scalar-relativistic character which eases comparison with the reference data of Ref. 32. Natural orbitals with occupancies higher than 0.1 in all configurations are listed.