Pascal Fontaine
email: pascal.fontaine@uliege.be

Hans-Jörg Schurr
email: hans-jorg.schurr@inria.fr

Quantifier Simplification by Unification in SMT

Keywords: SMT, quantifier instantiation, theorem proving

Quantifier reasoning in SMT solvers relies on instantiation: ground instances are generated heuristically from the quantified formulas until a contradiction is reached at the ground level. Current instantiation heuristics, however, often fail in presence of nested quantifiers. To address this issue we introduce a unification-based method that augments the problem with shallow quantified formulas obtained from assertions with nested quantifiers. These new formulas help unlocking the regular instantiation techniques, but parsimony is necessary since they might also be misguiding. To mitigate this, we identify some effective restricting conditions. The method is implemented in the veriT solver, and tested on benchmarks from the SMT-LIB. It allows the solver to prove more formulas, faster.

Introduction

Satisfiability modulo theories (SMT) solvers are successfully used as back-ends for formal method applications, within interactive proof assistants or verification platforms. SMT solvers based on the CDCL(T ) calculus [START_REF] Barrett | Satisfiability modulo theories[END_REF] excel at handling quantifier-free problems with theories -SMT problems with thousands of assertions are frequent. While originally SMT solvers were mostly applied on such problems, an increasing number of applications require some support for quantifier reasoning. Their main approach to handle quantifiers is quantifier instantiation. This approach separates the quantified assertions from the ground part of the problem. Whenever the solver finds a model for the ground part, it generates new ground instances of the quantified formulas. This is repeated until the ground solver determines that the ground problem is unsatisfiable. When done fairly, this approach is refutationally complete for many theories and due to the strength of ground solving it is also very powerful in practice. SMT solvers use multiple instantiation strategies to find these instances. The main challenge is to find the right instances without misguiding or overwhelming the solver. Often one can observe some kind of butterfly effect: if the instantiation methods are unlucky, the solver might be misguided to explore a large set of irrelevant instances and reach the solving timeout. In this regard, every strategy has its own strength and weaknesses (Section 2).

If the problem contains a quantified lemma that also occurs, for example, as an antecedent for another formula, the common instantiation methods often fail to quickly produce the right instances. This structure is quite typical of problems generated by interactive theorem provers -a domain to which the SMT solver veriT has been successfully applied [START_REF] Ekici | SMTCoq: A plug-in for integrating SMT solvers into Coq[END_REF][START_REF] Schurr | Reliable reconstruction of fine-grained proofs in a proof assistant[END_REF]. The following toy example illustrates this issue. We will use it to illustrate various ideas.

Example 1.

∀x. P (x) → P (f (x, c))

(1)

¬P (c) ∨ (∀y. (∀z. P (z) → P (f (z, y))) → ¬P (y)) ( 2)

P (c) (3)
This problem is trivially unsatisfiable: when y is set to c, assertion 1 occurs as the antecedent of the implication in assertion 2, so ¬P (c) is a direct consequence of the first two assertions, in contradiction with the third. As described in Section 2.3, all major instantiation techniques fail to directly produce the correct instances for this problem. Because SMT solvers typically only perform very limited preprocessing on quantified formulas and especially do not calculate a full clause normal form, the instantiation methods fail to recognize and exploit the fact that assertion 1 and the antecedent in assertion 2 are so similar. Since the instantiation methods do not produce the correct instances early, the SMT solver will need multiple instantiation rounds to solve the problem. This can lead to the butterfly effect mentioned above. Real world examples are usually more complex. For example, there are often many ground terms which mislead the instantiation heuristics. Furthermore, the assertions in this example are Horn clauses and could be handled by specialized reasoning. Practical problems, however, are not restricted to Horn clauses.

In CDCL(T ) quantified formulas are considered black boxes, and are abstracted as propositional variables in the propositional abstraction of the input formula. These propositional literals are generally of no value to the ground solver. We here make use of them to simplify larger formulas. To solve the example above we identify the occurrence of the unit assertion 1 within assertion 2. By using unification we can eliminate this quantified subformula. The result after simplification is the ground formula ¬P (c). After this formula is conjoined to the problem, it is trivially contradictory. In the general case, we use asserted quantified formulas to soundly simplify nested formulas and augment the problem with the result. We propose multiple variants of the core procedure (Section 3).

So far, techniques inspired by resolution-based theorem provers are underrepresented in SMT solvers. Systems such as DPLL(Γ ) [START_REF] De Moura | Engineering DPLL(T) + saturation[END_REF], DPLL(Γ + T ) [6], and AVATAR [START_REF] Voronkov | AVATAR: The architecture for first-order theorem provers[END_REF] combine the inference system of theorem provers with the CDCL(T ) transition system on a fundamental level, but the combination is coarse -in those systems the two worlds work side-by-side in tandem. Instead, our unification-based method is a lightweight and easily implemented prepro- cessing technique that solves some concrete shortcoming of current instantiation techniques.

We implemented our method in the SMT solver veriT [START_REF] Bouton | veriT: An open, trustable and efficient SMT-solver[END_REF]. To ensure the process is fast, we use a standard term index and unification algorithm which we extended to handle the presence of strongly quantified variables (Section 4).

The evaluation shows that our technique enables veriT to solve benchmarks not solved by any strategy before. When applicable, the method often allows veriT to solve problems within a short timeout. The different variants of the simplification process are useful within a strategy schedule (Section 5).

CDCL(T ) and Quantifier Instantiation

Figure 1 shows the operation of a typical SMT solver when refuting a problem. It first preprocesses the input problem (Section 2.2). Then two procedures together refute the problem: the ground solver either refutes the problem on the ground level, or finds a ground model. If a model is found the instantiation procedure creates new ground lemmas (Section 2.3).

Preliminaries

We use the many-sorted first-order logic with equality as defined in the SMT-LIB standard [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF] and assume the reader is familiar with the notions of signature, term, free and bound variable, quantified and ground formula, literal, and substitution. We use x, y, z to denote variables; s, t to denote terms; ϕ, ψ to denote formulas (i.e., terms of sort Bool); P to a predicate (i.e., a function with codomain sort Bool); and c to denote constants. To denote the substitution which replaces a variable x with a term t we write [t/x]. As usual, σ stands for a substitution. We write t for the sequence of terms t 1 , . . . , t n for an unspecified n ∈ N + that is either irrelevant or clear from the context. Hence, ∀x.ϕ corresponds to a term ∀x 1 , . . . , x n . ϕ. We write free(t) to denote the free variables of a term t. The set T (S) is the set of all subterms of the terms in S. We omit sorts when they are clear from the context and assume that sort constraints are always respected, e.g., substitutions only use terms of the same sort as the substituted variable.

Like in the SMT-LIB standard, the signature Σ always contains a sort Bool, two constants and ⊥, the usual Boolean connectives, and a family of predicate symbols (≈ : τ × τ → Bool) interpreted as equality for each sort τ . A trimmed formula is the generalization of the notion of atom to arbitrary formulas: trim(ϕ) is the formula ϕ after removing all leading negations. For example, trim(¬¬(ϕ 1 ∨ ¬ϕ 2 )) is ϕ 1 ∨ ¬ϕ 2 . The polarity pol(ϕ) ∈ {+, -} of a formula ϕ is -(negative) if trim(ϕ) removes an odd number of negations and + (positive) otherwise.

We write t[ ] for a term with a hole and t[u] for the term where the hole has been replaced by u. Any term has at most one hole. We borrow the notions of weak and strong quantifiers [START_REF] Baaz | Chapter 5normal form transformations[END_REF]: since we are working in a refutation context, a positive occurrence of a quantifier ∃x. ϕ or a negative occurrence of a quantifier ∀x. ϕ is strong and a negative occurrence of a quantifier ∃x. ϕ or a positive occurrence of a quantifier ∀x. ϕ is weak. We will call the subformula ψ of Qx.ψ, where Q ∈ {∀, ∃}, the matrix, even though ψ might not be in clausal normal form. Without loss of generality, we assume that all quantified variables have been renamed to be distinct.

To handle strong quantifiers we use the Skolemization operator sk. For a formula Qx.ψ it is defined as sk(Qx.ψ, ȳ) := ψ[s 1 (ȳ)/x 1 ] . . . [s n (ȳ)/x n ] and each s i is a fresh function symbol of correct arity. The strong quantifier Q might not be below a weak quantifier. In this case we write sk(Qx.ψ, ∅) and the fresh symbols are constants.

Preprocessing

Given an input formula P (i.e., a term of sort Bool) a CDCL(T ) solver performs multiple preprocessing steps before the solving phase is started. This produces an equisatisfiable problem P which is a conjunction of clauses.

To make efficient use of the ground solver, ground formulas are clausified. Quantified formulas, however, are treated differently. Strong quantifiers are usually not fully Skolemized, nor are the formulas put in prenex form or clausified. This has the benefit that the original structure of quantified formulas is preserved, which is crucial for some instantiation techniques.

Preprocessing applies some light form of rewriting on quantified formulas. In veriT, most rewriting steps apply to constants below arithmetic operators and Boolean connectives. For example, the term f (5 + c 1 + 3, c 2 * (3 -3)) is simplified to f (8 + c 1 , 0) and (⊥ → ϕ 1 ) → ϕ 2 is replaced by ϕ 2 . Rewriting also ensures that certain global invariants of veriT are met: for instance, all occurrences of bound variables are renamed to distinct variables, and quantifiers over Boolean variables are removed by Shannon expansion.

Another preprocessing step on quantified formulas is Skolemization. How Skolemization is applied is implementation dependent. The common CDCL(T ) calculus [START_REF] Barrett | Satisfiability modulo theories[END_REF] is only concerned with ground reasoning. While the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] has a builtin tactic called nnf that fully applies Skolemization, CVC4 [3] and veriT only Skolemize outermost strong quantifiers in their default configuration. The rewriter of veriT Skolemizes outermost strong quantifiers by replacing the subformula trim( ) of a formula by sk(trim( ), ∅) if trim( ) has the form Qx. ϕ, the quantifier Q is strong, and does not occur below any quantifier.

Due to the limited preprocessing of quantified formulas, some disjuncts of P start with a weak quantifier and contain complicated formulas. To clarify the distinction, we call the disjuncts which start with a quantifier, and are hence black boxes to the ground solver, boxes. Without loss of generality, we assume all boxes are universally quantified. Disjuncts which are not boxes are ground literals. A unit-box is a clause with only one disjunct that is a box.

Example 2. The preprocessor will not perform any operations on Example 1. We can illustrate the perspective of the ground solver by replacing quantified formulas by frames. The resulting claues are: 1 , ¬P (c) ∨ 2 , and P (c). The first clause is a unit-box and both boxes will be abstracted to different propositional variables for the SAT solver.

Instantiation Techniques

The instantiation loop (Figure 1) starts with the ground solver. It either determines that the ground literals of the preprocessed problem P are unsatisfiable or produces a ground model M. If the ground problem is unsatisfiable, then P is unsatisfiable. M is a set of formulas G ∪ Q where G are ground literals, and Q are boxes. M propositionally satisfies P , and G is consistent with respect to the used theories. The instantiation procedure will then generate lemmas (∀x. ϕ) → ϕσ where (∀x. ϕ) ∈ Q and σ is a substitution of x with ground terms. The generated lemmas are added conjunctively to P and the ground solver is called again.

We now give an overview of common instantiation techniques and illustrate why they cannot tackle Example 1 quickly. These techniques are presented in the order they are used by veriT: it first tries conflict-driven instantiation. If this fails, it will try trigger-based instantiation. Should this produce no instances, it will fall back to enumerative instantiation. Model-based quantifier instantiation is not implemented by veriT: it is crucial for satisfiability, but veriT focuses on proving unsatisfiability.

Conflict-Driven Instantiation. This method tries to find an instance that contradicts the ground model M in the theory of equality and uninterpreted functions (EUF) [START_REF] Barbosa | Congruence closure with free variables[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in smt[END_REF]. Hence, it searches for a box ∀x. ϕ ∈ Q and a substitution σ such that G ∧ ϕσ EUF ⊥. It returns the instance ϕσ or fails. It can also search for substitutions which solve multiple constraints simultaneously. Hence, this method can find a contradicting instance of a clause

ψ 1 ∨ • • • ∨ ψ n by solving G ∧ ψ 1 σ EUF ⊥, . . . , G ∧ ψ n σ EUF ⊥, but all ψ i s must be quantifier-free.
Conflict-driven instantiation is very helpful, since it only generates instances that are immediately useful. It forces the ground solver to find new models and eliminates spurious models from the search space.

Since assertion 2 of Example 1 contains a quantifier, it cannot be instantiated by conflict driven instantiation. Conflict driven instantiation also fails for assertion 1, because initially there is no ground formula that would be in conflict with an instance of P (f (x, c)). Even if the second assertion was Skolemized, conflict-driven instantiation would fail: since there is no ground instance of the Skolem term, no conflicting instance can be found.

Trigger-Based Instantiation. This instantiation scheme works by matching triggers with the current ground model. Triggers associate with every box ∀x. ϕ ∈ Q one or more lists of quantifier-free terms t 1 , . . . , t n such that free(t 1 ) ∪ • • • ∪ free(t n ) = {x}. The triggers are either provided by the user or are heuristically generated. Trigger inference uses the structure of the quantified formulas which is preserved by preprocessing. To construct instances of ϕ, trigger-based instantiation searches for substitutions σ and terms g 1 , . . . , g n ∈ T (G) such that G EUF t i σ ≈ g i . If the search is successful, it returns the instance ϕσ.

The process of matching terms within the theory of equality and uninterpreted functions is called E-matching [START_REF] Detlefs | Simplify: A theorem prover for program checking[END_REF][START_REF] Ge | Solving quantified verification conditions using satisfiability modulo theories[END_REF][START_REF] De Moura | Efficient E-matching for SMT solvers[END_REF]. Due to the heuristic nature of triggerbased instantiation, the generated instances might not be useful to solve the problem. Instead they can slow down or mislead the solver.

In the case of Example 1, a trigger P (x) on assertion 1 would produce the useless instance P (c) → P (f (c, c)) and a trigger P (f (x, c)) initially cannot match anything. The trigger P (y) on assertion 2 would produce the instance (∀z. P (z) → P (f (z, c))) → ¬P (c). This instance is a step towards solving the problem: the strong variable z is no longer below a quantifier and will be Skolemized to create the formula P (s 1 ) → P (f (s 1 , c)) → ¬P (c) where s 1 is a fresh constant. During the next instantiation round the trigger P (x) on assertion 1 generates the instance P (s 1 ) → P (f (s 1 , c)) which leads to the contradiction.

This technique is very sensitive to the availability of the right ground terms in the ground model. In the above example, if the formula contained ∀x. P (x) instead of P (c), trigger-based instantiation would have been helpless.

Enumerative Instantiation. While conflict driven instantiation is guided by the ground model it tries to contradict, and trigger-based instantiation is guided by the triggers, enumerative instantiation [START_REF] Reynolds | Revisiting enumerative instantiation[END_REF] is unguided. For a box with the form ∀x. ϕ ∈ Q it creates all substitutions [ t/x] where the terms t are ground terms from T (M). To limit the number of generated instances the procedure only uses the ground terms minimal with respect to some term order and does not return instances already implied by the ground model (i.e., it only returns ϕσ if G EUF ϕσ). Enumerative instantiation ensures the theoretical completeness of the SMT solver for the theory of uninterpreted functions. It can also find the small ground terms that are sometimes necessary to enable the two previous techniques to work, and is thus a useful fallback strategy.

For Example 1, enumerative instantiation also needs at least two rounds. First, the variable y of assertion 2 is instantiated with c. Then, after Skolemization, assertion 1 can be instantiated with the new Skolem constant. Eventually, the cooperation of enumerative instantiation and the above techniques would succeed. However, in presence of many ground terms of the same sort as c, enumerative instantiation might have needed a lot of time to find the right instance.

Model-Based Quantifier Instantiation. Finally, model-based quantifier instantiation [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF] extends heuristically the ground model M to a first-order interpretation I and tests if this interpretation is a model: if there exists a box of the form ∀x. ϕ ∈ Q and a substitution σ of x with terms from T (G) such that I ¬ϕσ, then M is not a true model of P and the ground instance ϕσ is produced. If this is not the case, then I is a model of P and the input problem is satisfiable. This methods works for every fragment that has the finite model property.

For Example 1, model-based quantifier instantiation fails to generate the right instances in one round for the same reason that trigger-based and enumerative instantiation fail: it might instantiate assertion 2 with c for y, but other rounds of instantiations will still be required to reach a contradiction.

Quantifier Simplification by Unification

The essence of our technique is to simplify boxes by replacing a quantified subformula of the box with the Boolean constant or ⊥. This can be done if the matrix of this quantified subformula can be unified with the matrix of a unit-box.

Example 3. On our running Example 1, the first assertion serves as unit-box, whose matrix is unifiable with the matrix of the box in the second assertion. As a result, the quantified subformula can be reduced to the Boolean constant , for some instance of the second formula.

∀x. P (x) → P (f (x, c)) ∀y. (∀z. P (z) → P (f (z, y))) → ¬P (y) → ¬P (c)
The rewriter simplifies the formula → ¬P (c) to ¬P (c). Notice that, in this example, the variable z must be Skolemized because its quantifier is strong.

The SUB rule (Section 3.1) formalizes this derivation. An SMT solver can use this rule to augment the problem with simplified formulas. It is carefully restricted to generate formulas which help the instantiation procedures (Section 3.2). In Section 3.3 we propose several variants of the rule with different tradeoffs.

The Core Rule

The simplification by unification of subformulas (SUB) rule simplifies a box by replacing a quantified subformula with a Boolean constant. To be able to do so, the rule unifies the matrix of the subformula with a unit-box using a substitution. The Boolean constant depends on the polarities of the matrices: if they have the same polarity the subformula is replaced by , if they have different polarity it is replaced by ⊥. The conclusion of the rule is the pre-simplified formula and will be fully simplified by the rewriter.

Definition 1 (SUB Rule). ∀x 1 , . . . , x n . ψ 1 ∀x n+1 , . . . , x m . ϕ[Qȳ. ψ 2 ] SUB ∀x k1 , . . . , x kj . ϕ[b]σ
where Q ∈ {∃, ∀}, the subformula Qȳ. ψ 2 appears only below the outermost universal quantifier of ϕ, and σ is a substitution. The rule is subject to the conditions:

1. trim(ψ 1 )σ = trim(ψ 2 )σ, if Qȳ. ψ 2 is weak; 2. trim(ψ 1 )σ = trim(sk(Qȳ. ψ 2 , x n+1 . . . x m ))σ, if Qȳ. ψ 2 is strong; 3. The bound variables of the conclusion {x k1 , . . . , x kj } are exactly free(ϕ[b]σ); In this case, the rewriter will simplify the pre-simplified formula G(c) ∧ ⊥ to ⊥ and the SMT solver can directly deduce unsatisfiability.

4. b = if pol(ψ 1 ) = pol(ψ 2 ) or b = ⊥ if pol(ψ 1 ) = pol(ψ 2 ).
The SUB rule allows us to simply combine and restrict Skolemization, unification, and the replacement of subformulas with the appropriate constant. In the next section we will see the role it has within an SMT solver. The rule soundly combines these sound steps. First, it Skolemizes the variables ȳ. Second, it applies the unifier σ. Now the subformula of ψ 1 corresponding to Qȳ. ψ 2 in the SUB rule is equivalent to trim(ψ 1 )σ and is replaced with a Boolean constant. The constant is chosen appropriately according to the polarity of the formulas. This replacement is sound since ψ 1 σ always holds. Overall, the SUB rule, together with applying the rewriter, somewhat resembles unit resolution where ∀x 1 , . . . , x n . ψ 1 is the unit clause. In the case of SMT solvers, however, ϕ might not be a clause. Furthermore, ψ 1 and ψ 2 will have the complex structure that is preserved from the input, since most currently used instantiation techniques have no advantage from applying full clausification.

The Simplification Within the SMT Solver

Since the SUB rule eliminates a quantified subformula, the conclusion is easier to handle for the SMT solvers. In general, however, the conclusion does not subsume the box serving as the second premise. Hence, this box cannot simply be replaced by the conclusion. Instead, the problem must be augmented with the derived box. As the evaluations show, augmenting the problem still helps the SMT instantiation procedures to find the appropriate ground instances. The pseudocode in Figure 2 shows the loop which augments the problem. It is executed after preprocessing finishes and before the ground solver starts. The procedure first iterates over the clauses in the preprocessed problem P to build a set I of unit-boxes (Line 4) which can be used to simplify quantified subformulas. At the same time, this loop collects in a queue Q all clauses containing boxes (Line 5). Then the procedure takes a clause from the queue and tries to simplify one of its boxes. To do so, it uses the SUB rule. If this succeeds, the conclusion is the pre-simplified formula. The procedure then uses the rewriter to finish the simplification and the problem is augmented with the simplified formula by adding it conjunctively to the problem (Lines 8 to 11). If the simplified clause still contains a box, it is pushed back onto the queue (Line 13).

I ← ∅ Q is an empty queue. for each clause C in P do 4 if C is unit-box with the box then I ← I ∪ { } 5 if C contains a box then push(Q, C) while Q is not empty do 1 ∨ • • • ∨ n ← pop(Q) 8 if there is ψ ∈ I and a box i such that ψ i SUB then 9 ← rewrite( ) 10 C ← 1 ∨ • • • ∨ i-1 ∨ ∨ i+1 ∨ • • • ∨ n 11 append C to P if C contains a box
The procedure terminates since the queue Q will eventually be empty. Every iteration removes a clause from the queue and adds at most one new clause. When the test in line 8 fails, i.e., the SUB rule can not be applied, no new clause is added. Otherwise, it adds a clause with fewer nested formulas that can serve as Qȳ.ψ 2 in the SUB rule. Hence, the SUB rule will eventually no longer apply to any box left in the clauses in Q.

The approach of augmenting the problem with derived, but new, formulas bears the risk that the instantiation procedures create more useless ground instances from the new formulas. To minimize this risk, the SUB rule is restricted to only apply when the result is likely to be helpful. First, the detection of subformulas which can be eliminated only uses unification instead of a more general approach. Since preprocessing preserves the structure of quantified formulas, unifiability can indicate the intention of the user. For example, the unit-box might be a lemma that is used within the box that is simplified. Second, the first premise must be a box. In principle it could also be a ground literal, but ground literals are already directly usable by the ground solver. Third, the simplified subformula must start with a quantifier because the instantiation procedures struggle to instantiate the quantified subformula. One of the variants described in the next section drops this restriction, but it is not as useful as the restricted rule.

Variants

As the experimental evaluation (Section 5) shows, the above version of quantifier simplification by unification solves more instances at little cost. Nevertheless, we also developed several variants with different tradeoffs. We will call quantifier simplification by unification as presented so far the normal variant and will often drop the phrase by unification to avoid repetition.

Eager Simplification. Since quantified subformulas block the instantiation procedures from creating the right instances quickly, the SUB rule is restricted to only simplify quantified subformulas. This restriction, however, can be removed to generate more simplified formulas. The eager SUB rule is the rule

∀x 1 , . . . , x n . ψ 1 ∀x n+1 , . . . , x m . ϕ[ψ 2 ]
eager-SUB ∀x k1 , . . . , x kj . ϕ[b]σ and all side conditions of SUB are changed to read ψ 2 in-place of Qx. ψ 2 .

The eager SUB rule can be applied on any subformula not below an extra quantifier. On the one hand, this corresponds to deriving general consequences of unit-boxes in full first-order logic, but on the other hand, it will generate many more new formulas which potentially slow down or misguide the solver. Solitary Variable Heuristic. To limit the potential downsides of eager simplification, we can limit the cases when the rule is applied: we apply the rule when it potentially removes a variable from the outermost quantifier of the second premise. The resulting formula will produce fewer misleading instances.

A variable is removed from the pre-simplified formula if it is solitary: it appears in the subformula ψ 2 , but not in any other subformula of ϕ. Hence, for example, in the case

ϕ = t 1 ∨ • • • ∨ t i ∨ • • • ∨ t n we apply the rule with ψ 2 = t i if there is a variable x ∈ free(t i ) such that x ∈ free(t 1 ∨ • • • ∨ t i-1 ∨ t i+1 ∨ • • • ∨ t n ).
Deletion of Simplified Clauses. Another way to restrict the number of newly created instances is to delete the clause that contains the box used as the second premise of the SUB rule after it has been simplified. While this is no longer complete, it can guide the solver towards solving the refutation problem. Especially, within a strategy schedule this can be a valuable strategy.

This variant can be combined with the three other variants. Overall, this results in six variants of quantifier simplification. The amount of clauses deleted depends on the activity of the simplification variant used. Especially in the case of eager simplification with deletion many input assertions will be deleted.

Implementation

Our implementation of quantifier simplification by unification in veriT uses a nonperfect discrimination tree as term index and a subsequent unifiability check (Section 4.1). Both steps are amended to take strong variables into account without explicit Skolemization and avoid the creation of unnecessary Skolem symbols.

The implementation also does not apply the simplification of clauses everywhere, but focuses on unit-boxes only: the queue Q will only be populated by unit-boxes. This simplifies the implementation, since we do not have to track which boxes of a clause have already been simplified. It indeed appears that in SMT-LIB benchmarks clauses with boxes are uncommon and quantified formulas are usually unit-boxes (e.g., quantifiers range over entire disjunctions). A prototype without this simplification did not perform better on these benchmarks than the simplified version.

Indexing and Unification Without Skolemization

A key element to execute quantifier simplification, as shown in the algorithm in Figure 2, is the lookup of the unit-box ∀x. ψ 1 from the index I. The trimmed matrix of this box must be unifiable with the trimmed matrix of the quantified subformula Qȳ. ψ 2 . To implement the search for unifiable formulas efficiently we use a term index. We use non-perfect discrimination trees [START_REF] Sekar | Term Indexing[END_REF]. Non-perfect means that the lookup is an over-approximation: some returned terms are not unifiable with the query term and must be removed by a full unification step.

For each unit-box ∀x. ψ 1 (of I in the algorithm in Figure 2) the index stores trim(ψ 1 ) together with pol(ψ 1 ). For each possible subformula Qȳ. ψ 2 the implementation uses trim(ψ 2 ) as a query term and retrieves unification candidates and their polarity. Afterwards, it performs a full unification to construct the substitution σ when possible. If, however, the quantifier of Qȳ. ψ 2 is strong, the subformula should be Skolemized.

To handle variables that would be replaced by Skolem terms, the lookup process is enhanced: while normal variables are replaced by a variable placeholder that can match any term, variables to be Skolemized act like constants and can not match any other term. This embeds Skolemization into indexing, since Skolem terms start with fresh function symbols that can never match indexed terms.

After the index returns a filtered set of possible premises trim(ψ 1 ) with their polarities pol(ψ 1 ) from I, the implementation must use full unification [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] to eliminate false positives and to build the unifier σ. It has to solve the unification problem between trim(ψ 1 ) and trim(ψ 2 ), where trim(ψ 2 ) can contain variables that must be Skolemized.

To handle Skolemized variables during unification, our implementation deviates from the standard version in two ways. First, similarly to the term index, it handles Skolemized variables as constants. Second, it considers a Skolemized variable as an occurrence of all the variables its Skolem term would depend on.

The resulting unifier σ cannot substitute a Skolem term into the quantified variables x n+1 , . . . , x m of the box that is simplified. Hence, the conclusion ϕ[b]σ is free of any Skolem terms, and no Skolem term has ever to be constructed. Overall, restricting quantifier simplification by unification to not simplify formulas below multiple nested quantifiers allows for this elegant implementation.

Evaluation

This section presents an empirical evaluation of quantifier simplification by unification and its variants as implemented in veriT. 3 The default variant of quantifier simplification solves more benchmarks than the default configuration of veriT, while losing few benchmarks. This justifies the activation of our quantifier simplification method in the default configuration. Almost all other variants also solve more benchmarks than the default configuration. veriT exposes a wide range of options to fine-tune the instantiation module. A specific configuration is a strategy. Quantifier simplification solves benchmarks not solved by any veriT strategy without this technique (Section 5.1).

In order to fully benefit from the strategies available, veriT can use strategy schedules. We generated strategy schedules with and without quantifier simplification and evaluated their performance. The strategies with quantifier simplification are an integral component of the generated schedules and increase the number of solved benchmarks. They are especially useful for short timeouts (Section 5.2).

We performed the experiments on the benchmarks from the SMT-LIB benchmark release 2021 [START_REF] Barrett | The SMT-LIB Standard: Version 2.6[END_REF]. Since quantifier simplification is only relevant for first-order formulas, we used the SMT-LIB logics supported by veriT which use quantifiers, uninterpreted functions, or arrays. Those are the SMT-LIB logics UF, UFLRA, UFLIA, UFIDL, ALIA, AUFLIA, and AUFLIRA. Since veriT is purely refutational, we removed benchmarks known to be satisfiable from the analysis. 4 Overall, the SMT-LIB contains 41 129 benchmarks using these logics. Of those, 1206 benchmarks are known to be satisfiable. This leaves 39 923 relevant benchmarks. We used the 2021.06-rmx release of veriT.

To interpret the numbers, the reader should keep in mind that veriT has no array solver. It treats the functions of the SMT-LIB theory of arrays as uninterpreted functions. Since veriT is restricted to refute benchmarks, this approach is sound. Nevertheless, veriT can fail to solve easy benchmarks that require array reasoning.

All experiments have been performed on computers with one Intel Xeon Gold 5220 processors with 18 cores and 96 GiB RAM. We ran one instance of veriT per available core and used a memory limit of 6 GiB per instance.

Baseline Comparison

Table 1 shows the number of benchmark solved within a timeout of 180 s in comparison to the default strategy. The standard version of quantifier simplification by unification is denoted N, eager simplification is denoted E, and the solitary variable heuristic is denoted S. A suffix d denotes the deletion of simplified clauses. Benchmarks are "Gained" if they are not solved by the default strategy and "Lost" if they are solved by the default strategy, but not by the variant. The column "Total" reports the union of the benchmarks solved by all variants.

The normal variant shows a good improvement by solving 237 benchmarks more. Most other variants solve more benchmarks not solved by the default strategy, but also lose many more. While the normal variant does not have the highest gain, the small loss justifies enabling it in the default strategy of veriT. The huge number of lost benchmarks for the variants that combine eager simplification and the solitary variable heuristic with clause deletion is not surprising: since most input assertions can be simplified in some way, clause deletion removes much of the original problem. The result is often an unsolvable problem.

Compared to the union of benchmarks solved by any existing veriT strategy (Theoretical Best), quantifier simplification by unification shows good improvement. We used a list of 43 strategies which are also used by veriT in the SMT competition. 5 The default configuration of veriT is on this list. Overall, the variants together are able to solve 125 benchmarks that veriT could not solve before. While eager simplification solves only 80 more, 18 of those are not solved by any other quantifier simplification variant. Here, the two variants with clause deletion that have a huge loss are somewhat redeemed: together they solve eight benchmarks not solved by the theoretical best solver and the other quantifier simplification variants. To perform the quantifier simplification, veriT does not need much time: for the normal variant, we measured a median runtime of 0.5 ms and mean of 3 ms.

Strategy Scheduling

Since quantifier instantiation relies on heuristics, veriT exposes parameters that can be set by the user in a strategy. Most benchmarks are solved by an appropriate strategy within a short timeout. Hence, it is sensible to execute many strategies for short time intervals one after another in a schedule.

To evaluate the quantifier simplification technique within a strategy schedule, we generated schedules with and without strategies extended with quantifier simplification. An optimal schedule is the set of strategy-timeout pairs which solves the most benchmarks. The list of possible strategies and timeouts is handcrafted. We use integer programming to solve this optimization problem. veriT itself uses the logic of the problem to select a schedule.

To build strategies with quantifier simplification we picked six strategies from the strategy list of 43 strategies: the default strategy, the strategy that solved the most benchmarks overall, and four complementary strategies. The four complementary strategies were selected by finding a pair of strategies that together with the best strategy maximize the number of solved benchmarks. We searched such a pair on all logics and on first-order logic with equality (UF) alone. We then extended these six strategies with the six variants of quantifier simplification. This resulted in 36 new strategies.

We generated schedules optimized for timeouts of 180 s and 24 s. The short 24 s timeout allows us to evaluate the value of quantifier simplification for applications such as interactive theorem provers, which require a short timeout. It corresponds to the timeout used by the SMT competition to evaluate solvers for this purpose. The longer 180 s timeout was arbitrarily chosen.

Figure 3 shows the number of benchmarks solved within a time limit on UF alone and on all logics. On all logics, the schedule with quantifier simplification solved 193 benchmarks more after 24 s than the original 24 s schedule. For the 180 s timeout, the 180 s schedule with quantifier simplification solves 191 more than the one without. The 24 s schedule with quantifier simplification solves 18 benchmarks more than the 180 s schedule after 180 s. Hence, quantifier simplification is very useful for short timeouts. Since the form of quantified lemmas that quantifier simplification by unification eliminates appear in problems generated by interactive theorem provers, it is especially useful for this application.

To provide context the plots contain the results of two other systems: the state-of-the-art SMT solver CVC4 and the superposition prover Vampire [START_REF] Kovács | First-order theorem proving and vampire[END_REF]. We used the official builds of version 1.8 of CVC4 and version 4.5.1 of Vampire. Vampire includes the SMT solver Z3, which aids theory reasoning. Since CVC4 has no scheduler optimized for 24 s or 180 s, we ran the default strategy. 6 For Vampire we used the SMT-COMP scheduler with a timeout of 180 s. 7 We discarded all "satisfiable" results. Overall, CVC4 solves 70 benchmarks more than veriT with quantifier simplification after 24 s and 26 after 180 s. veriT with quantifier simplification after 180 s solves 595 benchmarks not solved by CVC4, of which 107 are also not solved by veriT without quantifier simplification. Surprisingly, Vampire solves fewer benchmarks than any other system on UF. This is due to the nature of typical SMT benchmarks: they usually require little quantifier reasoning and are hence easier to solve for instantiation-based systems. 8 This confirms that restricted methods, such as quantifier simplification by unification, are useful for SMT problems. Figure 4 visualizes the schedules for the logic UF. Grey cells are strategies that use quantifier simplification. Cells with the same number use the same base strategy. Some base strategies appear both in the schedules with and without quantifier simplification. The strategies with quantifier simplification tend to be used for shorter time slices than the variants without.

Conclusion

We presented a new unification-based simplification technique for instantiationbased SMT solvers. Its design is motivated by limitations of modern instantiation methods, and it is efficient. Problems where formulas can be simplified are often solved much faster, despite the method creating new quantified formulas. We plan to enable quantifier simplification by unification by default in the next veriT release. The release will also produce machine-checkable proofs for simplifications performed by quantifier simplification by unification. We believe that the technique implemented here within veriT can be ported easily into any instantiation-based SMT solver, and we are confident that it would also enable mainstream solvers to tackle problems outside of reach with other current strategies. We will investigate its potential in other solvers.

Our method is a step towards using techniques inspired by resolution-based theorem provers within SMT solvers. It is currently only used as a preprocessing technique, but we plan to investigate novel quantifier instantiation techniques which can directly handle nested strong quantifiers.

Example 4 . 2 ) 7 .

 427 In the running example the subformula ∀z. P (z) → P (f (z, y)) occurs negatively. Since Q = ∀, the formula must be Skolemized (Condition 2): sk(∀z. P (z) → P (f (z, y)), y) = P (s 1 (y)) → P (f (s 1 (y), y))Hence, the unifier used in Example 3 is σ = [s 1 (c)/x][c/y].Example 5. Ignoring Skolemization (Condition 2) leads to unsoundness:∀x. P (x, x) ∀y. ¬(∀z. P (y, G(z))) ¬The result of Skolemization sk(∀z. P (y, G(z)), y)) = P (y, G(s 1 (y))) is not unifiable with P (x, x). The rule is not applicable. Example 6. The conclusion can contain variables from both premises. Here the unifier is σ = [G(x)/y 1 ][c/z]. ∀x. P (G(x), c) ∀y 1 , y 2 . (∀z. P (y 1 , z)) ∧ P (y 1 , y 2 ) SUB ∀x, y 2 . ∧ P (G(x), y Example The above examples were cases where pol(ψ 1 ) = pol(ψ 2 ). This example illustrates the other case: ∀x. ¬P (x, x) ∀y. G(c) ∧ (∀z. P (y, z)) SUB G(c) ∧ ⊥

Fig. 2 .

 2 Fig. 2. The augmentation procedure.

Fig. 3 .

 3 Fig. 3. CDF of different schedules on UF only and all logics.

Fig. 4 .

 4 Fig. 4. Visualization of optimized UF schedules. The bottom rows are the schedules with quantifier simplification. The numbers denote the base strategies.

Table 1 .

 1 Comparison with the default strategy and the theoretical best solver on 39 923 benchmarks.

	vs. Default (solves 31 690)	N	E	S	Nd	Ed	Sd	Total
	Solved	31 927 31 772 31 928 31 733 21 405 21 823 32 151
		+237	+82 +238	+43 -10 285 -9 867 +461
	Gained	282	315	285	291	115	255	475
	Lost	45	233	47	248 10 400 10 122	14
	vs. Theoretical Best (solves 32 633)
	Gained	83	80	85	86	32	76	125

The raw data is available on Zenodo [?].

Benchmarks known to be satisfiable can identify soundness problems. Hence, we included them in the experiments, but removed them from the data.

Competition website: https://smt-comp.github.io/

Using: -L smt2.6 --no-incremental --no-type-checking --no-interactive --full-saturate-quant

Using: -t 180s -m 6000 --mode portfolio --schedule smtcomp --input syntax smtlib2 -om smtcomp -p off

This has been confirmed to us by the Vampire team in conversations.

Acknowledgments. We are grateful to Haniel Barbosa, Jasmin Blanchette, Daniel El Ouraoui, Mathias Fleury, Martin Riener, and Athénaïs Vaginay for many fruitful discussions and suggestions to improve the text. We thank the anonymous reviewers for many good suggestions to improve the text. The second author has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations (see https://www.grid5000.fr).


Hossien B Eldeeb

Sreelal Maravanchery

Volker Jungnickel

Peter Hellwig

Jonas Hilt

Murat Uysal

S Mana

Distributed MIMO for Li-Fi: Channel Measurements, Ray Tracing and Throughput Analysis

Keywords: Li-Fi, multiple-input multiple-output, channel measurements, ray tracing, throughput analysis

LiFi has been considered as a promising candidate for future wireless indoor networks. The IEEE P802.15.13 and P802.11bb standardization groups agreed upon channel models generated using the non-sequential ray tracing approach of OpticStudio. In this paper, in order to validate the channel modelling approach, at first 2 × 2 multiple-input multiple-output (MIMO) channel measurements are carried out over 200 MHz bandwidth using a channel sounder. The experimental scenario is also modeled in 3D by applying ray tracing. The obtained results indicate good agreement between simulations and measured channel impulse responses, from which parameters such as path loss and delay spread are derived. After validating the channel modeling approach, we investigate the singular values and the effect of user mobility onto the performance in a 4 × 4 distributed multi-user MIMO scenario.

I. INTRODUCTION

N OWADAYS, light fidelity (LiFi) is gaining increasing attention with attractive features such as operation in unregulated spectrum and robustness to electromagnetic interference [START_REF] Ghassemlooy | Emerging optical wireless communicationsadvances and challenges[END_REF]. Both visible light (VL) and infrared (IR) wavelengths can be used to design LiFi systems where VL may be used to offload downlink traffic while the near-IR is commonly used in the uplink for bi-directional connectivity.

Initial works on LiFi channel modeling are mainly based upon computer simulations, see e.g., the survey in [START_REF] Al-Kinani | Optical wireless communication channel measurements and models[END_REF] and references therein. In particular, non-sequential ray tracing can be used to realistically model LiFi channels. The IEEE 802.15.13 and 802.11bb standardization groups agreed upon the reference channel models generated by a non-sequential ray tracing approach [START_REF]IEEE 802.15. 7r1 reference channel models for visible light communications[END_REF]. This approach makes possible to obtain the channel impulse response (CIR) for complex geometries. For a precise modeling of the light propagation, it takes into account multiple reflections as well as the wavelengthdependent reflectance of the surfaces and different types of reflections (i.e. specular, diffuse, mixed).

In more recent works [START_REF] Wei | Experimental demonstration of a cubic-receiver-based MIMO visible light communication system[END_REF]- [START_REF] Mana | Distributed MIMO experiments for LiFi in a conference room[END_REF], experimental measurements of LiFi channels are reported. For example, in [START_REF] Wei | Experimental demonstration of a cubic-receiver-based MIMO visible light communication system[END_REF], a demonstration of a MIMO LiFi system using a cubic receiver has been proposed showing that cubic receiver design reduces the correlation of the MIMO channel matrix. A field measurement for MIMO LiFi in a manufacturing cell has been reported in [START_REF] Berenguer | Optical wireless MIMO experiments in an industrial environment[END_REF] showing that deployment of multiple distributed links allows spatial diversity and reduces the impact of shadowing and blockage to increase the robustness of LiFi systems. In [START_REF] Mana | Distributed MIMO experiments for LiFi in a conference room[END_REF], it was demonstrated that a similar setting can also be used to transport multiple data streams to multiple users in parallel. Measurements require dedicated hardware and costly equipment while characterizing LiFi channels with a realistic simulation methodology is more flexible. However, verification of the simulation approach is required, at least in few exemplary scenarios.

In an effort to validate the non-sequential ray tracing approach adopted by the IEEE, we conducted a measurement campaign in [START_REF] Eldeeb | Channel modelling for light communications: Validation of ray tracing by measurements[END_REF] and demonstrated that the results of simulations and measurements were in a good agreement. However, the considered Li-Fi scenario was limited to an empty room and single transmitter (TX) and single receiver (RX). In this letter, we extend our results to multiple-input multiple-output (MIMO) scenarios. Specifically, we consider a multiuser MIMO link between two distributed optical frontends and two mobile users in a furnished conference room [START_REF]Channel measurements and ray tracing simulations for mimo light communication at 200 MHz[END_REF]. Results are used to validate the ray tracing approach for MIMO and to calculate channel parameters like path loss and delay spread. Next, we investigate the singular values and the channel throughput in a modelled 4 × 4 MIMO LiFi scenario. Moreover, we investigate the effect of user mobility on the overall throughput. The results show that the throughput depends on singular values and the SNR of each user at its individual position.

II. SIMULATION METHODOLOGY

In this section, we explain the channel modeling approach. Firstly, the 3D simulation model of the test environment (see Fig. 1.) is created in OpticStudio platform. Then, we import the CAD models of the objects (i.e., tables, tripods, chairs, etc.) inside the environment. Next, coating materials of each CAD object are defined by specifying the wavelengthdependent reflectance as well the type of reflection (i.e., specular, diffuse, and mixed). The light source specifications include total optical power, power spectral intensity, radiation pattern, and a number of emitted rays. The photodiode (PD) specifications contain sensitive area, field-of-view (FoV), and directivity. In the simulated environment, non-sequential ray tracing is performed to obtain the path length and the power of each ray emitted by the light source and absorbed by the PD. The statistics of the received photons versus their arrival time is imported into MATLAB for further processing. In this way, the simulated channel impulses responses (CIRs) for each link in the MIMO Li-Fi system are obtained as

h ij (t) = N ij n = 1 P ij (n) δ t -τ ij (n) , (1)
where N ij is the number of rays emitted from the j th TX and received by the i th RX and δ is the Dirac delta function. For each TX j and each RX i, P (n) and τ (n) denote the optical power and the propagation delay of the n th received ray, respectively where n = 1, 2, . . . , N . The channel frequency response (CFR) for all links can be then calculated by taking the Fourier transform (FT) of (1). After obtaining the CIR and CFR, various channel parameters can be calculated such as the path loss and the RMS delay spread [START_REF] Al-Kinani | Optical wireless communication channel measurements and models[END_REF].

III. EXPERIMENTAL SETUP A channel sounder capable of measurements at frequencies of up to 250 MHz is used for our measurements. Transmission side consist of 8-channel arbitrary waveform generator (Spectrum DN 2.662-08) which generates the waveform and feed the signals to the optical TX frontends. After the wireless transmission, signals are received at the RX frontends and fed into the connected 8-channel digitizer (Spectrum DN 2.445-08). We followed the similar experimental approach as mentioned in [START_REF] Berenguer | Optical wireless MIMO experiments in an industrial environment[END_REF]. The power of each TX and the sensitivity of each RX are boosted by using multiple IR LEDs with same driver and multiple PDs and combining the signals after individual trans-impedance amplifiers, respectively. The TX frontend uses four OSRAM OSLON SFH-4715AS LEDs having optical power per LED of P T X = 1.3 W, centroid wavelength at 850 nm, and half power angle of 40°. The RX frontend consists of five HAMAMATSU-S6968 PDs with a high sensitivity around 850 nm and half directivity angle of 35°. Since TX and RX have wide beam-width and FoV, light is transmitted into and received from many different directions, which is good for mobile scenarios. However, it also includes more non-line-of-sight signals which tend to reduce bandwidth in realistic scenarios. The waveform used in the measurement is based on direct current orthogonal frequency-division multiplexing (DC-OFDM) as described in [START_REF] Berenguer | Optical wireless MIMO experiments in an industrial environment[END_REF]. The measured frequency response contains the response of one TX and one RX frontend. As in [START_REF] Eldeeb | Channel modelling for light communications: Validation of ray tracing by measurements[END_REF], the frontend responses calibrate out to retrieve the frequency response of the channel.

IV. VALIDATION OF RAY TRACING

In the accompanying simulation, we consider the same measurement setup carefully by considering the radiation pattern of LEDs, the effect of the RX directivity, wavelengthdependent reflectance of walls and objects inside the room, As shown in Fig. 2, the frequency responses depend on the distance between TXs and RXs. The shorter the transmission distance, the flatter is the frequency response. For TX1 (which is located 0.6 m closer to both RXs), the channel is nearly flat up to 150 MHz. A flat channel is obtained at lower frequencies when using TX0 but there is more ripple above 120 MHz due to the longer transmission distance. Note, there is some ripple above 120 MHz in the measured results which is also present in simulation results. This is attributed to multipath components, accordingly, which become more significant with respect to the line-of-sight component if distance gets larger. Hence, when considering wideband LiFi channels over longer distances, it becomes increasingly important to include the multipath effects. It is obvious from Fig. 2 that results of both the amplitude and phase responses obtained from the simulations are in a good agreement with the measurements. Considering the flat part of the CFR, i.e., frequencies below 120 MHz, the simulation results have an average difference of 0.5 dB with respect to the measurements.

V. THROUGHPUT ANALYSIS

Since these results clearly validate the simulation methodology, we can use it further to investigate more complex scenarios. We consider broadband MIMO channels at frequencies up to 100 MHz and deploy the DC-OFDM approach with frequency points of N S . Similar to RF, the channel is characterized based on singular value decomposition (SVD) of the MIMO channel matrix [START_REF] Chaaban | Capacity bounds and high-SNR capacity of MIMO intensity-modulation optical channels[END_REF]. SVs represent the amplitude of the signals transmitted in parallel in a MIMO link. Generally, for a Li-Fi system with N T transmitters and N R receivers, the received signals can be represented as

Y = HS + Z, where S = (s 1 , • • • , s N T )
T is the transmitted

ηavg = NT NRNS N T j = 1 N R i = 1 N S k = 1 |H ijk | 2 . (2)
Let P r is the received power at one RX and P N oise is the noise power. The transmitted power (P T X ) to noise ratio is given by [START_REF] Jungnickel | Capacity measurements in a cooperative MIMO network[END_REF] PT

X PNoise = Pr ηavgPNoise = γ0 ηavg . (3)
Finally, the channel throughput of the MIMO Li-Fi system based on DC-OFDM and SVs can be obtained by [START_REF] Jungnickel | Capacity measurements in a cooperative MIMO network[END_REF] CMIMO =

N S k = 1 ∆B k • Γ j = 1 log 2 1 + γ0 NT ηavgζ • λ 2 j,k , (4)
where ∆B k = 122 kHz denotes the bandwidth occupied by k th subcarrier. In (4), we include an empirical scaling factor of ζ = 10 to consider the impairments such as the non-linear distortions and the imperfect constellation shaping.

VI. RESULTS AND DISCUSSION

A. Channel Parameters

The path loss is critical for link budget calculations and optimized system design. The results of all measured MIMO links are presented in Fig. 3(a). As expected, the corresponding path loss of both RXs with respect to TX1 (i.e., TX1-RX0 and TX1-RX1) is lower than the corresponding path loss to TX0. For example, RX1 is located 0.6 m closer to TX1. The path loss values are given as 14.8 dB and 17.2 dB with respect to TX1 and TX0, respectively, i.e. the longer the propagation distance, the larger is the path loss. In furnished rooms, multiple copies of the signal reach the receiver which cause different paths with different power levels and different delays. The temporal dispersion is characterized by the RMS delay spread. It is plotted for each link in Fig. 3(a). The RMS values are given as 12.1 ns and 12.8 ns for TX1-RX1 and TX0-RX1, respectively. Obviously, the delay spread is correlated with the path loss, i.e., higher path loss implies higher delay spread. Note that RMS values are limited by the limited of the channel sounder, which widens all pulses in the CIR.

B. Singular Values

In Fig. 3(b), at first, we investigate the SVs of the 2 × 2 MIMO scenario considered in the measurements (i.e., N R = N T = Γ = 2). There is only one strong SV, i.e. only one data stream can be transmitted in the same time slot, at least for low SNR. The main reason is that TX1 was nearer to RX1 and RX2 so that the corresponding column in the channel matrix dominates the result. Nonetheless, because the methodology is validated in Section IV, now we can investigate more flexible Txs and RXs positions by means of channel modeling and learn more about more complex MIMO scenarios. As shown in Fig. 4, therefore we consider a 4 × 4 MIMO LiFi setup (i.e., N R = N T = Γ = 4) in a furnished conference room. The four TXs are installed near the ceiling at 2.9 m height uniformly distributed in the room in order to achieve homogeneous coverage. The users are kept at the table-top height facing towards the ceiling. We further consider that users are moving along specified trajectories inside the room with a step size of 0.5 m. In Fig. 4, we investigate the SVs for specific user positions denoted by Sc 1, Sc 2, Sc 3, and Sc 4. In Sc 1, the four users (i.e., U1, U2, U3, and U4) are located at a room corner near TX1 with short separation of 0.5 m between each other. In Sc 2, the users become more separated, so that two users (i.e., U1 and U4) are located near TX1 while the other two users (i.e., U2 and U3) are near TX2. In Sc 3, U4 moves away from TX1 but nearer to TX4. Finally, in Sc 4, each user moves near to a different TX as shown in Fig. 4.

The singular values (λ 1 , λ 2 , λ 3 , λ 4 ) are calculated at each frequency bin up to 100 MHz as shown in Fig. 5. In Sc 1 (see Fig. 5(a)), there is only one strong SV allowing only one data stream to be transmitted in the same time slot. In Sc 2 (see Fig. 5(b)), there are two strong SVs i.e. two parallel data streams are supported. In Sc 3 (see Fig. 5(c)), three strong SVs are observed. In Sc 4 (see Fig. 5(d)), a full rank of the MIMO channel matrix is achieved with four strong SVs. The results in Fig. 5 show that the principal experimental findings in [START_REF] Mana | Distributed MIMO experiments for LiFi in a conference room[END_REF] can be confirmed by means of ray tracing.

C. Throughput

The achievable throughput for the four MIMO Li-Fi scenarios versus the SNR is shown in Fig. 6(a), where SNR is considered constant, i.e., Foschini's formula (4) is used. It is observed that increasing the number of parallel streams results in a steeper slope of throughput particularly at high SNR. The throughput is significantly higher at any SNR if the channel allows spatial multiplexing. The throughput in Sc 1, Sc 2, Sc 3, and Sc 4 is given as 233, 309, 334, and 385 Mbit/s at SNR=10 dB and 542, 891, 1.070 and 1.320 Mbit/s at SNR=20 dB, respectively. Next, we consider the mobility of the users. If users are moving along the specified trajectories in Fig. 4, this implies variations on the optical path loss what has to be included in the throughput results. Thus, the assumption of fixed SNR becomes invalid. Therefore, we utilize the fundamental throughput formula [10, Eq.( 2)] to evaluate the throughput results keeping only P T X as a fixed value. Fig. 6(b) illustrates the effect of mobility, where we present the channel throughput versus distance (i.e., moving steps along the trajectories). These results reveal that the user mobility creates noticeable variation of the throughput. Decrease and increase of the throughput are observed if users meet near TXs and when they are mode separated, respectively. The latter case yields more significant SVs available for spatial multiplexing. For example, at the beginning (i.e., distance ≤ 1 m), only a small throughput is possible because all users locate around TX1. With only one moving step (i.e., distance of 1.5 m), an increase of 360 Mb/s of the throughput is observed, because U2 and U3 move closer to TX2 allowing the transmission of two parallel data streams. Another example, when the distance increases from 4 m to 4.5, the throughput climbs up by 396 Mb/s as 3 strong SVs become available. We notice that the throughput at 1.5 m with 2 SVs is 160 Mb/s higher than at 4.5 m which has 3 SVs. This is attributed to the reduced SNR when users move farther away from the TXs. Therefore, in the real-world MIMO LiFi network, it is important to take into account the possible number of parallel data streams and the SNR in order to maximize the throughput. Besides the sum throughput considered here, advanced schedulers will take other metrics, like individual user rates, fairness among the users, latency and robustness into account. These objectives are beyond the scope of this paper and would be interesting for future research.

VII. CONCLUSIONS

In this letter, we have used an experimental study of MIMO channels for LiFi to validate the channel models produced by non-sequential raytracing. Furthermore, we have investigated the performance. First, the measured channels have been compared to modelled ones between all TXs and all RXs. Results indicate a very good match for both, amplitude and phase responses over a wide bandwidth and confirm that raytracing creates very realistic LiFi channel models also when using MIMO with distributed optical frontends and multiple mobile users. We have analyzed the path loss and delay spread which show the well-known correlation, i.e. high path loss implies longer delay spread due to the diffuse multi-paths. Next, we have considered the performance of distributed MIMO links by means of the singular values and the achievable throughput. It was confirmed that the position of users has an essential impact on the singular values. The more distant the users are, the more significant singular values are observed, and the more streams can be supported in parallel. Finally, we investigated the effect of user mobility on the total throughput which is related to the singular values and the SNR of each user.

Fig. 1 .

 1 Fig. 1. Furnished conference room where measurements carried out.

Fig. 2 .

 2 Fig. 2. Channel frequency response (CFR) of simulations and measurements (a) Amplitude response and (b) Phase response.etc. to allow a one-to-one comparison between simulation and measurements. To validate the ray tracing, we compare both the amplitude and phase responses obtained from simulations and measurements. As shown in Fig.1, we consider a 2 × 2 distributed multiuser MIMO scenario in a furnished conference room with dimensions of (X × Y × Z) as 7.1 m × 5.8 m × 3 m. Two TX frontends (TX0 and TX1) are installed at the ceiling with a height of 2.9 m and separated by 2 m with respect to X axis. Two users represented by two laptop devices are located on table-top height (0.8 m) having their corresponding RX frontends (RX0 and RX1) located beside. Consider the center between TX0 and TX1 is reference point (X,Y) = (0, 0), the locations of RX0 and RX1 are then given as (0.65 m, 1.6 m) and (0.6 m, -1.6 m), respectively.As shown in Fig.2, the frequency responses depend on the distance between TXs and RXs. The shorter the transmission distance, the flatter is the frequency response. For TX1 (which is located 0.6 m closer to both RXs), the channel is nearly flat up to 150 MHz. A flat channel is obtained at lower frequencies when using TX0 but there is more ripple above 120 MHz due to the longer transmission distance. Note, there is some ripple above 120 MHz in the measured results which is also present in simulation results. This is attributed to multipath components, accordingly, which become more significant with respect to the line-of-sight component if distance gets larger. Hence, when considering wideband LiFi channels over longer distances, it becomes increasingly important to include the multipath effects. It is obvious from Fig.2that results of both the amplitude and phase responses obtained from the simulations are in a good agreement with the measurements. Considering the flat part of the CFR, i.e., frequencies below 120 MHz, the simulation results have an average difference of 0.5 dB with respect to the measurements.

Fig. 3 .

 3 Fig. 3. Results of the 2 × 2 MIMO scenario (a) Path loss and RMS delay spread and (b) Normalized SVs. signal vector, Y = (y 1 , • • • , y N R ) is the received signal vector, and Z= (z 1 , • • • , z N R )T is the noise vector which consists of the ambient shot and thermal noises in the receiver. H is MIMO channel matrix (N R × N T ) which contains the channel coefficients between TX and RX pairs. Let U and V are unitary rotation matrices and assume Λ is a quasi-diagonal "scaling" matrix. We can always decompose the channel matrix H by means of U, Λ, and V as H = UΛV * . It can be noted that both H and Λ matrices have the same shape N T × N R and the rank is given by Γ ≤ min (N T, N R ). The diagonal elements of Λ represent the real-valued and non-negative SVs of the channel matrix H which are given as (λ 1, • • • , λ Γ ). To calculate the throughput at a constant SNR of γ 0 , we first compute the average path gain which is given by

Fig. 4 .

 4 Fig. 4. MIMO Scenarios under consideration.

Fig. 5 .Fig. 6 .

 56 Fig. 5. Normalized SVs for (a) Sc 1, (b) Sc 2, (c) Sc 3, and (d) Sc 4.

This work was supported by the H2020 MSC ITN (VisIoN) 764461. The work of M. Uysal was supported by the Turkish Scientific and Research Council (TUBITAK) Grant 215E311. H B. Eldeeb and M.