Vassil Todorov

Safouan Taha

Frédéric Boulanger

Armando Hernandez

Improved invariant generation for industrial software model checking of time properties

Keywords: Software verification, Formal methods, Model checking, SMT solving, Invariant generation, Time properties

Modern automotive embedded software is mostly designed using model-based design tools such as Simulink or SCADE, and source code is generated automatically from the models. Formal proof using symbolic model checking has been integrated in these tools and can provide a higher assurance by proving safety-critical properties. Our experience shows that proving properties involving time is rather challenging when they involve long durations and timers. These properties are generally not inductive and even advanced techniques such as PDR/IC3 are unable to handle them on production models in reasonable time.

In this paper, we first present our industrial use case and comment on the results obtained with the existing model checkers. Then we present our invariant generator and methodology for selecting invariants according to physical dimensions. They enable the proof of properties with long-running timers. Finally, we discuss their implementation and benchmarks.

I. INTRODUCTION AND MOTIVATION

Model-based design tools such as Simulink or SCADE are massively used in today's automotive embedded software design. These tools provide a higher level of abstraction compared to implementation code, and losen the coupling between system and software design. In the near future, with the advent of autonomous vehicles, car manufacturers could be asked to provide more guarantees and confidence to those systems by demonstrating the correctness of the software, at least for the safety-critical part. Actually, in industries such as aviation and railway, these guarantees are achieved by obtaining a certificate from a certification authority claiming that the software is safe (aviation) or that it is compliant with the safety standard of the domain (railway). For some use cases, it is possible to use formal methods for certification. For example, Airbus illustrates the use of Deductive Proof and Abstract Interpretation tools in [START_REF] Souyris | Formal Verification of Avionics Software Products[END_REF]. Industrial experiments were done by the Ariane group in [START_REF] Bouissou | Space Software Validation using Abstract Interpretation[END_REF], by Dassault Aviation in [START_REF] Moy | Testing or Formal Verification: DO-178c Alternatives and Industrial Experience[END_REF], by Rockwell Collins in [START_REF] Cofer | Formal Methods Case Studies for DO-333[END_REF] and by other companies. Formal methods such as the B Method and Model Checking are used by some railway companies, and use cases are presented in [START_REF] Behm | Météor: A Successful Application of B in a Large Project[END_REF] and [START_REF] Petit-Doche | Formal Verification of Industrial Critical Software[END_REF].

In a previous paper [START_REF] Todorov | Formal Verification of Automotive Embedded Software[END_REF], we shared our experience about applying tools that use formal methods (Abstract Interpretation, SMT-based Model Checking and Deductive Proof) on industrial software. As we are interested in automatic verification of safety properties, we will focus on SMT-based Model checking. Abstract Interpretation is well adapted for proving the absence of runtime errors, and Deductive Proof requires too much human intervention for our purpose.

We will use symbolic model checking to prove the correctness of properties about the deactivation of the cruise control of a car. These properties are safety related invariants about system requirements and are generally modeled as observers [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF]. Observers are described in the same language as the model, and engineers can easily write them. When proved valid, they provide a higher assurance level of software correctness. Otherwise, the designer gets a valuable counterexample that helps him correct his design. In our case, we distinguish two kinds of safety properties, those that are stateless invariants and those that involve timers.

For our use case, we used SCADE with its integrated prover called Design Verifier (SCADE DV). We found that all our properties were proved immediately except those that were using long-running timers. For some models, it was impossible to prove them within 24 hours. The commercial tools that we used are black boxes and it is impossible to understand the reason of this proof failure by putting them into debug mode for example. As timers are something very common in industrial models, this motivated us to convert our SCADE model into Lustre [START_REF] Caspi | LUSTRE: A Declarative Language for Real-time Programming[END_REF], and then use some open source model checkers to understand why they were not proved, and to experiment new algorithms for proving this type of properties.

Our contribution, presented below, is about scaling the proof of time properties on production models. We propose a general improvement for invariant generators and a new methodology for obtaining better performance and scaling. As a proof of concept, we implemented it in the JKind model checker [START_REF] Gacek | The JKind Model Checker[END_REF] and tested it on our representative production model, as well as on some production models from Rockwell Collins (now Collins Aerospace). The result is that properties previously very slow or impossible to prove are now proved within a few seconds and in a completely automatic manner.

II. USE CASE PRESENTATION

In this section, we first present the algorithms we used for proving properties then we present our model and the properties to be proved.

A. Preliminaries 1) Induction-based Model Checking: An inductive approach called k-Induction was proposed in [START_REF] Sheeran | Checking Safety Properties Using Induction and a SAT-Solver[END_REF]. It consists in proving that a property/specification is valid for all reachable states of a system i.e. it is invariant. It proceeds in two steps: firstly, it proves that the property is initially satisfied by the k first states, secondly it proves that if the property holds for k successive states it also holds for their successor. Common inductive-based model checkers iterate over k and send requests to SMT-solvers to check the validity of the k-Induction. At iteration k, each variable is duplicated k times, so the size of the SMT requests grows with the number of iterations and their solving time grows exponentially with k.

2) Invariant generation: An invariant generation procedure produces lemmas to allow the proof of properties that are not k-inductive. An invariant can be totally inductive or kinductive for some k ≥ 2.

3) Property Directed Reachability: Property Directed Reachability (PDR), which is also known as IC3 1 , was developed initially for purely propositional systems and hardware verification [START_REF] Bradley | Property-directed incremental invariant generation[END_REF], [START_REF] Een | Efficient Implementation of Property Directed Reachability[END_REF]. Some generalization for SMT was introduced in [START_REF] Cimatti | Software Model Checking via IC3[END_REF] and [START_REF] Hoder | Generalized Property Directed Reachability[END_REF] for software verification. When a property is not inductive, PDR uses the counterexample provided by the SMT-solver to generate and/or strengthen the invariants. A sequence of frames blocking the dangerous states is constructed incrementally, mixing backward analysis of the proof obligation and forward propagation taking into account the initial states. Despite interval generation policies applied to the SMT counterexamples, PDR only generates invariants of simple forms that may not be strong enough to prove the property.

In practice, inductive model checkers often use a combination of the above techniques.

B. Model and Environment

We illustrate the use of symbolic model checking to prove the correctness of safety properties on a representative production model of a cruise control function. This function manages the speed of the car, switches to the right operating mode, manages the user interface, detects faults and decides whether the function should be turned on or off. It uses only linear arithmetic over integers.

We used ANSYS SCADE Suite (Safety Critical Application Development Environment) to design the model from low-level software textual requirements. The properties to be checked were also modeled in SCADE from high-level system safety requirements. The proof was done with SCADE DV [START_REF] Bouali | Formal Verification for Model-Based Development[END_REF], which is a symbolic model checker integrated in SCADE. We chose SCADE for our experiments because it has formal foundations [START_REF] Colaço | Scade 6: A Formal Language for Embedded Critical Software Development[END_REF] compared to Simulink, which is more simulation oriented and without a single formal background [START_REF] Zou | Formal verification of simulink/stateflow diagrams[END_REF]. Actually, SCADE has a formal language based on Lustre, thus we could compare its internal model checker with other open source model checkers for Lustre.

At Groupe PSA, the embedded software is developed according to a standard V-Model methodology. High-level system requirements (HLR) are allocated to an Electronic Control Unit (ECU). Then they are decomposed into lowlevel software requirements (LLR) used to develop the code (handwritten or model-based).

We present our use case environment on Fig. 1. It is composed of a SCADE model, properties, and assumptions when needed. We used multiple model checkers to compare their performances (GATeL [START_REF] Marre | Test Selection Strategies for Lustre Descriptions in GATeL[END_REF], SCADE DV [START_REF] Bouali | Formal Verification for Model-Based Development[END_REF], JKind [START_REF] Gacek | The JKind Model Checker[END_REF], Kind2 [START_REF] Champion | The Kind 2 Model Checker[END_REF]), and addressed multiple SMT solvers in the back-end (CVC4 [START_REF] Barrett | CVC4[END_REF], MathSAT [START_REF] Cimatti | The MathSAT5 SMT Solver[END_REF], SMTInterpol [START_REF] Christ | SMTInterpol: An Interpolating SMT Solver[END_REF], Yices2 [START_REF] Dutertre | Yices 2.2[END_REF], Z3 [START_REF] Moura | Z3: An Efficient SMT Solver[END_REF]). GATeL has its own SMT called Colibri developed at CEA. SCADE DV has its own SMT provided by Prover Technologies. JKind can use CVC4, MathSAT, SMTInterpol, Yices2 and Z3 via SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF]. Kind2, the successor of PKind and Kind, can use CVC4, Yices2 and Z3 also via SMT-LIB. At the moment of our experiments, Kind2 was unable to use IC3 with Yices2.

C. Writing formal properties

As reported in [START_REF] Cofer | Formal Methods Case Studies for DO-333[END_REF], writing good formal properties shares many similarities with writing good requirements and is as much art as science. This report mentions that properties that cut across an entire system often find the most errors and that the best sources of formal properties are found in the safetyrelated requirements for the system.

We therefore formalized properties from the safety-related requirements, and extended them to all high-level requirements (HLR) concerning the deactivation of the function. We have safety-related requirements separated from the HLRs because they are written by a safety engineer and the HLRs are written by the function designer. We want to prove the validity of all these properties i.e. no matter what happens, the cruise controller will deactivate upon the specified conditions. Some of these requirements are listed in Table I.

REQ-01

A simple press on the Cancel button shall disable the cruise controller.

REQ-02

Switching off the ignition shall disable the cruise controller.

REQ-03

In order to respect the safety objectives when the brake pedal sensor is not working: a deceleration (Decel) under a defined threshold value (T2) and the brake pedal not seen pressed during 2 seconds shall turn off the function.

REQ-01 and REQ-02 are typical stateless invariants that are well handled and easy to prove with the actual model checkers.

REQ-03 uses time. When time is increased in the property and in the model, this makes the proof difficult because the number of states explodes. For our experiments, we modeled this property at three different levels:

• We name PG the global property that is checked at the bounds of the whole system (1300 lines of Lustre code and 78 nodes), see Fig. 3. • Then we keep the model of the whole system but we rewrite PG into PL, which is the same property expressed locally on the bounds of the node that implements the authorization function, see Fig. 4. • Finally, we isolate the node that implements the authorization function (320 lines of Lustre code and 3 nodes) to reduce the state-space, and call PI the property to be checked, which is the same as PL, only the context is different, see Fig. 5. The inductive model checkers that we considered implement slicing algorithms such as the cone of influence (COI). Roughly, the cone of influence of a property is the structural part of the design on which the property depends. Before starting an analysis, the COI is computed in order to remove the parts of the design that have no influence on the property under analysis. We decided to check the PL property in order to see the efficiency of the slicing algorithms, and also to use it for compositional analysis, see section II-D. It is equivalent to PI but has some sort of environment that can give preconditions and reduce its state space.

In the case of PI (Fig. 5), we noticed that two things made the proof difficult. Firstly, trying to prove a property over a long period of time, such as 2 minutes instead of 2 seconds, takes too much memory or time for some model checkers. We call this property PI-X where X is the number of 50 ms time steps (for example, 2 seconds represent 40 steps). Secondly, we want to check the difficulties that a model checker would have when checking a valid property that does not match exactly what the code does. We consider two variants of PI-X depending on the deceleration threshold:

• PI-X-T2: (Decel < T 2 ∧ X) ⇒ P I is the original property; • PI-X-T1: (Decel < T 1 ∧ X) ⇒ P I has a stronger precondition because T 1 < T 2, thus it is a weaker property, which is valid when PI-X-T2 is valid. Our final goal was to prove the global property PG (involving the entire model) directly, but we noticed that for long-running time properties it was impossible to scale. We decomposed it in two smaller properties and used a compositional approach to prove the property on the entire model. Property PL (expressed locally on the node implementing it) was used for compositional reasoning as discussed in the next section.

D. Compositional approach

A compositional approach reduces the complexity of the verification of a big model by dividing it into 2 or more components. We divided our model into two components as shown on Fig. 6:

E. Results analysis

In this section, we comment on the results obtained for PG, PL and PI with a small number of time steps (40, which is equivalent to 2 seconds) and with a large number of time steps (2400, equivalent to 2 minutes). We also used two different values for the properties deceleration threshold: T1 and T2, where T 1 < T 2. Experiments were run on an Intel ® Xeon ® CPU E5-2609 v2 @ 2.50GHz and 64 GiB of memory with SCADE DV, Kind2 1.1.0 and JKind 4.0.1. We used all available SMT-solvers with Kind2 and JKind but found that Kind2 generally works best with Z3 (4.7.1) and JKind with Yices2 (2.5.2). Our results listed below are obtained with these solvers. Kind2 does not support PDR/IC3 with Yices2 and thus cannot be compared to JKind with Yices2, which supports it. The timeout option of the model checkers was set to 2 hours (wall-clock time). The results obtained by GATeL were unsound and we do not comment on this model checker in the rest of the paper.

1) Invariant generation is mandatory: Our first experiment was to disable PDR and invariant generation processes and we found that this type of time properties were not k-inductive even for 2-step models. We needed additional invariants to strengthen the property.

2) PDR/IC3 only for small timers and models: Our results show that PDR is a good strengthening algorithm only for small numbers of time steps and small models. With the time span of properties and the size of the model, there is a combinatorial explosion.

3) Threshold impact: The deceleration threshold T1 affected essentially SCADE DV. We noticed that Kind2 and JKind had no problem with it, even if it slowed down the proof. The SMT solvers behind them have stronger theories on integers. The threshold T2 affected essentially Kind2, as long-running timers were impossible to prove with it.

4) Subnode property PI: Increasing the time span from 40 to 2400 steps for the small model with property PI took more time with Kind2, but resulted in a timeout for JKind. JKind and Kind2 use a different implementation of the templatebased invariant generation techniques described in [START_REF] Kahsai | Instantiation-based Invariant Discovery[END_REF]. Even when the PDR process produces the proof, it sometimes uses invariants provided by the invariant generator, we noted it PDR+Invgen in the results below.

5) Compositional approach with property PL:

We used property PL combined with PLH to decompose the complex property PG into two simpler problems. Proving PL is almost equivalent to PI when using slicing because it eliminates the code that is not concerned by the property. JKind was unable to prove the long time PL property, and Kind2 showed that for the T1 threshold it was possible to prove it using its invariant generator, but not for T2. 6) Global property PG: Our final goal was to prove the global property PG, taking into account the entire model with a long-running timer (2400 steps). We encountered some difficulties with SCADE to prove it when using the T1 threshold, and Kind2 was unable to prove it with the T2 threshold. JKind was unable to prove long-running timers at all. This motivated us to try to understand these difficulties.

Table II and Table III present the results obtained with different number of time steps and thresholds. The measured time is in seconds of wall-clock time. As Kind2 and JKind run multiple engines such as PDR, k-Induction and invariant generation in parallel, we put the engine that provided the first result. The second one helped the first with a useful invariant.

A. SCADE to Lustre transformation

As SCADE has a textual language inherited from Lustre, we developed a tool based on an XSLT transformation called SCADE2Lustre. We used SCADE to convert our model into the SCADE textual language and then we transformed this textual representation of our model into Lustre code using our SCADE2Lustre tool. As JKind does not support SCADE automata, we rewrote our automaton in Lustre and checked using JKind and Kind2 that we had the same proof results as those obtained by SCADE DV.

B. Understanding the problem

We analyzed our model with different numbers of time steps, different algorithms such as k-Induction, PDR/IC3 and invariant generation, at different levels of abstraction (properties PG, PL, PI). We also used different model checkers and different SMT solvers as back-ends. We found use cases with long-running timers in production models that all available model checkers were unable to prove. In order to understand the problem we decided to use and modify JKind for its particular implementation of Inductive Validity Cores (IVC) [START_REF] Ghassabani | Efficient Generation of Inductive Validity Cores for Safety Properties[END_REF]. We used IVC to get the invariants that had enabled the proof. It was useful for understanding what candidates we needed to generate for the proof.

1) k-Induction: The basic idea behind k-Induction is to make use of invariants that are not 1-inductive. With the increase of k, there is a combinatorial explosion, so it can run for a very long time. It was the case for our property involving time because it was not k-inductive for a small k. This is why we needed a smarter invariant generator to help strengthen the property before k goes too high.

2) PDR/IC3: PDR can strengthen the property, but the number of invariants it constructs from the property explodes when the time span of the property and the size of the model increase. Because of the interval generation, most invariants are useless for our proof and just slow down the proof process. Furthermore, these invariants appear to find relations only between variables and constants but not between multiple variables. For long-running time properties on production models, PDR suffered from the same combinatorial explosion problem as k-Induction.

3) The JKind invariant generator: JKind uses a templatebased lemma generation, as described in [START_REF] Kahsai | Instantiation-based Invariant Discovery[END_REF], for its invariant generation procedure. In order to obtain invariants to strengthen the proof, JKind creates a list of candidates representing literals. Four different types of candidates are generated automatically:

• Boolean candidates: all boolean system variables and their negations e.g. a and not a where a is a boolean. • Init candidates: integer variables are compared with ≥ and ≤ operators to their initial values e.g. (i ≥ 0), (i ≤ 0) where 0 is the initial value of i. • Subrange candidates: variables of an integer subrange type are compared for equality to all the values in the subrange, e.g. (s = 0), (s = 1), (s = 2) for s ∈ [0..2]. • Enum candidates: variables of an enum type are compared for equality to all the values of the enum. The invariant generator checks all propositional formulae (with boolean operators) involving these literals, whether they are invariants or not. The number of formulae grows exponentially with the number of literals. To avoid this combinatorial explosion, JKind reduces its candidates to those listed above and no relational candidates (explained in subsection III-C) are considered.

All these candidates were not strong enough for proving our long-running timer properties.

C. Contribution

JKind uses multiple cooperative engines in parallel, including k-Induction, PDR and template-based invariant generation. We worked on the improvement of the invariant generation. We noticed that our property used a constant value for the number of time steps and the code also used a constant for it. The same was true for other clauses in the property. We needed invariants that could provide information about the relation (essentially a comparison) between constants and variables of the property and constants and variables of the model. In order to find relations between the property and the model, we propose two new additional categories of relational candidates (atoms):

• INT × INT: for all integer variables in the model and the property, add a comparison relation with the ≥ operator, e.g. V ariable1 ≥ V ariable2

• INT × CONST: for all integer variables and constants in the model and the property, add comparison relations with the ≥ and ≤ operators, e.g. V ariable1 ≥ Constant1; V ariable1 ≤ Constant1 We implemented this new invariant generation algorithm in JKind and applied it to a sub-node of our model with a large number of time steps (property PI-2400). We were able to prove the property within a few seconds although it was impossible to prove before. Once we could prove the property, it was possible to use IVC to find the invariant that had enabled the proof. We used it to understand what were the most useful candidates we needed to generate for the proof.

Next, we wanted to prove the entire model with a long time property (property PG-2400). With our new invariant generator, we had the needed candidates but for the entire model their number was too big. We noticed also that numerous candidates did not make sense, e.g. when comparing a variable about speed to a constant about deceleration, or comparing counters with non counter elements. To get interesting invariants, we propose to use the physical type (speed, deceleration, counter, etc.) of the variables and the constants, and to keep only candidates that compare elements of the same physical type. We explain this in details in the next section.

1) Physical types methodology: A physical quantity is a physical property that can be quantified by measurement. A physical quantity can be expressed as the combination of a number and a unit. For example, in the physical world, we measure the quantity of speed using the unit m s -1 and its derivations. The same is true for other physical quantities. In the automotive and other industries, most of the external interfaces of a function represent a physical quantity (speed, deceleration, battery voltage, etc.) and has a physical unit.

At the code level, information about units is lost and only numbers are present. Fortunately, at the software architecture design level, the physical units are present. As most of the software is designed using model-based design tools, this information can be used for model verification. We propose to use this semantic information to have a deeper understanding of the variables and to generate less invariant candidates while increasing their usefulness. As a methodology, we propose the introduction of physical types at the model level for tools such as Simulink or SCADE. Instead of using a base representation types such as int, we declare a type for each physical quantity, e.g. tSpeed, tDeceleration, tVoltage, tCounter etc. Then all the variables and constants are typed according to their appropriate physical type. Actually, these new types are just aliases of the base representation types, but they carry more semantics for our algorithm. Thus we can recognize data of the same physical type and reason on them using the appropriate relations, see Fig. 7.

For our use case, we defined physical types in SCADE during the design phase. Then, we used them for all the constants and variables of the model. This takes little when done during the design stage. As types are immediately evaluated and shown on the SCADE model, it also gave a better readability during the review of the model. Once the Fig. 7. Constants and variables partitioned by their physical types model was validated, we converted it into Lustre code using our SCADE2Lustre converter, which preserves types.

2) Timers patterns: We wanted to optimize further our algorithm, and to push only the most relevant candidates. By analyzing the useful candidates from the minimal invariants used for the proof (see IVC above), we noticed that all the variables that were useful were assigned a previous value (they correspond to state variables). We propose to eliminate variables that are not assigned a previous value, which correspond to combinatorial variables for which SMT solvers are very efficient, so invariant generation is not necessary. An example of state and combinatorial variables is shown on Fig. 8 Fig. 8. The interesting variables for proving properties about time are those that encode a state. The others are dismissed.

3) Implementation in JKind: We introduced our improvement on a GitHub branch of JKind2 called "invgen-timers". We modified JKind to be able to preserve the original Lustre types because they were lost after inlining. We introduced an option "-inv_gen_level" proposing more and more candidates when the level increases: This level can be used if the other levels do not provide the necessary invariants. The idea behind this new option is to provide different amount of invariants so that the user can begin with the lowest level. If the property cannot be proved with it, the next level could be used until the property is proved. Beginning with the highest level may degrade the performance for properties where a lower level would be sufficient.

IV. RESULTS AND BENCHMARKS

In this section, we examine the results obtained by our invariant generation algorithm and methodology using physical types compared to the results obtained with the official versions of JKind and Kind2. We also used JKind's and Kind's benchmarks to find use cases about timers and compare performances. Finally, we asked Rockwell Collins for use cases about timers and found that some properties on production models, which were not proved before with JKind, were now proved within a few seconds thanks to our improvements.

A. Our use cases

We summarize here the results obtained with our cruise controller model.

In tables IV and V we present the results in seconds obtained using our methodology (JKind new) based on physical types compared to the previous results (Kind2 and JKind official versions). We notice that JKind new (Level 1) outperforms the official versions of the other model checkers for both deceleration threshold values T 1 and T 2.

B. JKind benchmark

JKind provides with its source files, 56 Lustre programs with properties to be proved. We used it to compare the performance of our different algorithms with the official one. We did not find long-running timers in this benchmark and the new levels of invariant generation we introduced in JKind did not bring better results. We suppose that this benchmark was tuned for the current JKind version, as there are no unsolvable problems in it (everything can be proved or invalidated).

C. Kind benchmark

We also used a suite of 1047 Lustre programs developed as a benchmark for Kind [START_REF] Hagen | Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques[END_REF]. Most of them were very small and not containing timers. Their properties were proven in less than a second. However, we found some programs that were using timers. We present their results in Table VI using our implementation of the three different levels of invariant generation (L1, L2 and L3), compared to the JKind and Kind2 official versions. The timeout was set to 10 minutes, Z3 was used with Kind2 and Yices2 with JKind.

D. Rockwell Collins use cases

At Rockwell Collins, Lustre is used as an intermediate language to make formal proofs of high-level properties. Some models have properties with long-running timers. First, they provided us with a representative version of their production model with a property using 6000 time steps that was impossible to prove before. We proved it in a few seconds. Then we shared our new version of JKind with them so that they try it on their internal production models that they could not share with us. They told us that it proved in a few seconds properties that were not proved before.

V. CONCLUSIONS AND FUTURE WORK

In this paper, we have proposed an algorithm that brings an improvement to invariant generation, enabling the automatic proof of properties involving long-running timers, which are present in most embedded software. This algorithm consists in injecting new relational invariant candidates to enrich the invariant generation. However, if too few candidates do not allow concluding, too many candidates can slow down the proof and lead to timeouts. That is why we propose a new methodology using physical types (speed, deceleration, etc.), which restricts the number of candidates to only those that make sense (e.g. deceleration variables compared to deceleration constants or speed variables compared to other speed variables) and may therefore be useful for the proof. Our algorithm is applicable to all forms of inductive model checkers. We have implemented it as part of the open source model checker JKind. We have shown that it outperforms the official versions of JKind, Kind2 and SCADE Design Verifier on benchmarks and on several industrial use cases.

With this paper, we also want to show a way to improve the state of the art in formal methods. When using real production models we do not have access to advanced academic model checkers and solvers because industrial companies essentially use black box tools that cannot be put in a debug mode or modified. If the proof is not possible, it is very difficult to understand why. We used the Lustre language as an intermediate language between the black box tools and the open source model checkers. This allowed us to understand what was missing to automatically strengthen the proofs, and to implement our new algorithm in JKind as a proof of concept.

The presented method for generating invariants is working fine when the counter in the property and the counter in the model evolve at the same rate and sequentially. This is the most common case for industrial models. There can exist models that increment counters at different rates. For the moment, these models need additional invariants provided by the user as assertions.

Our invariant generation technique and methodology using types could also be applied to a more difficult problem: proving properties on nonlinear systems. Modern SMT solvers take into account some nonlinear theories, but it is time consuming to obtain models for complex nonlinear queries. We plan to investigate how the nonlinear barrier could be removed using invariant generation.

Fig. 1 .

 1 Fig. 1. Verification using multiple model checkers and multiple SMT solvers

Fig. 2

 2 Fig.2shows the principal blocks of our SCADE model. It contains an automaton for managing modes, a function for enabling/disabling the cruise control and a function for managing transitions. These components communicate with each other. We want to prove the correctness of the model by writing safety-properties as observers over the SCADE model.

Fig. 2 .

 2 Fig. 2. Cruise controller SCADE model's principal blocks

Fig. 3 .

 3 Fig. 3. Property PG-40 expressed on the bounds of the model

Fig. 6 .

 6 Fig. 6. Compositional approach for properties PL and PLH

TABLE I SYSTEM

 I REQUIREMENTS USED FOR MODEL CHECKING

  Although our model used linear arithmetic over integers, we noticed that increasing the time span of our global property based on REQ-03, e.g. from 2 seconds to 2 minutes, made the proof with SCADE DV fail in a reasonable time (24 hours). To understand the problem, we translated the SCADE model with its properties into the Lustre language, and used open source SMT-based model checkers, putting them into debug mode to analyze the situation.

			TABLE II
	RESULTS USING DECELERATION THRESHOLD T1
		SCADE DV	Kind2 / Z3	JKind / Yices2
	PI-40	2972	141.7 | PDR+Invgen	10.7 | Invgen
	PI-2400	Timeout	139.6 | PDR+Invgen	Timeout
	PL-40	Timeout	156.8 | Invgen	12.6 | PDR
	PL-2400	Timeout	1353 | PDR+Invgen	Timeout
	PG-40	Timeout	373.7 | Invgen	7064 | PDR
	PG-2400	Timeout	155.2 | Invgen	Timeout
			TABLE III
	RESULTS USING DECELERATION THRESHOLD T2
		SCADE DV	Kind2 / Z3	JKind / Yices2
	PI-40	3	3.8 | Invgen	0.8 | Invgen
	PI-2400	2	8.1 | Invgen	Timeout
	PL-40	7	23.9 | Invgen	12.5 | PDR
	PL-2400	11	Timeout	Timeout
	PG-40	9	1370 | Invgen	51.2 | PDR
	PG-2400	11	Timeout	Timeout
	III. APPROACH AND CONTRIBUTION

  All the variables and constants are of type integer, real or boolean. Our level 1 invariant generator is more suitable when physical types are used. However, we can see that levels 2 and 3 performed well on these programs containing counters.

			TABLE VI
	RESULTS USING OUR NEW INVGEN ON KIND BENCHMARK
	Program	Kind2	JKind	JKind-L1	JKind-L2	JKind-L3
	P1	Timeout	13.2	4.3	9.2	6.6
	P2	Timeout	9.9	7.9	10.3	4
	P3	Timeout	13.2	9.4	7.6	13.6
	P4	Timeout	6.5	8.7	10.1	3.8
	P5	Timeout	9.1	58.7	6.9	5.6
	P6	Timeout	Timeout	Timeout	1.7	1.3
	P7	Timeout	Timeout	1.8	1.4	Timeout
	P8	19.3	50.4	6.3	4.4	7.7
	P9	0.4	1.3	1.3	0.2	0.2
	The full names of these programs are:

• P1: DRAGON_11.lus • P2: DRAGON_11_e1_2450.lus • P3: DRAGON_11_e1_2450_e1_5887.lus • P4: DRAGON_11_e1_2450_e2_1483.lus • P5: DRAGON_11_e2_5396_e3_282.lus • P6: durationThm_3_e3_442_e6_113.lus • P7: durationThm_3_e7_334_e8_369.lus • P8: microwave05.lus • P9: twisted_counters.lus This benchmark does not use physical types.

Incremental Construction of Inductive Clauses for Indubitable Correctness

JKind on GitHub: https://github.com/agacek/jkind


Dr Pierre Thuéry
email: pierre.thuery@cea.fr

Dr Youssef Atoini

Sotaro Kusumoto

Shinya Hayami

Dr Yang Kim

Dr Jack Harrowfield
email: harrowfield@unistra.fr

Optimizing Photoluminescence Quantum Yields in Uranyl Dicarboxylate Complexes: Further Investigations of 2,5-, 2,6-and 3,5-Pyridinedicarboxylates and 2,3-Pyrazinedicarboxylate

Keywords: Uranyl cation, Carboxylic acids, Structure elucidation, Photoluminescence

The 2, 5-, 2,6-, and 3,5-pyridinedicarboxylic (2,5-, 2,6-and 3,5-pydcH2), and 2,3-pyrazinedicarboxylic (2,3-pyzdcH2) acids have been used to synthesize six uranyl ion complexes including various counterions under solvo-hydrothermal conditions. While

) is a diperiodic species with sql topology. All complexes have well-resolved uranyl emission spectra in the solid state, and three of them have photoluminescence quantum yields among the highest reported for uranyl carboxylate complexes, 44% for 1, 71% for 3, and 36% for 6.

Introduction

The distinctive photoluminescence properties of the uranyl ion, a cation with a characteristic green emission arising from ligand-to-metal charge transfer and plainly visible in uranylcontaining glasses, have been known for long and studied in depth in recent years. [1] A particular feature of uranyl emission spectra is the presence of a fine structure arising from vibrational coupling, which generally results in a well-resolved pattern of at least four intense peaks. Associated with the richness of uranyl coordination chemistry, encompassing in particular a wide range of coordination polymers of varying periodicity, [2] as well as polynuclear closed species, [3] these luminescence properties have potential application in chemical sensors or other photoactive systems, [4] among which species able to detect ionizing radiation [5] or D2O, [6] or displaying aggregation-induced emission [7] can be singled out. The study of the emission properties of mixed uranyl-lanthanide systems is also an active field or research. [8] In the particular case of cavity-defining, uranyl-containing polynuclear discrete species or porous frameworks, applications as selective heterogeneous photo-oxidation catalysts [9] could be contemplated. [10] Indeed, several reports describe photocatalytic uses of uranyl-containing frameworks, [11] particularly for degradation of pollutants. In this regard, uranyl complexes with high solid state photoluminescence quantum yields (PLQYs) are highly desirable, but these values are seldom reported and, when they are measured, they are often low. If the PLQY of crystalline uranyl nitrate hexahydrate (24%) [12] is taken as a reference, only five carboxylate complexes, all polymeric, have comparable or higher PLQYs, these complexes involving the ligands (1R,3S)-(+)camphorate (23%), [12] 1,2,4-benzenetricarboxylate (35%), [13] 2,6-pyridinedicarboxylate (42%), [12] succinate (49%), [5a] and 1,3,5-benzenetricarboxylate (58%). [5b] It is notable however that a PLQY close to 100% has been measured for a photoluminescent borate framework in which uranyl ions were introduced as activators. [14] In view of the high PLQY measured [12] for the 2, 6-pyridinedicarboxylate complex [UO2Rb2(2,6-pydc)2], [15] it seemed worthwhile to synthesize other complexes with this ligand or its positional isomers, the interest being both to further investigate the polymeric assemblies formed by these ligands and possibly to obtain high PLQY values. We report herein the synthesis, crystal structure, emission spectrum and PLQY in the solid state of five uranyl ion complexes with the deprotonated forms of 2, 6-, 2,5-and 3,5-pyridinedicarboxylic acids (2,6-, 2,5-and 3,5-pydcH2, also known as dipicolinic, isocinchomeronic, and dinicotinic acids, respectively), and of one complex with the dianion of the related 2,3-pyrazinedicarboxylic acid (2,3-pyzdcH2). A search of the Cambridge Structural Database (CSD, version 5.41 [16] ) shows that uranyl complexes of the 2,6 isomer have been the most investigated, with 46 examples reported, among which a helical monoperiodic species is particularly notable, [17] whereas only three examples are known with the 2,5 isomer [18] and one with the 3,5 isomer. [8b] As for 2,3pyrazinedicarboxylate, only three of its uranyl ion complexes have been characterized [19] (some examples with pyrazinecarboxylate [20] and pyrazinetetracarboxylate [21] are also known, and the uranyl ion complexes with the derivatives 2,3-pyrazino [1,10]phenanthroline-2,3-dicarboxylate and 2,6-bis(2-pyrazinyl)pyridine-4-benzoate have been shown to be usable for nitroaromatics detection through fluorescence quenching [22] ). In order to generate complexes with structures different from those already known, different counterions were used in the present work, i.e. ammonium, phosphonium (PPh4 + and PPh3Me + ), and [M(R,S-Me6cyclam)] 2+ (M = Ni, Cu; R,S-Me6cyclam (meso isomer) = 7(R), 14(S)-5,5,7,12,12,14hexamethyl-1,4,8,11-tetraazacyclotetradecane). The complexes thus obtained are zero-, mono-or diperiodic, and one of them has, to the best of our knowledge, the highest PLQY reported up to now for a uranyl ion carboxylate complex.

Results and Discussion

Syntheses

Crystals of all complexes were grown under solvo-hydrothermal conditions at a temperature of 140 °C, the crystals being formed directly from the pressurized and heated reaction mixtures and not as a result of subsequent cooling. The organic cosolvents used were either acetonitrile (1 and 2) or N,N-dimethylformamide (DMF) (3-6), with the occurrence in two complexes of solvent degradation products, i.e. ammonium from acetonitrile in 1, and formate from DMF in 5, both being usual outcomes in such reactions. [12] Three complexes (3, 4 and 6) include hydroxo anions, the ensuing oligomerization being however reduced to dimerization in all cases. Under conditions, as here, where uranyl ion is reacted with simple polycarboxylic acids without addition of base to deprotonate the acid, hydrolysis of the uranyl ion is usually prevented but here may be a consequence of the presence of the pyridine or pyrazine units. The metal/ligand stoichiometry of 7:10 in all the syntheses was chosen so as to favor the formation of an anionic uranium polycarboxylate species and consequent inclusion of counterions, which indeed occurs in all cases, although the metal/ligand stoichiometry in the final complex is either 1:2 (1 and 2) or 1:1 (3-6), the extra negative charge in the latter cases being provided by the hydroxide or formate anions. In the search for complexes with high solid state PLQY values, a useful practical criterion is the colour of the crystals (for illustrations, see references 5 and 7), since at least for values larger than 40% the green emission dominates the pale yellow due to uranyl ion absorption. In the present series, crystals of complexes 1, 3 and 6 clearly showed this feature.

Crystal Structures

Complex 1, [NH4]2[UO2(2,6-pydc)2]3H2O, is a zero-periodic, centrosymmetric, discrete mononuclear complex in which the single uranyl cation is O,N,O-chelated by two 2,6-pydc 2- anions (Figure 1), the tridentate complexation mode being ubiquitous with this ligand. [15,23] The uranium atom is thus in a hexagonal bipyramidal coordination environment, with bond lengths in the usual range [U-O(oxo) 1.774(3) Å, U-O(carboxylato) 2.421(2) and 2.472(2) Å, U-N 2.667(3) Å]. The UO4N2 motif is nearly planar, with a root mean square (rms) deviation of 0.03 Å, the coordinating atoms being slightly displaced from the mean plane in chair fashion. One water molecule forms a bifurcated hydrogen bond with atoms O2 and O4 i bound to uranyl, thus creating a ring with the graph set descriptor [24] R1 2 (4), and it forms another bond with the uncoordinated atom O5 of another complex unit. A second, wider ring, with the descriptor R3 3 (12), results from the connection of the uncoordinated carboxylate atoms O3 and O5 i by the ammonium cation and a second water molecule located on a twofold rotation axis (O7). Further hydrogen bonding of ammonium and water to carboxylate groups from different units results in the formation of a triperiodic network [OO distances 2.757(3)-3.003(3) Å, O-HO angles 137-166°; NO 2.782(3)-3.219(3) Å, N-HO 148-175°]. Calculation of short contacts with PLATON [25] indicates the presence of parallel-displaced -stacking interactions involving the complex anions located in the sheets parallel to (100) [centroidcentroid distance of closest pyridine rings 3.6102(16) Å, dihedral angle 5.30 (14)°, slippage 1.10 Å]. Examination of the Hirshfeld surfaces (HS) [26] calculated with CrystalExplorer (Version 3.1) [START_REF] Wolff | CrystalExplorer[END_REF] shows that CHO hydrogen bonds, [28] generally prevalent in uranyl carboxylate complexes, are absent here. With a Kitaigorodski packing index (KPI, calculated with PLATON) of 0.74, the structure has no free space.

The same arrangement of two 2,6-pydc 2-ligands around uranyl is found in [UO2(2,6pydc)2Cu(R,S-Me6cyclam)] (2), shown in Figure 2. Here also, the uranium atom is located on an inversion centre, and the bond lengths are unremarkable [U-O(oxo) 1.775(5) Å, U-O(carboxylato) 2.462(5) and 2.468(5) Å, U-N 2.664( 6) Å]. The equatorial donors are in a chair conformation and the mean UO4N2 plane has a rms deviation of 0.15 Å. The copper(II) cation This arrangement is reminiscent of that found in other uranyl complexes with 2,6-pydc 2- incorporating 3d-block metal cations. [23b,23g] As usual when a metal azamacrocycle complex is bound to a uranyl-containing motif, hydrogen bonds may contribute to the stability of the assembly, in particular that involving atoms N2 j and O2 [NO 2.969(8) Å, N-HO 177°]. The chains are arranged in sheets parallel to (01ī), within which chains adjacent along [100] are involved in parallel-displaced -stacking interactions [centroidcentroid distance 3.468(5) Å, dihedral angle 0°, slippage 1.22 Å], and the packing is compact (KPI 0.69).

The complexes 1 and 2 are additions to a quite large family [15,23] of species containing the mononuclear [UO2(2,6-pydc)2] 2-anion. Given the many similarities between NH4 + and K + as structural entities, the structure of complex 1 could be regarded as completing structural characterization of the sub-group of this family involving the alkali metals as counter cations. [15,23d,23e] Crystals of complex 1 certainly have the same greenish-yellow colour as have those of its K + analogue, though this is a colour which, visually, is the same for the whole alkali metal family (as well as H + ), [15] and is shared by the related materials involving [AsPh4] + and [HNEt3] + countercations, [23a,29] though not that involving acridinium, [23c] where the colour appears to be dominated by that of the cation. These species do not form an isomorphous series but a striking feature of all the structures is the presence of extended stacking arrays of the [UO2(2,6-pydc)2] 2-units, which are close to planar in all except for [HNEt3]2[UO2(2,6-pydc)2], where they are appreciably bowed. Another feature is that the shortest UU separation is 7 Å or greater, on the high side for most uranyl carboxylate complexes and considerably exceeding that in [UO2(NO3)2(H2O)2]4H2O (6.092 Å), [30] for example. The possible significance of both these features in relation to PLQY values is discussed ahead.

Uranyl O,N,O-chelation is no longer possible with the 2,5-pydc 2-isomer in [PPh3Me][UO2(OH)(2,5-pydc)]H2O (3), and the unique uranyl cation is here O,N-chelated by the nitrogen atom and the adjacent carboxylate group, and bound to one oxygen atom of the carboxylate in the 5 position of another ligand, and to two hydroxide anions [U-O(oxo) 1.7860( 17) and 1.7878( 17) Å, U-O(carboxylato) 2.3779(18) and 2.3984( 17) Å, U-O(hydroxo) 2.2868( 17) and 2.3147( 17), U-N 2.601(2) Å], its environment being thus pentagonal bipyramidal (Figure 3). Such dinuclear uranyl subunits with double hydroxo bridges are very common, [2c] and some examples have been found with the 2,6-pydc 2-isomer. [29] Here again, a monoperiodic coordination polymer is formed, which runs along [010] and has the shape of a quasi-planar ribbon containing a succession of 12-membered rings. These chains are arranged into sheets parallel to (101), separated from one another by layers of counterions (KPI 0.70). The hydroxide anion is hydrogen bonded to the O6 atom of a ligand bound to the same uranyl cation (R1 1 (6) ring), and the water molecule bridges atom O6 and atoms O3 and O4 in the same chain [OO 2.685(2)-3.102(3) Å, O-HO 145(4)-166(4)°]. The 2,5-pydc 2- ligand is not involved in any -stacking interaction, but the PPh3Me + cations are arranged in zigzag rows parallel to [010], with a PP distance of 7.4380(8) Å, held by parallel-displaced -stacking interactions [centroidcentroid 4.1566(15) Å, dihedral angle 23.18( 12)°], an arrangement similar to the "phenyl embraces" found with PPh4 + . [31] The HS shows the presence of several CHO hydrogen bonds, in particular one involving the methyl group of 7) Å, U-O(carboxylato) 2.408 (7) and 2.408(6) Å, U-O(hydroxo) 2.288 (6) and 2.330 (7), U-N 2.632(8) Å] (Figure 4). A ribbon-like, monoperiodic coordination polymer running along

[100] is formed, which displays a shape slightly different to that in 3. In the latter complex, the two bridging ligands in a ring are bound to only one uranyl cation from each dinuclear subunit, these subunits being only slightly inclined with respect to the chain axis, while in 4 they are perpendicular to it and each bridging ligand is bound to a different uranyl cation in the dimer, thus forming larger, 16-membered rings. While the uncoordinated atom O6 of the non-chelating, monodentate carboxylate group is directed outward from the 12membered ring in 3, it is oriented inside the ring in 4 and hydrogen bonded to the hydroxide anion [O7 j O6 2.685(9) Å, O7 j -HO6 148(12)°; R1 1 (8) ring]. In contrast to copper(II) in 2, nickel(II), located on an inversion centre, is only bound to the four nitrogen atoms of the macrocycle [Ni-N 1.959(8) and 1.990(9) Å], so that bridging of the chains is achieved through hydrogen bonding only, either directly or via a water molecule [NO 2.863(12) and 2.909(11) Å, N-HO 161 (11) and 173( 11)°], with formation of R3 3 (10) rings. The packing (KPI 0.74) displays an alternation of anionic and cationic sheets parallel to (010). With a centroidcentroid distance of 4.550( 6) Å and a large slippage of 3.12 Å, the possible intrasheet -stacking interaction may not be significant.

N,O-Chelation is precluded with the 3,5 isomer of the ligand, and the unique uranyl cation in [(UO2)2(3,5-pydc)2(HCOO)2Ni(R,S-Me6cyclam)] ( 5) is chelated by one carboxylate group and bound to two oxygen donors from two more 3,5-pydc 2-ligands, and to one from a formate anion, its environment being pentagonal bipyramidal [U-O(oxo) 1.7653(18) and 1.7737(18) Å, U-O(carboxylato) 2.4426( 16) and 2.4887( 17) Å for the chelating group, 2.3190(18)-2.3455( 16) Å for the other groups] (Figure 5). Uranyl and 3,5-pydc 2-ligands alone form ribbon-like chains parallel to [001] with double bridging of the cations resulting in an alternation of centrosymmetric 8-and 16-membered rings, analogous to that found in the other known complex with this ligand. [8b] The nickel(II) cation, located on an inversion centre, is in a slightly elongated octahedral environment, with four basal nitrogen donors and two axial formate donors [Ni-N 2.061(2) and 2.085(2) Å, Ni-O 2.1690( 17) Å]. The formate bridge between uranium and nickel has a syn(Ni)/anti(U) conformation similar to that seen in other heterometallic complexes, [12] or in simple uranyl formate species. [32] Ni II cations thus bridge the uranyl-containing chains to form a diperiodic 3,4-coordinated network parallel to (110), which has the point symbol {4 2 .6 3 .8}{4 2 .6} and the V2O5 topology. This topological type is frequently encountered when monoperiodic uranyl-containing chains are linked by additional cations. [13,33] One of the NH groups of the macrocycle is hydrogen bonded to the formate oxygen atom bound to uranium (R1 1 different ways in which a given tetra-azamacrocycle complex may contribute to a crystal array. [34] Although the 2,3-pyzdc 2-ligand could be twice O,N-chelated and also O,O-chelated by the two carboxylate groups, modes of coordination indeed observed in previously reported uranyl ion complexes, [19] it has the same connectivity in [PPh4][UO2(OH)(2,3-pyzdc)] ( 6) as 2,5-pydc 2-in 3 and 4. The unique uranyl cation is O,N-chelated by one ligand (a coordination mode also found with the related 2,3-pydc 2-ligand, which is nevertheless also O,O-chelating [23b] ), and bound to one carboxylate oxygen atom from a second ligand and two hydroxide anions [U-O(oxo) 1.754(5) and 1.777(4) Å, U-O(carboxylato) 2.342(4) and 2.370(4) Å, U-O(hydroxo) 2.312(4) and 2.314(4), U-N 2.643(4) Å] (Figure 6). However, instead of crystallizing as a monoperiodic coordination polymer, it yields a diperiodic assembly parallel to (100) which, if the binuclear subunits are considered as single 4coordinated nodes, has the square lattice (sql) topology (however, this description ignores the herringbone arrangement of the dinuclear subunits). A diperiodic network was also found with the related 2,3-pydc 2-ligand, but in this case no hydroxide anion is present and all carboxylate oxygen atoms are coordinated. [23b] The uncoordinated nitrogen atom in 6 is involved in a hydrogen bond with the hydroxide anion [ON 2.816( 6) Å, O-HN 172°; R1 1 (7) ring]. The packing (KPI 0.67) shows quasi-planar sheets separated by layers of counterions, the latter being associated in twos by "phenyl embrace" interactions, with a PP separation of 6.460(3) Å. A parallel-displaced -stacking interaction associates the pyrazine ring and one ring of the counterion [centroidcentroid 3.940(4) Å, dihedral angle 23.9(3)°], and several CHO hydrogen bonds also link the anions and cations.

Luminescence Properties

Emission spectra of complexes 1-6 in the solid state at room temperature under excitation at 420 nm were recorded and are shown in Figure 7. All display the commonly observed fine structure associated with the vibronic progression corresponding to the S11  S00 and S10  S0 ( = 0-4) electronic transitions. [1b] The most blue-shifted spectrum is that of complex 6, with the four main maxima (corresponding to the electronic transitions denoted E and S1-S3 [1h] ) at 482, 502, 524 and 547 nm, these values being more typical of a complex with an O6 rather than an O4N equatorial environment. [35] The maxima in the spectrum of complex 1 are at 488, 510, 533 and 557 nm, these values being at the upper end of the range previously found for complexes with uranyl O4N2 equatorial environments, [35] and similar to those measured for [UO2(2,6-pydc)] [23b] and [UO2(2,6-pydcH)2]4H2O. [15] The most red-shifted spectrum is found for complex 3 (O4N environment) with maxima at 510, 533, 558 and 584 nm, these values being among the most red-shifted measured for a five-coordinated uranyl cation, those for complexes with O5 environments being generally below about 500, 520, 545 and 575 nm. [35] The spectra of the other complexes are more slighly red-shifted with respect to that of 1, with values of 492, 513, 538 and 561 nm for 2 (O4N2), 495, 516, 539 and 563 nm for 4 (O4N), and 489, 511, 534 and 559 nm for 5 (O5). The values for 5 in particular are typical of those generally found for complexes with O5 environments. [35] It is notable that the spectra of 1 and 3 are peculiar in this series since all peaks display shoulders on the lowenergy side, one of these shoulders being even partly resolved for 3 (517 nm). Such shoulders, albeit less prominent, were also present in the spectra of two other uranyl complexes with the 2,6 isomer, either partly or fully deprotonated. [15,23b] This may be significant in the light of the measurements of PLQYs, although such additional complexity in the vibronic progression has been detected in a variety of species [1e,1f,36] and has been attributed to coupling of the electronic transition to vibrational modes involving either the equatorial ligands bound to the uranyl centre or bending of the UO2 unit [1f,36] or indeed to the superposition of another vibronic progression associated with a metal-to-ligand charge transfer transition. [23b] While complexes 2, 4 and 5 have low PLQYs of 4, 1 and 1%, respectively, complexes 1, 3 and 6 have values of 44, 71 and 36%, respectively, the value for 3 being the highest yet reported for a uranyl ion carboxylate complex. The fact that the PLQY is low in 2 4, which have environments similar to 1 and 3, respectively, is likely due to the presence of 3dblock metal cations, the latter either preferentially absorbing the 420 nm radiation, or allowing energy transfer and nonradiative relaxation, often resulting in complete quenching of uranyl luminescence. [37] Such quenching also appears to occur in complexes where [UO2(2,6-pydc)2] 2-units are linked by Fe II , Co II , Ni II , Cu II or Zn II bridges, [23g] since the colours of the isolated crystals under normal sunlight reflect those of the different transition metals and are not dominated by green emission. Complexes 1, 3 and 6, with organic counterions, do not suffer from this drawback. Like all aromatic species, pyridine-and pyrazinedicarboxylate ligands may enhance uranyl luminescence through the "antenna" effect, [1e] arising from energy transfer from excited  electrons of the ligand to the metal, [23b] and given its apparently long-distance operation in uranyl oxyfluorides containing pyridinium as counterion, [38] and efficacity in a uranyl complex with 2,2 -bipyrimidine, [39] it could be possible that heteroaromatic units are efficient in energy transfer than simple aromatic ones, though no visually obvious effects are seen with complexes of the common ligands 2,2 -bipyridine and 1,10phenanthroline. [40] In considering the luminescence of uranyl ion coordination polymers and organic frameworks, it is important to note that such materials are usually insoluble in all solvents other than those which cause their decomposition, so that only solid state PLQY values can be obtained. It has been long known [1e,41] that for simple, water-soluble uranyl complexes PLQY values in water are usually much less than those of the solid solutes and in fact we have observed [15] that emission from water-soluble, mononuclear [UO2(2,6-pydc)2] 2-derivatives involving alkali metal cations, is much weaker in solution than in the solid. More recently, [42] it has been shown that emission from uranyl ion complexes with 2,6-pydc 2-in acetonitrile is an order of magnitude more intense than in water. Hence, it is plausible that the high, solid state PLQY values observed for simple [UO2(2,6-pydc)2] 2- derivatives (presently extended to the species with countercations Li + , Na + , K + and Cs + with of 26, 33, 27 and 38%, respectively, as well as the 44% found for complex 1) may be a form of "aggregation enhanced luminescence" where the effect of the aggregation required to form a crystal is simply that of minimizing contact with solvent molecule quenchers (water, in particular). This is in conflict with our earlier suggestion [15] that the extensive stacking arrays of aromatic units observed in the structures of these materials might signify interactions giving rise to an especially efficient means of energy transfer from the "antenna" to the metal ion but it is consistent with numerous more recent structure determinations showing extensive stacking arrays in complexes which are not strongly luminescent. [43] Nonetheless, for a uranyl carboxylate complex which undergoes a singlecrystal to single-crystal transformation when exposed to water, [7] it is the hydrated product which has the higher PLQY and there are many instances in general where coordinated water has a negligible effect on emission intensity, [1e] not to mention the moderate solid state PLQY retained in [UO2(NO3)2(H2O)2]4H2O, so that the "lack of quenchers" argument to the high PLQY values of variously hydrated crystalline (Cation)2[UO2(2,6-pydc)2] species must remain tentative, even though it is true that there are no direct interactions between the water molecules and uranyl oxygen atoms in any of the structures. [15,23d,23e] In regard to interactions within the stacks of aromatic units, examination of the Hirshfeld surfaces does not provide of interactions beyond dispersion, indicating that they are not unusually strong and where, in different complexes, there do appear to be additional, specific interactions, these lead not to enhancement of uranyl emission but to its replacement by emission with the characteristics of an organic fluorophore. [44] Emission from hydroxo/oxo-bridged oligomers of uranyl ion can have an unusual form taken to be indicative of direct electronic interactions between close uranyl centres, [45] and an alternative explanation of the strong emission from (Cation)2[UO2(2,6-pydc)2] species initially considered was that the relatively long UU separations (7 Å) found in the crystal structures might signify an absence of perturbations shortening excited state lifetimes due to UU interactions. There is a rough correlation between the minimum UU distances and the PLQY values, with the PLQY generally increasing with increasing separation but this is clearly not an argument which could be extended to explain the high PLQY values in complexes 3 (71%), [UO2 (1,3,5-btcH)] (58%, btc = benzenetricarboxylate) [5b] ,

[NMe4]2[(UO2)4(C2O4)4(succinate)] (49%) [5a] , 6 (36 %) or [PPh4][UO2 (1,2,4-btc)] (35%), [13] where the minimum UU separations are 3.85, 5.23, 5.55, 3.85 and 5.12 Å, respectively. These five complexes have features which clearly distinguish them from the (Cation)2[UO2(2,6-pydc)2] family. They are all true coordination polymers of low solubility and all contain pentagonal-bipyramidal, not hexagonal-bipyramidal, U VI centres. Three of the five, 3, [UO2 (1,3,5-btcH)] and [PPh4][UO2 (1,2,4-btc)], have structures incorporating monoperiodic polymer chains in which dinuclear units have hydroxide or carboxylate bridges, while that of [NMe4]2[(UO2)4(C2O4)4(succinate)] contains monoperiodic chains of oxalate-bridged uranium centres lying in sheets linked into a triperiodic array by succinate ligand bridging, and that of complex 6 involves diperiodic sheets where dihydroxy-bridged dinuclear units are linked by the ligands. All show a well-resolved vibronic progression in their green emissions, with little evidence (see above) that the proximity of uranium centres has any marked influence on the form of the emission bands. While there are similarities in the four monoperiodic chains, related complexes such as [PPh4]2[(UO2)2 (1,2,4-btcH)3]H2O [13] containing monoperiodic chains seemingly only slightly different, although in this instance containing hexagonal-bipyramidal uranium centres, are only weakly luminescent, so that exactly what features of the chain structures may be most important is uncertain.

Conclusions

The synthesis, crystal structure, emission spectrum, and PLQY of six uranyl ion complexes with the ligands 2,5-, 2,6-and 3,5-pyridinedicarboxylate and 2,3-pyrazinedicarboxylate have both expected and unexpected features. Solvothermal syntheses using the acids and not their conjugate bases as reactants have provided, as commonly observed with carboxylic acids, carboxylate complexes of uranyl ion but in three cases in association with a degree of hydrolysis of the cation which may reflect the influence of aza-aromatic-N. Given the high PLQY values found here for complexes containing U(OH)2U units, this may be a particularly important property of these ligands. All the ligands employed except 3,5-pydc 2-act as chelates towards the uranyl cation in the O,N or O,N,O mode depending on whether the nitrogen atom is flanked by one or two carboxylate groups but in the pyrazinedicarboxylate one nitrogen atom remains uncoordinated, consistent with the oxophilic character of uranyl ion. Except for complex 1 which is a discrete anionic mononuclear species, all the complexes are anionic coordination polymers, with periodicities of 1 (2, 3 and 4) or 2 (5 and 6) and low solubility, rendering them of potential interest as heterogeneous photo-oxidation catalysts.

Various countercations are included, which play different roles in the structures: NH4 + in 1 and Ni(R,S-Me6cyclam) 2+ in 4 interact with the anion through hydrogen bonding, PPh3Me + in 3 and PPh4 + in 6 are organized in sheets loosely interacting with the anionic layers through CHO hydrogen bonds and -stacking interactions, and Cu(R,S-Me6cyclam) 2+ in 2 and Ni(R,S-Me6cyclam) 2+ in 5 are part of the coordination polymers. All six complexes have wellresolved uranyl emission spectra in the solid state, but the PLQYs are widely different. While complexes 2, 4 and 5 have low PLQY values of 4, 1 and 1%, respectively, probably because of the presence of 3d-block transition metal cations in the structure, complexes 1, 3 and 6, with counterions, have values of 44, 71 and 36%, respectively, that for 3 being the highest reported for a uranyl ion carboxylate complex. Consideration of the structures of 1, 3 and 6 with those of other known species having high PLQY values is hampered by the limited extent of current data but complexes of 2,6-pydc 2-containing hexagonal-bipyramidal U VI appear to emit strongly when in a structure where they are well separated (and where transition metal ions are not present) while, somewhat paradoxically, complexes of other aza-aromatic dicarboxylates containing pentagonal-bipyramidal U VI emit strongly (in the presence of organic counter cations) when binuclear species bridged by hydroxide or carboxylate are present.

Experimental Section

General: UO2(NO3)2•6H2O (RP Normapur, 99%) was purchased from Prolabo, and the dicarboxylic acids were from Merck or Aldrich. [M(R,S-Me6cyclam)(NO3)2] (M = Ni, Cu) were synthesized as previously described. [33b,46] Elemental analyses were performed by MEDAC Ltd. at Chobham, UK. For all syntheses, the mixtures in demineralized water were placed in 10 mL tightly closed glass vessels and heated at 140 °C in a sand bath, under autogenous pressure.

Caution! Uranium is a radioactive and chemically toxic element, and uranium-containing samples must be handled with suitable care and protection.

[NH4]2[UO2(2,6-pydc)2]3H2O ( 1): 2,6-pydcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and PPh4Br (42 mg, 0.10 mmol) were dissolved in a mixture of water (0.8 mL) and acetonitrile (0.2 mL), giving green-yellow crystals of complex 1 within one month ( 13mg, 38% yield based on the acid). C14H20N4O13U calcd. C 24.36, H 2.92, N 8.12; found C 24.01, H 2.70, N 7.93.

[UO2(2,6-pydc)2Cu(R,S-Me6cyclam)] (2): 2,6-pydcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and [Cu(R,S-Me6cyclam)(NO3)2] (24 mg, 0.05 mmol) were dissolved in a mixture of water (0.8 mL) and acetonitrile (0.2 mL), giving light purple crystals of complex 2 low yield within two weeks.

[PPh3Me][UO2(OH)(2,5-pydc)]H2O (3): 2,5-pydcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and PPh3MeBr (36 mg, 0.10 mmol) were dissolved in a mixture of water (0.8 mL) and DMF (0.2 mL), giving green-yellow crystals of complex 3 within ten days (22 mg, 42% yield based on U). Elemental analysis results indicate the presence of a small amount of water in excess of the quantity found from crystal structure determination. C26H24NO8PU + 0.5H2O (756.46): calcd. C 41.28, H 3.33, N 1.85; found C 41.18, H 3.15, N 1.57. [Ni(R,S-Me6cyclam)][UO2(OH)(2,5-pydc)]22H2O (4): 2,5-pydcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and [Ni(R,S-Me6cyclam)(NO3)2] (23 mg, 0.05 mmol) were dissolved in a mixture of water (0.8 mL) and DMF (0.2 mL), giving orange crystals of complex 4 overnight (24 mg, 53% yield based on U). C30H48N6NiO16U2 (1283.51): calcd. C 28.07, H 3.77, N 6.55; found C 27.75, H 3.71, N 6.26.

[(UO2)2(3,5-pydc)2(HCOO)2Ni(R,S-Me6cyclam)] ( 5 were dissolved in a mixture of water (0.8 mL) and DMF (0.2 mL), giving yellow crystals of complex 5 within two months (21 mg, 46% yield based on U). C32H44N6NiO16U2 (1303.50): calcd. C 29.49, H 3.40, N 6.45; found C 28.82, H 3.33, N 5.84.

[PPh4][UO2(OH)(2,3-pyzdc)] ( 6): 2,3-pyzdcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and PPh4Br (42 mg, 0.10 mmol) were dissolved in a mixture of water (0.8 mL) and DMF (0.2 mL), giving yellow-green crystals of complex 6 in low yield within one month.

Crystallography: The data were collected at 100(2) K, either on a Nonius Kappa-CCD area detector diffractometer [47] using graphite-monochromated Mo K radiation ( = 0.71073 Å) (complexes 1, 2 and 6) or on a Bruker D8 Quest diffractometer equipped with an Incoatec Microfocus Source (IS 3.0 Mo) and a PHOTON III area detector, and operated through the APEX3 software [START_REF] Bruker | APEX3. Version 2019[END_REF] (complexes 35). The crystals were mounted into glass capillaries or on Mitegen micromounts with a protective coating of Paratone-N oil (Hampton Research). The data were processed with HKL2000 [START_REF] Otwinowski | [END_REF] or SAINT, [START_REF]SAINT. Version 8.40A[END_REF] absorption effects were corrected for empirically with SCALEPACK [START_REF] Otwinowski | [END_REF] or SADABS. [START_REF] Bruker | SADABS. Version 2016/2[END_REF] The structures were solved by intrinsic phasing with SHELXT, [52] expanded by subsequent difference Fourier synthesis and refined by fullmatrix least-squares on F 2 with SHELXL, [53] using the ShelXle interface. [54] All non-hydrogen atoms were refined with anisotropic displacement parameters. When present, the hydrogen atoms bound to oxygen and nitrogen atoms were found on difference Fourier maps and they were either refined isotropically (with restraints if necessary) or treated as riding atoms. The carbon-bound hydrogen atoms were introduced at calculated positions and were treated as riding atoms with an isotropic displacement parameter equal to 1.2 times that of the parent atom (1.5 for CH3, with optimized geometry). Crystal data and structure refinement parameters are given in Table 1. The molecular plots were drawn with ORTEP-3 [55] and the polyhedral representations with VESTA. [56] Topological analyses were conducted with ToposPro. [57] Table 1. Crystal data and structure refinement details. Zero-, mono-and diperiodic homo-or heterometallic uranyl ion complexes were obtained with 2,5-, 2,6-and 3,5-pyridinedicarboxylates and 2,3-pyrazinedicarboxylate ligands. All are luminescent and one of them has the highest photoluminescence quantum yield reported for a uranyl ion carboxylate complex.

Figure 1 .

 1 Figure 1. (a) View of complex 1. Displacement ellipsoids are drawn at the 50% probability level. Carbon-bound

Figure 2 .

 2 Figure 2. (a) View of complex 2. Displacement ellipsoids are drawn at the 30% probability level. Carbon-bound

Figure 3 .

 3 Figure 3. (a) View of complex 3 with counterions omitted. Displacement ellipsoids are drawn at the 50%

  the cation and the uranyl oxo atom O1 [CO 3.460(3) Å, C-HO 169°]. The complex [Ni(R,S-Me6cyclam)][UO2(OH)(2,5-pydc)]22H2O (4) displays structural features close to those of 3. The unique uranyl cation is similarly O,N-chelated by one ligand and bound to another carboxylate donor and two hydroxide anions [U-O(oxo) 1.749(7) and 1.770(

Figure 4 .

 4 Figure 4. (a) View of complex 4. Displacement ellipsoids are drawn at the 50% probability level. Carbon-bound

Figure 5 .

 5 Figure 5. (a) View of complex 5. Displacement ellipsoids are drawn at the 50% probability level. Carbon-bound

  (6) ring), and the other makes a bifurcated hydrogen bond with the formate oxygen atom bound to Ni II and a uranyl oxo group [NO 2.853(3)-3.098(3) Å, N-HO 110(2)-164(3)°]. The packing is of the bump-tohollow type, the layers being offset with respect to one another (KPI 0.70), with a possible inter-sheet -stacking interaction [centroidcentroid 4.4647(19) Å, dihedral angle 0°, slippage 2.51 Å]. The structures of complexes 4 and 5 provide further examples of the

Figure 6 .

 6 Figure 6. (a) View of complex 6. Displacement ellipsoids are drawn at the 40% probability level. Counterions

Figure 7 .

 7 Figure 7. Normalized emission spectra of compounds 1-6 under excitation at 420 nm.

  ): 3,5-pydcH2 (17 mg, 0.10 mmol), UO2(NO3)2•6H2O (35 mg, 0.07 mmol), and [Ni(R,S-Me6cyclam)(NO3)2] (23 mg, 0.05 mmol)

data can be obtained free of charge from The Cambridge Crystallographic Data Centre via www.ccdc.cam.ac.uk/data_request/cif.

Luminescence Measurements: Emission spectra were recorded on solid samples using a Horiba-Jobin-Yvon IBH FL-322 Fluorolog 3 spectrometer equipped with a 450 W xenon arc lamp, double-grating excitation and emission monochromators (2.1 nm/mm of dispersion; 1200 grooves/mm) and a TBX-04 single photon-counting detector. The powdered compounds were pressed to the wall of a quartz tube, and the measurements were performed using the right-angle mode. An excitation wavelength of 420 nm, a commonly used point although only part of a broad manifold, was used in all cases and the emission was monitored between 450 and 600 nm. The quantum yield measurements were performed by using an absolute photoluminescence quantum yield spectrometer Hamamatsu Quantaurus C11347 and exciting the samples between 300 and 400 nm.