Mahdi Gueffaz
email: mahdi.gueffaz@u-bourgogne.fr

Sylvain Rampacek
email: sylvain.rampacek@u-bourgogne.fr

Christophe Nicolle
email: chistophe.nicolle@u-bourgogne.fr

Qualifying Semantic graphs using Model Checking

Keywords: Semantic graph, Model-checking, temporal logic. I

Semantic interoperability problems have found their solutions using languages and techniques from the Semantic Web. The proliferation of ontologies and metainformation has improved the understanding of information and the relevance of search engine responses. However, the construction of semantic graphs is a source of numerous errors of interpretation or modeling and scalability remains a major problem. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border of two areas: the semantic web and the model checking. This line of research concerns the adaptation of model checking techniques to semantic graphs. In this paper, we present a first method of converting RDF graphs into NμSMV and PROMELA languages.

INTRODUCTION

W3C 1 aims to standardize the representation and the exchange of information on the WEB. This objective should help make the information understandable for both automated processes and users. The homogenization of computer exchanges took place due to the introduction of the XML [START_REF] Bray | Extensible Markup Language (XML) 1.1[END_REF] standard. This standard has enabled the program to manipulate information through languages with hierarchical structure mark-up defined by grammars derived from the XML standard. However, this effort has not helped improve the user"s understanding of information. Thus, new standards have been developed to enable the semantic representation of information in the form of XML-derived languages. This base is called Semantic Web standards and it is usually represented as a stack of languages ranging from automatic processes oriented languages to languages representing more abstract concepts of formal semantics [START_REF] Berners-Lee | The Semantic Web[END_REF]. These languages are used to represent the semantics associated with information, whatever its form and structure. To allow the construction of semantic graph, many tools have been developed like Annotea [START_REF] Kahan | Annotea: An Open RDF Infrastructure for Shared Web Annotations[END_REF] which is a project of the W3C that specifies the infrastructure for the annotation of Web documents. The main format used in the annotation is RDF and the types of documents can be annotated are HTML documents or XML based. However, none provides the functionality to verify the consistency of semantics, and reduce errors annotations. This paper proposes a new way to check these semantic graphs by model-checking in order to reduce errors in annotation and make the data more relevant. Model checking 1 World Wide Web Consortium is an automatic verification technique, it has been applied to many cases in industry, for example [START_REF] Katoen | The princiapl of Model Checking[END_REF], in the Netherlands, model-checking has revealed several serious flaws in the design of control system of a barrier protection against flooding which protects the main port of Rotterdam against floods. The large manufacturing company processor "Intel" has used the model-checking to detect the bug in its Pentium II processor that caused a loss of 475 million dollars damage to the reputation of INTEL. Finally, the model-checking was allowed to find an error in the system of handling baggage at the Denver airport (USA), delayed opening its doors for 9 months and a loss of 1.1 million dollars per day.

Model checking is a powerful tool for system verification because it can reveal errors that were not discovered by other formal methods such as testing or simulation. Model checking uses temporal logic to describe the properties checking the system model. As we have seen in the examples above, the model-checking can handle complex problems with large amounts of information, stored as a graph, in order to verify critical systems. In comparison, in the semantic web, the use of graphs is pervasive and serious problems of scalability arise [START_REF] Homma | Modeling and Verification of Web Applications Using Formal Approach[END_REF]. Thus, it is appropriate to use the algorithms developed for model-checking to the field of Semantic Web.

Related Work

In this section, we briefly discuss some of the researches related to the verification of the Semantic graphs using the model checking. There are very few researches about the use of the model checking method to qualify a Semantic graph. On the contrary, there are several researches that verify the Web application. The work in [START_REF] Mateescu | Extending SPARQL with Temporal logic[END_REF] proposes a new way of converting an RDF graph to the BCG2 format that was used in the CADP3 toolbox.

The CADP toolbox is a verification toolbox for asynchronous concurrent systems. The toolbox accepts as input several languages and all of these languages are compiled into LTS 4 , which are state/transition graphs representing the behavior of concurrent systems. CADP provides several representations for LTS; one of these representations is the BCG format.

There are several researches in which the Web application is modeled as a directed graph. In [START_REF] Sciascio | Web Applications Design and Maintenance using Symbolic Model Checking[END_REF], [START_REF] Sciascio | AnWeb: a System for Automatic Support to Web Application Verification[END_REF], the components of a window (e.g., a page, a frame and a link) are modeled as states. The reachability between states is defined as requirements of the Web application and they are verified using the model checking. In [START_REF] Ricca | Analysis and Testing of Web Applications[END_REF], [START_REF] Ricca | Web Site Analysis: Structure and Evolution[END_REF], [START_REF] Han | Modeling and Verification of Adaptive Navigation in Web Applications[END_REF], they took an approach to model the Web applications using parallel composition of the UML diagrams. The work in [START_REF] Haydar | Properties and Scopes in Web Model Checking[END_REF] proposes the way to discriminate states of interest by introducing a specialized operator for LTL. They use it to verify the Web applications.

In [START_REF] Yuen | Web Automa A Behavioral Model of Web applications based on the MVC model[END_REF], the authors propose a behavioral model of the Web application, called "Web Automata" based on the MVC 5 model architecture. They model the behavior of a Web application with dynamic contents as an extension of linksautomata with the constraint-logic feature of the Extended Finite Automata (EFA). The testing framework of Web applications based on the behavioral model is also presented in their research. In [START_REF] Haydar | Formal Verification of Web Applications Modeled by Communicating Automata[END_REF], the authors present a formal approach for modeling Web applications using communicating automata. They observe the external behavior of an explored part of a Web application using a monitoring tool. The observed behavior is then converted into communicating automata representing all windows, frames and framesets of the application under test by intercepting HTTP 6 requests and responses using a proxy server.

II. MODEL CHECKING AND TEMPORAL LOGIC OVERVIEW

Formal methods [START_REF] Katoen | The principal of Model Checking[END_REF] offer great potential for an early inclusion of verification in the design process, providing technical audit more efficiently and reduce the verification time. Formal methods are highly recommended techniques for the development of software. They have led to the development of some very promising verification techniques that facilitate early detection of defects. Two types of formal verification methods can be distinguished: methods based on the proof of the theorem and the methods based on models.

Methods based on the proof of the theorem verify the correctness of systems by properties in a mathematical theory. These properties are proven with the highest possible precision using tools such as theorem provers and proof checkers. Theorems proof are also called proof assistants.

Methods based on models describe the possible system behavior in a mathematical precise and unambiguous manner. The system models are accompanied by algorithms that systematically explore all states of the system model. This provides the basis for a whole range of verification techniques ranging from an exhaustive exploration "Model checking" to experiments with a restrictive set of scenario in the model "Simulation". Simulation allows the user to study the system behavior. It is less suited to detect errors because it is difficult to generate all possible scenarios of the system and to simulate them all. Model checker is a verification technique that explores all possible system state. In this way, it can be shown that a given system model truly satisfies a certain property.

The model checker examines all relevant system states in order to check whether they satisfy the desired property. The model checker gives a counter example that indicates how the model can violate the property. With a help of a simulator, the user can locate the error and adapt the model or the property to prevent the violation of property (Fig. 1). 5 Model, View, and Control 6 Hypertext Transfer Protocol For our approach we will use model checking to analyze semantic networks. We use both linear time logic "LTL" and computation tree logic "CTL" for describing the specifications of the properties to be verified with model checking. The concepts of temporal logic used for the first time by Pnueli [START_REF] Pnueli | The temporal logic of programs[END_REF] in the specification of formal properties are fairly easy to use. The operators are very close in terms of natural language. The formalization in temporal logic is simple enough although this apparent simplicity therefore requires significant expertise. Temporal logic allows representing and reasoning about certain properties of the system, so it is well-suited for the systems verification. There are two main temporal logics, that is linear time and branching time. In linear time temporal logic, each execution of the system is independently analyzed. In this case, a system satisfies a formula f, if f holds along every execution. The branching time combines all possible executions of the system into a single tree. Each path in the tree is a possible representation of the system execution.

Algorithm

III. THE SCALESEM APPROACH

This section details our approach which consists in transforming semantic graphs into models in order to be verified by the model-checker. For this, we have developed two tools called "RDF2SPIN" and "RDF2NμSMV", that

Satisfied

System

Formalizing Modeling

Requirement

Location error

Property specification

Model-Checking

Violated + Counterexample Simulation

System model transform semantic graphs into PROMELA 7 and respectively into NµSMV [START_REF] Cimatti | NµSMV: a new symbolic model checker[END_REF] language.

We use SPIN [START_REF] Ben-Ari | Principles of the SPIN Model Checker[END_REF] and NµSMV as model checkers to check the model of semantic graphs. We want to compare them in term of capabilities. SPIN is a software tool for verifying system models. The system is described in a language model called PROMELA. NµSMV is the amelioration of SMV model checker, working on the same simple principles as SMV. SPIN verifies the correctness of properties expressed in linear time logic; on the other side NµSMV verifies the properties in both linear time logic and computation tree logic. In Fig. 2, we present the architecture of our approach. In this architecture, from a natural language description, we can get the semantic graph (RDF 8 ) and its description in temporal logic, as shown in the example found in the section VII. We divide this architecture in two phases. The first phase concerns the transformation of the semantic graph into a model using our tools RDF2SPIN and RDF2NμSMV. There are three steps in this transformation. The first step is to explore the entire RDF graph to obtain the triplets table. The second step is to determine a root for the graph, and the last step is to write the model that represents the semantic graph in the PROMELA or NµSMV languages. The second phase concerns the verification of properties expressed in temporal logic on the model using the model-checker SPIN or NµSMV. The choice of model checker depends on the tool that you use to convert the semantic graphs. For example, when using RDF2SPIN, you must use the modelchecker SPIN to check your model.

A. Introducing RDF

RDF is a language developed by the W3C to bring a semantic layer to the Web [START_REF] Becket | RDF/ XML Syntax Specification (Revised)[END_REF]. It allows the connection of Web resources using directed labeled edges. The structure of RDF documents is a complex labeled directed graph. An RDF document is a set of triples <subject, predicate, object>. In addition, the predicate (also called property) connects the subject (resource) to the object (value). Thus, the subject and the object are nodes of the graph connected by an edge directed from the subject towards the object. The 7 Process Meta Language 8 Resource Description Framework nodes and the edges belong to "resource" types. A resource is identified by a Uniform Resource Identifier [START_REF] Berners-Lee | W3C recommandation[END_REF].

The declarations can also be represented as a graph, the nodes as resources and values, and arcs as properties. The resources are represented in the graph by circles; the properties are represented by directed arcs and values by a box (a rectangle). Values can be resources if they are described by additional properties. For example, when a value is a resource in another triplet, the value is represented by a circle [START_REF] Bönström | Storing RDF as a graph[END_REF].

The RDF graphs considered here are represented as XML verbose files, in which the information is not stored hierarchically (so-called graph point of view). These RDF graphs, that is, in fact, the semantic model of an RDF file, are not necessarily connected, meaning they may have no root vertex from which all the other vertices are reachable. The RDF graph transformation into a model is articulated in three steps: exploring the RDF graph, holding election of the root vertex, generating the model of the semantic graph.

B. Exploring RDF graph

In order to exploit the RDF graphs by using SPIN or NµSMV, we therefore have to determine whether they have a root vertex, by analyzing RDF triples, and if this is not the case, we must create a new root vertex by taking care to keep the size of the resulting graph as small as possible.

We achieve this by appropriate explorations of the RDF graphs, as explained below. Let us consider that an RDF graph is represented as a couple (V, E), where V is the set of vertices and V E  x V is the set of edges. For a vertex x, we note

 ) (x E { V y  | E y x  ) , (
} the set of its successor vertices. This corresponds to the classical data structure for representing graphs in memory, consisting of an array indexed by the vertices and containing in each entry the list of successor vertices of the corresponding vertex. There are several algorithms to traverse a large graph, of these basic algorithms include the best known, depth-first search (DFS) and breadth-first search (BFS). We use depthfirst search algorithm, illustrated below to explore graph, knowing that the breadth-first algorithm also works in this context. We considered here an iterative variant of DFS which makes use of an explicit stack, rather than the recursive variant given in [START_REF] Tarjan | Depth-First search and linear graph algorithm[END_REF]; this is required in practice to avoid overflows of the system call stack when the algorithm is invoked for exploring large graphs.

C. Determining a Root Vertex

If the RDF graph has no vertex root, we must create a root as to be the successors of all vertices of the graph but it will increase the number of edges. We look forward to doing this by adding a few edges as possible. A vertex x of a directed graph is a partial root if it cannot be reached from any other vertex of the graph. If the graph contains only one partial root, all other vertices of the graph can be reached from the root, otherwise there would be other roots in the partial graph. If the graph has multiple partial roots, the most economical way to provide a root is to create a new record with all the roots as a partial successor: this will add to the graph a minimum number of edges. We compute the set of partial roots in two phases, each one consisting in successive explorations of the graph. The first phase identifies a set of candidate partial roots, and the second one refines this set in order to determine the partial roots of the graph.

Remark: a property must always have a resource and a value; the resource should never be a value with the same predicate, i.e. a loop in the graph. The first phase explores the graph until it is fully explored, and inserts in root_list all vertices that have no predecessor. If root_list contains a single vertex, so overall it is the global root of the graph since all the other vertex are accessible from it and it is useless to the second phase has passed. Otherwise, any vertex contained in root_list could also be a root of the graph: the role of the second phase is to determine which of the partial root the root of the global graph is.

The second phase performs a new wave of exploration of the roots contained in partial root_list in reverse order in which they were inserted in the list. If a root in root_list is to be visited by a partial root, it is removed from the list because it is not a partial root. At the end of this phase, all partial roots of the graph are present in root_list. Indeed, each vertex is unreachable from the partial roots which were explored during the second phase. A new root is created (see Fig. 3), having as successor all the partial roots of root_list, which ensures that all vertices of the graph are accessible from the new root. Therefore, such a summit is inaccessible from other nodes of the graph. A root is a single node that has no predecessor. In this graph, we have node A and node B, two roots, and then we will create a new virtual root (blue circle "R") that points to the two roots.

The algorithm for determining a root has a complexity O(|V|+|E|), linear in the size of the graph (number of vertices and edges), since each phase visits every state and traverses every edge of the graph only once. Given that the graph must be traversed entirely in order to determine whether it has a root or not, this complexity is optimal.

D. Generating the model

The third step is divided into three sub-steps. The first one consists in creating the table of all triples by exploring the entire graph; the second one consists in generating the table of resources and values for RDF2SPIN but for RDF2NµSMV, it generates the table of association. The last one consists in producing the model representing the semantic graph written in PROMELA or in NµSMV language. The model -In this last sub-step, we will write the model in PROMELA language for RDF2SPIN tool or in NµSMV language for RDF2NµSMV tool, corresponding to the RDF graph that we want to check.

IV. EXAMPLE AND BENCHMARK

To illustrate our approach, we take the natural language description in [START_REF] Vatant | Metadata to describe resources (Semantic Web Languages)[END_REF] as follows:

Ninety-three is a novel by Victor Hugo published in 1874, whose theme is the French Revolution. Victor Hugo was born in February 26, 1802 in Besançon.

From the description above, we can easily extract simple propositions, see Table 1 described below, and also the proposal described in temporal logic a little lower. Table 2 presents the RDF triples derived from the Table 1. "Ninety-three is a novel" 2 "Ninety-three its author is Victor Hugo" 3 "Ninety-three has been published in 1874" 4 "Ninety-three"s theme is the French revolution" 5 "Victor Hugo was born in February 26, 1802" 6 "Victor Hugo was born in Besançon"

Figure 1 .

 1 Figure 1. The model checking approach.

Figure 2 .

 2 Figure 2. The ScaleSem architecture.

  Algorithm: procedure Dfs (x): begin visited(x) := true; // vertex x becomes visited p(x) := 0; // start exploring its successors stack := push(x, nil); while stack ≠ nil do y := top(stack); if p(y) < |E (y)| then // y has some unexplored successors z := E (y) ) ( y p ; p(y) := p(y)+1; // take the next successor of y if  visited (z) then visited(z) := true; // visit it p(z) := 0;//start exploring its successors

  Algorithm: procedure RootElection(): // precondition:  x  V.visited(x) = false Begin // first phase root_list := nil; forall x  V do if  visited(x) then Dfs(head(root_list) // the single partial root is the global root else forall x  V do visited(x):= false; endfor; forall x  root_list do // reexplore partial roots in reverse order if  visited(x) then Dfs(x) else root_list := root_list \ {x} // partial root is not a real one endif endfor; if |root_list| = 1 then root := head(root_list) // a single partial root is the global root else root := new_node(); // new root predecessor of the partial roots E(root) := root_list endif endif

Figure 3 .

 3 Figure3. A root is a single node that has no predecessor. In this graph, we have node A and node B, two roots, and then we will create a new virtual root (blue circle "R") that points to the two roots.

Table of triples

 of -We will create a table consisting in resources, properties and values, by exploring the RDF graph. In our RDF graph, the resource and the value are represented by nodes and the property is an edge directed from the resource towards the value. The table of triples of the RDF graph is useful for the next sub-step. In this second sub-step, RDF2SPIN generates a table of resources and values, while RDF2NµSMV generates a table of association. • Table of resources and values -Browsing the table triples seen in the previous step, we attribute a unique function for each resource and for each value. These functions are of proctype type. We combine all these functions in a table called table of resources and values. • Table of association -This table contains an identifier for each resource, property and value.

TABLE 1 .

 1 SHORT LIST OF SIMPLE PROPOSITION

Binary Coded Graph

Construction and Analysis of Distributed Processes

Labeled Transition System

Victor Hugo Place_born Besançon

From the previous description in natural language, we can express it in temporal logic as shown in Table 3. These temporal logics are expressed in a general way, but they can be expressed as well in both linear time logic and computation tree logic. We check that Victor Hugo was born in Besançon Now, we will be able to transform the RDF graph in Fig. 4 with our tools "RDF2SPIN" and RDF2NμSMV" into a model in order to check each formula of temporal logic described in Table 3 and see if each formula is verified or not in the model with the SPIN and NµSMV modelcheckers. In this way we can verify the semantic graphs. We tested our tools on several RDF graphs, and we calculated the time of conversion as shown in Fig 5 . Note that RDF2SPIN tool is faster in converting semantic graphs than the RDF2NµSMV tool. Both tools are quick in converting semantic graphs; we have less than 15 seconds for a graph of 53 MB size with RDF2SPIN tool and almost 21 seconds with RDF2NµSMV tool. Both transformation tools follow a polynomial curve. In Fig. 6, we see the size of converted semantic graphs from RDF to PROMELA language with RDF2SPIN and NµSMV language with RDF2NµSMV. We remark that the sizes of PROMELA model are smaller than the NµSMV model. This paper presents a new technique for the semantic graphs verification by using a model-checker. Knowing that the model-checker does not understand the semantic graphs, we developed two tools RDF2SPIN and RDF2NµSMV to convert them into PROMELA and NµSMV languages in order to be verified with the temporal logics. There are formulas that can be presented in LTL and not in CTL and vice versa. The advantage of NµSMV is that the verification can be made with both linear time logic and computation tree logic formulas.

In future work, we would like to convert the SPARQL query language for RDF graphs into queries using the operator of the temporal logic, to have a better verification of RDF graphs representing the building industry.

REFERENCE


Piotr Graczyk
email: piotr.graczyk@univ-angers.fr

Jacek Malecki
email: jacek.malecki@pwr.wroc.pl

Yamada-Watanabe Theorem

Jacek Małecki

MULTIDIMENSIONAL

Keywords: 2010 Mathematics Subject Classification. 60J60, 60H15 stochastic differential equations, strong solutions, Yamada-Watanabe theorem, Wishart process

come

Introduction

In this note we prove a multidimensional and matrix analogues of the celebrated Yamada-Watanabe theorem, ensuring the existence and uniqueness of strong solutions of one-dimensional stochastic differential equations (SDEs) with a Hölder coefficient in the Itô integral part. In Section 2 we prove a multidimensional Yamada-Watanabe theorem (Theorem 2). In Section 3 we show the existence and uniqueness of a strong solution of the matrix SDEs dX t = g(X t )dB t h(X t ) + h(X t )dB T t g(X t ) + b(X t )dt where g, h, b : R → R are such that g ⊗ h is 1/2-Hölder continuous symmetrized g 2 ⊗ h 2 and b are Lipschitz continuous and B t is a Brownian p × p matrix, and establish in this way a matrix Yamada-Watanabe theorem, see Theorem 5. Section 4 contains interesting applications. We apply Theorems 2 and 5 to (i) noncolliding particle systems of squared Bessel processes which are intensely studied in recent years in statistical and mathematical physics (Katori, Tanemura [START_REF] Katori | Symmetry of matrix-valued stochastic processes and noncolliding diffusion particle systems[END_REF][START_REF] Katori | Noncolliding Squared Bessel processes[END_REF]).

(ii) the systems of SDEs for the eigenvalues of Wishart and Jacobi matrix processes, as well as to the β-Wishart and β-Jacobi processes. We note the importance of the β-Wishart systems in statistical physics: they are statistical mechanics models of "loggases", see the recent book of Forrester [START_REF] Forrester | Log-gases and random matrices[END_REF].

Surprisingly, the existence of strong solutions of SDEs for such "Hölder" non-colliding particle systems was not established in general; only some cases of (ii) were treated by Demni [START_REF] Demni | Note on radial Dunkl processes[END_REF][START_REF] Demni | β-Jacobi processes[END_REF]. In Sections 4.1 and 4.4 we prove the existence and uniqueness of a strong solution to all these systems of SDEs.

The matrix Yamada-Watanabe theorem is applied in Sections 4.2 and 4.3 to some matrix valued squared Bessel type processes. We improve the known results of Bru [START_REF] Bru | Processus de Wishart[END_REF][START_REF] Bru | Wishart processes[END_REF], Mayerhofer et al. [START_REF] Mayerhofer | On strong solutions for positive definite jump-diffusions[END_REF] and Doumerc [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF] on the existence and uniqueness of strong solutions to Wishart and Jacobi matrix SDEs. We extend them to the whole range of the drift parameter b(X t ). In the Wishart case we contribute in this way to realization of a programme started by Donati-Martin, Doumerc, Matsumoto, Yor [START_REF] Donati-Martin | Some properties of the Wishart processes and a matrix extension of the Hartman-Watson laws[END_REF], claiming that Wishart processes have similar properties as classical 1-dimensional squared Bessel processes.

A multidimensional Yamada-Watanabe theorem

Let us recall the classical Yamada-Watanabe theorem, see e.g. [START_REF] Ikeda | Stochastic differential equations and diffusion processes[END_REF], p.168 and [START_REF] Yamada | On the uniqueness of solutions of stochastic differential equations[END_REF].

Theorem 1. Let B(t) be a Brownian motion on R. Consider the SDE

dX(t) = σ(X(t))dB(t) + b(X(t))dt.
If |σ(x) -σ(y)| 2 ≤ ρ(|x -y|) for a strictly increasing function ρ on R + with ρ(0) = 0 and 0 + ρ -1 (x)dx = ∞, and b is Lipschitz continuous, then the pathwise uniqueness of solutions holds; consequently the equation has a unique strong solution.

No multidimensional versions of the Yamada-Watanabe theorem seem to be known, even if their need is great (cf. [START_REF] Bru | Wishart processes[END_REF], p. 738). We propose a useful generalization, however we stress the fact that the Hölder continuous functions σ i appearing in the following system of SDEs are one-dimensional. The proof is based on the approach presented in Revuz,Yor [START_REF] Revuz | Continuous Martingales and Brownian Motion[END_REF], in particular on the results of Le Gall [START_REF] Gall | Applications du temps local aux équations différentielles stochastiques unidimensionnelles[END_REF]. By • we mean the Euclidean norm

• 2 on R d .
Theorem 2. Let p, q, r ∈ N and the functions b i : R p → R, i = 1, . . . , p and c k , d j : R p+r → R, k = p + 1, . . . , p + q, j = p + 1, . . . , p + r, be bounded real-valued and continuous, satisfying the following Lipschitz conditions

|b i (y 1 ) -b i (y 2 )| ≤ A||y 1 -y 2 ||, i = 1, . . . , p, |c k (y 1 , z 1 ) -c k (y 2 , z 2 )| ≤ A||(y 1 , z 1 ) -(y 2 , z 2 )||, k = p + 1, . . . , p + q, |d j (y 1 , z 1 ) -d j (y 2 , z 2 )| ≤ A||(y 1 , z 1 ) -(y 2 , z 2 )||, j = p + 1, . . . , p + r,
for every y 1 , y 2 ∈ R p and z 1 , z 2 ∈ R r . Moreover, let σ i : R → R, i = 1, . . . , p, be a set of bounded Borel functions such that

|σ i (x) -σ i (y)| 2 ≤ ρ i (|x -y|), x, y ∈ R,
where ρ i : (0, ∞) → (0, ∞) are Borel functions such that 0 + ρ -1 i (x)dx = ∞. Then the pathwise uniqueness holds for the following system of stochastic differential equations

dY i = σ i (Y i )dB i + b i (Y )dt, i = 1, . . . , p, (2.1
)

dZ j = p+q k=p+1 c k (Y, Z)dB k + d j (Y, Z)dt, j = p + 1, . . . , p + r. (2.2)
Proof. Let (Y, Z) and ( Ỹ , Z) be two solutions with respect to the same Brownian motion B = (B i ) i≤p+q such that Y (0) = Ỹ (0) and Z(0) = Z(0) a.s. For every i = 1, . . . , p we have

Y i (t) -Ỹi (t) = t 0 (σ i (Y i (s)) -σ i ( Ỹi (s)))dB i (s) + t 0 (b i (Y (s)) -b i ( Ỹ (s)))ds. (2.3)
Then we get

t 0 1 {Y i (s)> Ỹi (s)} ρ i (Y i (s) -Ỹi (s)) d Y i -Ỹi , Y i -Ỹi = t 0 (σ i (Y i (s)) -σ i ( Ỹi (s))) 2 ρ i (Y i (s) -Ỹi (s)) 1 {Y i (s)> Ỹi (s)} ds ≤ t.
Thus, applying Lemma 3.3 from [START_REF] Revuz | Continuous Martingales and Brownian Motion[END_REF] p. 389 , we get that the local time of Y i -Ỹi at 0 vanishes identically. Consequently, by Tanaka's formula we get

|Y i (t) -Ỹi (t)| = t 0 sgn(Y i (s) -Ỹi (s))d(Y i (s) -Ỹi (s)) + 1 2 L 0 t (Y i -Ỹi ) = t 0 sgn(Y i (s) -Ỹi (s))d(Y i (s) -Ỹi (s)).
Since σ i is bounded, using (2.3), we state that

|Y i (t) -Ỹi (t)| - t 0 sgn(Y i (s) -Ỹi (s))(b i (Y (s)) -b i ( Ỹ (s)))ds
is a martingale vanishing at 0. This together with the Lipschitz conditions satisfied by b i give

E|Y i (t) -Ỹi (t)| ≤ A t 0 E||Y (s) -Ỹ (s)||ds.
Summing up the above-given inequalities we arrive at

E||Y (t) -Ỹ (t)|| ≤ C t 0 E||Y (s) -Ỹ (s)||ds
and Gronwall's lemma shows that Y (t) = Ỹ (t) for every t > 0 a.s. Using in a standard way the properties of the Itô integral and the Schwarz inequality, similarly as in [START_REF] Ikeda | Stochastic differential equations and diffusion processes[END_REF], p. 165, we get that for every t ∈ [0, T ]

E|Z j (t) -Zj (t)| 2 ≤ C p+q k=p+1 E( t 0 c k (Y (s), Z(s)) -c k ( Ỹ (s), Z(s))dB k (s)) 2 + CE( t 0 d j (Y (s), Z(s)) -d j ( Ỹ (s), Z(s))ds) 2 ≤ C p+q k=p+1 E t 0 (c k (Y (s), Z(s)) -c k ( Ỹ (s), Z(s))) 2 ds + CT E t 0 (d j (Y (s), Z(s)) -d j ( Ỹ (s), Z(s))) 2 ds ≤ CA 2 (q + T )E t 0 (||Y (s) -Ỹ (s)|| 2 + ||Z(s) -Z(s)|| 2 )ds
Thus, using the previously proved fact that Y = Ỹ a.s. we get that

E||Z(t) -Z(t)|| 2 ≤ CA 2 (q + T )r t 0 E||Z(s) -Z(s)|| 2 ds.
One more application of the Gronwall's lemma ends the proof.

Matrix stochastic differential equations

Consider the space S p of symmetric p × p real matrices. Recall that if g : R → R and X ∈ S p then g(X) = Hg(Λ)H T , where X = HΛH T is a diagonalization of X, with H an orthonormal matrix and Λ a diagonal one. Denote by B t a Brownian p×p matrix. Let X t be a stochastic process with values in S p such that X 0 ∈ Sp , the set of symmetric matrices with p different eigenvalues. Let Λ t = diag(λ i (t)) be the diagonal matrix of eigenvalues of X t ordered increasingly: λ 1 (t) ≤ λ 2 (t) ≤ . . . ≤ λ p (t) and H t an orthonormal matrix of eigenvactors of X t . Matrices Λ and H may be chosen as smooth functions of X until the first collision time τ = inf{t : λ i (t) = λ j (t) for some i = j}, cf. [START_REF] Norris | Brownian motions of ellipsoids[END_REF].

3.1. Eigenvalues and eigenvectors of X t . In order to prove a matrix Yamada-Watanabe theorem we need to consider the SDEs satisfied by the processes of eigenvalues and eigenvectors of X t . Theorem 3. Suppose that an S p -valued stochastic process X t satisfies the following matrix stochastic differential equation

dX t = g(X t )dB t h(X t ) + h(X t )dB T t g(X t ) + b(X t )dt (3.1)
where g, h, b : R → R, and

X 0 ∈ Sp . Let G(x, y) = g 2 (x)h 2 (y) + g 2 (y)h 2 (x).
Then, for t < τ the eigenvalues process Λ t and the eigenvectors process H t verify the following stochastic differential equations

dλ i = 2g(λ i )h(λ i )dν i + b(λ i ) + k =i G(λ i , λ k ) λ i -λ k dt (3.2)
dh ij = k =j h ik G(λ j , λ k ) λ j -λ k dβ kj - 1 2 h ij k =j G(λ j , λ k ) (λ k -λ j ) 2 dt (3.3)
where (ν i ) i and (β kj ) k<j are independent Brownian motions and β jk = β kj .

Proof. The proof generalizes ideas of Bru [START_REF] Bru | Diffusions of perturbed principal component analysis[END_REF] in the case of Wishart processes. Following [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF] in the case of matrix Jacobi processes, it is handy to use the Stratonovich differential notation X • dY = XdY + 1 2 dXdY . We then write the Itô product formula

d(XY ) = dX • Y + X • dY.
We also have dX

• (Y Z) = (dX • Y ) • Z and (X • dY ) T = dY T • X T . Define A, a stochastic logarithm of H, by dA = H -1 • dH = H T • dH.
Observe that by Itô formula applied to H T H = I, the matrix A is skew-symmetric. By Itô formula applied to Λ = H T XH, setting dN = H T • dX • H, we get

dΛ = dN + Λ • dA -dA • Λ.
The process Λ • dA -dA • Λ is zero on the diagonal. Consequently dλ i = dN ii and 0 = dN ij + (λ i -λ j ) • dA ij , when i = j. Thus

dA ij = 1 λ j -λ i • dN ij , i = j. (3.4)
For further computations we need the quadratic variation X st , X s ′ t ′ which is easily computed from (3.1):

dX st dX s ′ t ′ = g 2 (X) ss ′ h 2 (X) tt ′ + g 2 (X) st ′ h 2 (X) s ′ t + g 2 (X) s ′ t h 2 (X) st ′ + g 2 (X) tt ′ h 2 (X) ss ′ .
The martingale part of dN equals the martingale part of H T dX H and by the last formula

dN ij dN km = g 2 (Λ) ik h 2 (Λ) jm + g 2 (Λ) im h 2 (Λ) jk + g 2 (Λ) jk h 2 (Λ) im + g 2 (Λ) jm h 2 (Λ) ik . (3.5)
From (3.5) it follows that

dN ii dN jj = 4δ ij g 2 (λ i )h 2 (λ i )dt. (3.6)
Now we compute the finite variation part dF of dN

dF = H T b(X)H + 1 2 (dH T dX H + H T dXdH) = b(Λ) + 1 2 (dH T H)(H T dX H) + (H T dX H)(H T dH) = b(Λ) + 1 2 (dNdA + (dNdA) T ).
Using (3.4) and (3.5) we find, writing

G(x, y) = g 2 (x)h 2 (y) + g 2 (y)h 2 (x), (dNdA) ij = k =j dN ik dA kj = δ ij k =i G(λ i , λ k ) λ i -λ k .
It follows that the matrix dNdA is diagonal, so also dF is diagonal,

dF ii = b(λ i )dt + k =i G(λ i , λ k ) λ i -λ k dt
and by (3.4), A is a martingale. Finally, using (3.6) and the last formula, there exist independent Brownian motions ν i , i = 1, . . . , m, such that (3.2) holds.

In order to find SDEs for H t , we deduce from the definition of dA that

dH = H • dA = HdA + 1 2 dHdA = HdA + 1 2
HdAdA.

By (3.5) we find dN ij dN ij = g 2 (λ i )h 2 (λ j ) + g 2 (λ j )h 2 (λ i )
and dN ij dN km = 0 when the ordered pairs i < j and k < m are different. We infer from (3.4) that

dA ij = G(λ i , λ j ) λ j -λ i dβ ij , (3.7)
where the Brownian motions (β ij ) i<j are independent and β ji = β ij . Moreover, when k < m, we have dλ i da km = dN ii dN km /(λ m -λ k ) = 0 by (3.5), so the Brownian motions (β ij ) i<j and (ν i ) i are independent. From (3.7) we deduce that the matrix dAdA is diagonal and

(dAdA) ii = - k =i dA ik dA ik = - k =i G(λ i , λ k ) (λ k -λ i ) 2 .
Now we can compute dH = HdA + 1 2 HdAdA and prove (3.3). 3.2. Complex case. In this subsection we study the eigenvalues process for a process X t with values in the space H p of Hermitian p × p matrices. Theorem 4. Let W t be a complex p × p Brownian matrix (i.e. W t = B 1 t + iB 2 t where B 1 t and B 2 t are two independent real Brownian squared matrices). Suppose that an H p -valued stochastic process X t satisfies the following matrix stochastic differential equation

dX t = g(X t )dW t h(X t ) + h(X t )dW * t g(X t ) + b(X t )dt, (3.8)
where g, h, b : R → R, and

X 0 ∈ Hp . Let G(x, y) = g 2 (x)h 2 (y) + g 2 (y)h 2 (x).
Then, for t < τ the eigenvalues process Λ t verifies the following system of stochastic differential equations

dλ i = 2g(λ i )h(λ i )dν i + b(λ i ) + 2 k =i G(λ i , λ k ) λ i -λ k dt, (3.9)
where (ν i ) i are independent Brownian motions.

Proof. We will need the following formula for the quadratic variation X st , X s ′ t ′ which is computed from (3.8), using the fact that for a complex Brownian motion W t , the quadratic variation processes satisfy d W, W = 0 and d W, W = 2dt.

dX st dX s ′ t ′ = 2 g 2 (X) st ′ h 2 (X) s ′ t + g 2 (X) s ′ t h 2 (X) st ′ . (3.10)
Define A, a stochastic logarithm of H, by

dA = H -1 • dH = H * • dH.
By Itô formula applied to H * H = I, the matrix A is skew-Hermitian. In particular, the terms of diag(A) are purely imaginary (recall that in the real case they were 0). By Itô formula applied to Λ = H * XH, we get, setting

dN = H * • dX • H dΛ = dN + Λ • dA -dA • Λ.
We have

dN = H * dXH + 1 2 (dH * dX H + H * dXdH)
so the process N takes values in H p . In particular its diagonal entries are real. The process Λ • dA -dA • Λ is zero on the diagonal, so dλ i = dN ii . Moreover, when i = j, we have 0 = dN ij + (λ i -λ j ) • dA ij and

dA ij = 1 λ j -λ i • dN ij , i = j. (3.11)
The martingale part of dN equals the martingale part of H * dX H and by formula (3.10) we obtain

dN ij dN km = 2 g 2 (Λ) im h 2 (Λ) jk + g 2 (Λ) jk h 2 (Λ) im . (3.12)
From (3.12) it follows that

dN ii dN jj = 4δ ij g 2 (λ i )h 2 (λ i )dt. (3.13)
Now we compute the finite variation part dF of dN

dF = H * b(X)H + 1 2 (dH * dX H + H * dXdH) = b(Λ) + 1 2 ((dH * H)(H * dX H) + (H * dX H)(H * dH)) = b(Λ) + 1 2 (dNdA + (dNdA) * ).
Recall that G(x, y) = g 2 (x)h 2 (y) + g 2 (y)h 2 (x). We get

(dNdA) ij = k dN ik dA kj = 2δ ij k =i G(λ i , λ k ) λ i -λ k + dN ij dA jj .
When i = j, the term dN ii is real and dA ii ∈ iR. It follows that

dF ii = b(λ i )dt + 2 k =i G(λ i , λ k ) λ i -λ k dt.
Finally, using (3.13) and the last formula, there exist independent Brownian motions ν i , i = 1, . . . , m, such that (3.9) holds.

The Theorem 4 may be applied in a special case g(x) = √ x, h(x) = 1 and b(x) = 2δ > 0, when the equation (3.8) is the SDE for the complex Wishart process, called also a Laguerre process. This process and its eigenvalues were studied by König-O'Connell [START_REF] König | Eigenvalues of the Laguerre process as non-colliding squared Bessel processes[END_REF] and Demni [START_REF] Demni | The Laguerre process and generalized Hartman-Watson law[END_REF].

Collision time.

In this subsection we show that under some mild conditions on the functions g and h in the SDE (3.1), the eigenvalues of the process X t never collide.

Proposition 1. Let Λ = (λ i ) i=1...p be a process starting from λ 1 (0) < . . . < λ p (0) and satisfying (3.2) with functions b, g, h : R → R such that b, g 2 , h 2 are Lipschitz continuous and g 2 h 2 is convex or in class C 1,1 . Then the first collision time τ is infinite a.s.

Proof. We define U = -i<j log(λ j -λ i ) on t ∈ [0, τ ]. Applying Itô formula, using (3.2) and the fact that

d λ i , λ j = δ ij 4g 2 (λ i )h 2 (λ j )dt we obtain dU = i<j dλ i -dλ j λ j -λ i + 1 2 d λ i , λ i + d λ j , λ j (λ j -λ i ) 2
= dM + dA (1) + dA (2) + dA (3) ,

where dM = 2 i<j g(λ i )h(λ i )dν i -g(λ j )h(λ j )dν j λ j -λ i , dA (1) = i<j b(λ i ) -b(λ j ) λ j -λ i dt, dA (2) = 2 i<j (g 2 (λ j ) -g 2 (λ i ))(h 2 (λ j ) -h 2 (λ i )) (λ j -λ i ) 2 dt, dA (3) = i<j 1 λ j -λ i k =i,k =j G(λ i , λ k ) λ i -λ k - G(λ j , λ k ) λ j -λ k dt = i<j<k G(λ j , λ k )(λ k -λ j ) -G(λ i , λ k )(λ k -λ i ) + G(λ i , λ j )(λ j -λ i ) (λ j -λ i )(λ k -λ i )(λ k -λ j ) dt.
We will show that the finite variation part of U is bounded on any interval [0, t]. Lipschitz continuity of b, g 2 and h 2 implies that A

t ≤ Kp(p -1)t/2 and A

t ≤ K 2 p(p -1)t, where K is a constant appearing in the Lipschitz condition. Observe also that if for every x, y, z we set

H(x, y, z) = [(g 2 (x) -g 2 (z))(h 2 (y) -h 2 (z)) + (g 2 (y) -g 2 (z))(h 2 (x) -h 2 (z))](y -x),
then H(x, y, z) = (G(x, y) -G(x, z) -G(y, z) + G(z, z))(y -x) and H(x, y, z) + H(y, z, x) -H(x, z, y) = 2(z -y)G(y, z) -2(z -x)G(x, z)

+ 2(y -x)G(x, y) + G(x, x)(z -y) -G(y, y)(z -x) + G(z, z)(y -x).
Using the last equality and the fact that |H(x, y, z)| ≤ 2K 2 |(y -x)(z -y)(z -x)| we can write 2dA (3) = dA (4) + dA (5) , where 0 ≤ A (4)

t ≤ K 2 p(p -1)(p -2)t/6 and dA (5) t = i<j<k G(λ j , λ j )(λ k -λ i ) -G(λ i , λ i )(λ k -λ j ) -G(λ k , λ k )(λ j -λ i ) (λ j -λ i )(λ k -λ i )(λ k -λ j ) dt = i<j<k G(λ j , λ j ) -G(λ i , λ i ) λ j -λ i - G(λ k , λ k ) -G(λ j , λ j ) λ k -λ j 1 λ k -λ i dt If G(x, x) = 2g 2 (x)h 2 (x)
is convex then obviously the expression under the last sum and

A (5) is non-positive. When G(x, x) is C 1,1 , (i.e. |G ′ (x, x) -G ′ (y, y)| ≤ C|x -y|) then it is bounded by C and |A (5)
t | ≤ Ct. Since finite-variation part of U is finite whenever t is bounded, applying McKean argument, we obtain that U can not explode in finite time with positive probability and consequently τ = ∞ a.s.

Remark 1. Note that if p = 2 then the assumptions on g 2 h 2 can be dropped since in that case dA (3) ≡ 0. Observe also that the Proposition 1 holds also in the complex case. The eigenvalues of the process X t on H p verify the system (3.9) and the proof of the Proposition 1 remains valid.

t = g(X t )dB t h(X t ) + h(X t )dB T t g(X t ) + b(X t )dt where g, h, b : R → R and X 0 ∈ Sp . Suppose that |g(x)h(x) -g(y)h(y))| 2 ≤ ρ(|x -y|), x, y ∈ R, (3.14)
where ρ : (0, ∞) → (0, ∞) is a Borel function such that 0 + ρ -1 (x)dx = ∞, that the functions G(x, y) = g 2 (x)h 2 (y) + g 2 (y)h 2 (x) is locally Lipschitz and strictly positive on {x = y} and that b is locally Lipschitz. Then, for t < τ , the pathwise uniqueness holds for the SDE (3.1).

Remark 2. The hypothesis in Theorem 5 on the strict positivity of G(x, y) off the diagonal {x = y} is equivalent to the condition that g and h have no more than one zero and their zeros are not common.

Remark 3. In the matrix SDE (3.1) the functions g and h appear only in the martingale part, whereas in the equations (3.2) and (3.3) they intervene also in the finite variation part. That is why a Lipschitz condition on the symmetrized function g 2 ⊕ h 2 cannot be avoided in a matrix Yamada-Watanabe theorem on S p .

Proof. We diagonalize X 0 = h 0 λ 0 h T 0 . We first show that the equations (3.2) and (3.3) have unique strong solutions when Λ 0 = λ 0 and H 0 = h 0 . The functions

b i (λ 1 , . . . , λ p ) = b(λ i ) + k =i G(λ i , λ k ) λ i -λ k , c ij (λ 1 , . . . , λ p , h 11 , h 12 , . . . , h pp ) = δ kj h ik G(λ j , λ k ) λ j -λ k , d ij (λ 1 , . . . , λ p , h 11 , h 12 , . . . , h pp ) = - 1 2 h ij k =j G(λ j , λ k ) (λ k -λ j ) 2 are locally Lipschitz continuous on D = {0 ≤ λ 1 < λ 2 < . . . < λ p } × [-1, 1] r , r = p 2 .
Thus, they can be extended from the compact sets

D m = {0 ≤ λ 1 < λ 2 < . . . < λ p < m, λ i+1 -λ i ≥ 1/m} × [-1, 1] r
to bounded Lipschitz continuous functions on R p+r . We will denote by b m i , c m ik and d m ij such extensions for m = 1, 2, . . .. We consider the following system of SDE (recall that β kj = β jk )

dλ m i = g(λ m i )dν i + b m i (Λ m )dt, i = 1, . . . , p, dh ij = k =j c m ij (Λ m , H) dβ kj (t) + d m ij (Λ m , H) dt, 1 ≤ i, j ≤ p.
Since |g(x)h(x) -g(y)h(y))| 2 ≤ ρ(|x -y|) and 0 + ρ(x) -1 dx = ∞, by Theorem 2 with q = 1 2 p(p -1), we obtain that there exists a unique strong solution of the above-given system of SDEs. Using the fact that D m ⊂ D m+1 , lim m→∞ D m = D and the standard procedure we get that there exists a unique strong solution (Λ t , H t ) of the systems (3.2) and (3.3) up to the first exit time from the set D. This time is almost surely equal to τ , the first collision time of the eigenvalues.

Suppose that X and X are two solutions of (3.1) with X 0 = X0 = h 0 λ 0 h T 0 . Consider the corresponding eigenvalues and eigenvectors processes (Λ, H) and ( Λ, H) with Λ 0 = Λ0 = λ 0 and H 0 = H0 = h 0 . We have just proved that Λ(t) = Λ(t) and H(t) = H(t) for every t > 0 a.s., so X(t) = X(t) a.s.

The Theorem 5 and the Proposition 1 imply the following global strong existence result for matrix SDEs on the positive cone S + p . Corollary 1. Consider functions g, h : R + → R + . Suppose that b, g 2 , h 2 are Lipschitz continuous, g 2 h 2 is convex or in class C 1,1 and that G(x, y) is strictly positive on {x = y}. Then the matrix SDE (3.1) on S + p admits a unique strong solution on [0, ∞). Proof. Recall that if a non-negative function F is Lipschitz continuous then √ F is 1/2-Hölder continuous. Observe that if g 2 and h 2 are Lipschitz continuous then g 2 h 2 is locally Lipschitz and gh is 1/2-Hölder. Thus (3.14) is verified and the Theorem 5 applies on [0, τ ). By the Proposition 1, τ = ∞ almost surely.

Applications

4.1. Noncolliding particle systems of squared Bessel processes. In a recent paper by Katori,Tanemura [START_REF] Katori | Noncolliding Squared Bessel processes[END_REF], particle systems of squared Bessel processes BESQ (ν) , ν > -1, interacting with each other by long ranged repulsive forces are studied. If there are N particles, their positions X (ν) i are given by the following system of SDEs, see [START_REF] Katori | Noncolliding Squared Bessel processes[END_REF] p.593:

dX (ν) i (t) = 2 X (ν) i (t)dB i (t) + 2(ν + 1)dt + 4X (ν) i (t) j =i 1 X (ν) i (t) -X (ν) j (t) = 2 X (ν) i (t)dB i (t) + 2(ν + N)dt + 2 j =i X (ν) i (t) + X (ν) j (t) X (ν) i (t) -X (ν) j (t) , i = 1, . . . , N
with a collection of independent standard Brownian motions {B i (t), i = 1, . . . , N} and, if -1 < ν < 0, with a reflection wall at the origin. It is shown in [START_REF] Katori | Noncolliding Squared Bessel processes[END_REF] and it follows from the Proposition 1 that the collision time τ = ∞ a.s. The Theorem 2 applied to such systems, with a standard use of localization techniques as in the proof of Theorem 5, gives the following Corollary 2. The system of SDEs for a particle system of N squared Bessel processes BESQ (ν) admits a unique strong solution on [0, ∞).

Wishart stochastic differential equations. Wishart processes on S +

p are matrix analogues of squared Bessel processes on R + . Wishart processes with shape parameter n (which corresponds to the dimension of a BESQ on R + ) are simply constructed as X t = N T t N t where N t is an n × p Brownian matrix. Let α > 0 and B = (B t ) t≥0 be a Brownian p × p matrix. The Wishart stochastic differential equation for a Wishart process with a shape parameter α is

   dX t = √ X t dB t + dB T t √ X t + αIdt X 0 = x 0 . (4.1)
It was introduced by Bru [3] by first writing the SDE for X t = N T t N t and next replacing the parameter n by α. It was shown in [START_REF] Bru | Wishart processes[END_REF] that if x 0 ∈ Sp and α ∈ (p -1, p + 1) then there exists a unique weak solution of (4.1) and the condition α ≥ p + 1 implies that (4.1) has a unique strong solution. We reinforce considerably these results. Our methods apply with g(x) = √ x, h(x) = 1 and G(x, y) = x + y for x, y ∈ R + . These functions satisfy the hypotheses of the Theorem 5 and the Proposition 1. First, using the Theorem 3 and the Proposition 1 we obtain Corollary 3. For α > 0 and 0 ≤ λ 1 (0) < λ 2 (0) < . . . < λ p (0) the eigenvalues λ i (t) never collide, i.e. the first collision time τ = ∞ almost surely.

Next, the Theorem 5 implies Corollary 4. The Wishart SDE (4.1) with x 0 ∈ Sp has a unique strong solution on [0, ∞) for α > 0.

Remark 4. Bru [START_REF] Bru | Wishart processes[END_REF] showed that for α > p -1 the Wishart processes have the absolutely continuous Wishart laws which are very important in multivariate statistics, see e.g. the monograph of Muirhead [START_REF] Muirhead | Aspects of multivariate statistical theory[END_REF]. The singular Wishart processes corresponding to α = 1, . . . p -1 are obtained as X t = N T t N t where N t is an α × p Brownian matrix. Then X 0 = N T 0 N 0 has eigenvalue 0 of multiplicity p -α so x 0 ∈ Sp . Thanks to our matrix Yamada-Watanabe Theorem, we discover a new and unexpected class of Wishart processes for α ∈ (0, p -1] and x 0 ∈ Sp , whose study is an interesting research objective.

Remark 5. Let Q ∈ S + p .
As observed in Bru [START_REF] Bru | Wishart processes[END_REF] p.746-747, X t is a solution to the matrix SDE (3.1) if and only if

Y t = QX t Q is a solution of dY t = Y t dB t Q + QdB T t Y t + αQ 2 dt. (4.2)
The process Y t is a Wishart process with shape parameter α and scale parameter Q 2 .

Observe that if Q = αI, the matrix SDE (4.2) has not the form (3.1) for any b, h : R + → R + . However, using the relation Y t = QX t Q and Theorem 5 it is easy to see that the SDE (4.2) has a unique strong solution.

Another perturbation of the Wishart SDE (4.1) is the equation for the Wishart process with constant drift c > 0, which may be also viewed as a squared matrix Ornstein-Uhlenbeck process More general squared matrix Ornstein-Uhlenbeck processes were first studied by Bru [START_REF] Bru | Wishart processes[END_REF] and recently by Mayerhofer et al. [START_REF] Mayerhofer | On strong solutions for positive definite jump-diffusions[END_REF]. Our strong existence and uniqueness result for (4.3) is not covered by these papers. A matrix Jacobi process of dimensions (q, r), with q ∧ r > p -1, and with values in S p [0, I], was defined and studied by Doumerc [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF] as a solution of the following matrix SDE, with respect to a p × p Brownian matrix

dX t = X t dB t + dB T t X t + αIdt + cX t dt, X 0 ∈ Sp . ( 4
B t    dX t = √ X t dB t I p -X t + I p -X t dB T t √ X t + (qI m -(q + r)X t )dt X 0 = x 0 ∈ S p [0, I]. (4.4)
In [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF] Th.9.3.1, p.135 it was shown that if q ∧ r ≥ p + 1 and x 0 ∈ Ŝp [0, I] then (4.4) has a unique strong solution in Ŝp [0, I]. In the case q or r ∈ (p -1, p + 1) and x 0 ∈ Sp [0, I] the existence of a unique solution in law was proved in [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF]. Our methods allow one to strengthen the results of Doumerc.

Corollary 5. Let q ∧ r > p -1 and x 0 ∈ Sp [0, I]. Then the matrix SDE (4.4) has a unique strong solution for t ∈ [0, ∞).

Proof. We apply Theorem 5 and Proposition 1 with g(x) = √ x, h(x) = √ 1 -x and b(x) = q -(q + r)x.

4.4. β-Wishart and β-Jacobi processes. As known from [START_REF] Bru | Diffusions of perturbed principal component analysis[END_REF] and by Theorem 3, the eigenvalues of the Wishart process verify the following system of SDEs

dλ i = 2 λ i dν i + α + k =i λ i + λ k λ i -λ k dt.
Let β > 0. One calls a β-Wishart process a solution of the system of SDEs

dλ i = 2 λ i dν i + β α + k =i λ i + λ k λ i -λ k dt. (4.5)
The β-Wishart processes were studied by Demni [START_REF] Demni | Note on radial Dunkl processes[END_REF]. In the theory of random matrices and its physical applications, the β-Wishart processes are related to Chiral Gaussian Ensembles, which were introduced as effective (approximation) theoretical models describing energy spectra of quantum particle systems in high energy physics. Usually a symmetry of Hamiltonian is imposed and it fixes the value of β to be 1, 2 or 4, respectively in real symmetric, hermitian and symplectic cases. On the other hand, from the point of view of statistical physics, β is regarded as the inverse temperature, β = 1/(k B T ), and should be treated as a continuous positive parameter. In this sense, the β-Wishart systems are statistical mechanics models of "log-gases" (The strength of the force between particles is proportional to the inverse of distances. Then the potential, which is obtained by integrating the force, is logarithmic function of the distance. So the system is called a "log-gas"). For more information on log-gases, see the recent monograph of Forrester [START_REF] Forrester | Log-gases and random matrices[END_REF]. In [START_REF] Demni | Note on radial Dunkl processes[END_REF] the existence and uniqueness of strong solutions of the SDE system (4.5) was established for β > 0 , α > p -1 + 1 β and t ∈ [0, τ ∧ R 0 ), where R 0 = inf{t| λ 1 = 0}. Our Theorem 2 and Proposition 1 imply the following Corollary 6. The SDE system (4.5) with 0 ≤ λ 1 (0) < λ 2 (0) < . . . < λ p (0) has a unique strong solution for t ∈ [0, ∞), for any α > 0 and β > 0.

The β-Jacobi processes (λ i ), i = 1, . . . , p are [0, 1] p -valued processes generalizing processes of eigenvalues of matrix Jacobi processes defined by (4.4):

dλ i = 2 λ i (1 -λ i )dν i + β q -(q + r)λ i + k =i λ i (1 -λ k ) + λ k (1 -λ i ) λ i -λ k dt. (4.6)
Indeed, for β = 1 the formula (4.6) was shown in [START_REF] Doumerc | Matrices aléatoires, processus stochastiques et groupes de refléxions[END_REF] and it follows directly from the Theorem 3. β-Jacobi processes were recently studied by Demni in [START_REF] Demni | β-Jacobi processes[END_REF]. He showed that the system (4.6) has a unique strong solution for all time t when β > 0 and q∧r > m-1+1/β. As an application of Theorem 2 and Proposition 1 we strengthen essentially this result.

Corollary 7. The SDE system (4.6) with 0 ≤ λ 1 (0) < λ 2 (0) < . . . < λ p (0) ≤ 1 has a unique strong solution for t ∈ [0, ∞), for any β > 0 and q ∧ r > m -1.

Remark 6. It would be interesting to extend our generalization of the Yamada theorem to the SDE's considered by Cépa-Lépingle [START_REF] Cépa | Brownian particles with electrostatic repulsion on the circle: Dyson's model for unitary random matrices revisited[END_REF]. On the other hand the Jacobi eigenvalues processes being an important example of the radial Cherednik processes, we conjecture that the strong existence and unicity would hold for radial Cherednik processes. For radial Dunkl processes this is proved by Demni [START_REF] Demni | Radial Dunkl processes: existence, uniqueness and hitting time[END_REF], using [START_REF] Cépa | Brownian particles with electrostatic repulsion on the circle: Dyson's model for unitary random matrices revisited[END_REF].

3. 4 .Theorem 5 .

 45 Matrix Yamada-Watanabe theorem. Consider the matrix SDE (3.1) on S p dX

. 3 )

 3 This equation has the form (3.1) with g(x) = √ x, h(x) = 1 and b(x) = cx. By Theorem 5 and Proposition 1, it has a unique strong solution with t ∈ [0, ∞) for any α, c > 0.

4. 3 .

 3 Matrix Jacobi processes. Let 0 p and I p be zero and identity p × p matrices. Define S p [0, I] = {X ∈ S p | 0 p ≤ X ≤ I p }. Denote by Ŝp [0, I] = {X ∈ S p | 0 p < X < I p } and by Sp [0, I] the set of matrices in S p [0, I] with distinct eigenvalues.

Acknowledgements. We thank N. Demni, C. Donati, M. Katori and M. Yor for discussions and bibliographical indications.

The authors were supported by MNiSW grant N N201 373136 and the l'Agence Nationale de la Recherche grant ANR-09-BLAN-0084-01.