From Orchestration to Choreography through Contract Automata

We study the relations between a contract automata and an interaction model. In the former model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The interaction model relies on channel-based asynchronous communication and choreography to coordinate distributed services. We define a notion of strong agreement on the contract model, exhibit a natural mapping from the contract model to the interaction model, and give conditions to ensure that strong agreement corresponds to well-formed choreography.

Introduction
We investigate the relations between two models of distributed coordination: contract automata [3] and communicating machines [4].
The former model has been recently introduced as a contract-based coordination framework where contracts specify the expected behaviour of distributed components oblivious of their communicating partners. The underlying coordination mechanism of contract automata is orchestration. In fact, such model envisages components capable of communicating messages on some ports according to an automaton specifying the component's behavioural contract. These messages have to be thought of as directed to an orchestrator synthesised out of the components; the orchestrator directs the interactions in such a way that only executions that "are in agreement" happen. In this way, it is possible to transfer the approach of [2,1] to contract automata so to identify misbehaviour of components that do not realise their contract.
We illustrate this with the following simple example. Alice is willing to lend her aeroplane toy, Bob offers a bike toy in order to play with an aeroplane toy, while Carol wants to play with an aeroplane or a bike toy. Let a and b denote respectively the actions of offering an aeroplane or a bike toy and, dually, a and b denote the corresponding request actions. The contract automata for Alice, Bob, and Carol correspond to the following regular expressions, used here for conciseness: If Alice exchanges her toy with Bob, then all contracts are fulfilled. Instead, if not coordinated, Alice, Bob, and Carol may share their toys in a way that does not fulfill their contracts. In fact, Alice can give her aeroplane to Bob or Carol, while Carol can receive the bike from Alice or Bob, therefore if Alice gives her aeroplane to Carol the contracts of Alice and Carol are fulfilled while Bob's contract is not. In the model of contract automaton the coordinator acts as the mam of the three kids who takes their desires and suggests how to satisfy them (and reproaches those who do not act according to their declared contract).
Communicating machines -the other model we consider here -were introduced with the aim of studying distributed communication protocols and ensure the correctness of distributed components again formalised as automata. But -unlike contract automata -communicating machines do not require an orchestrator since they interact directly with each other through (FIFO) buffers. In fact, a relation between communicating and distributed choreographies has been recently proved in [8].
We show that these models -invented to address different problems and having different coordination mechanisms -are related. For this purpose, we introduce the notion of strong agreement, which requires the fulfillment of all offers and requests. Strong agreement differs from previous notions of agreements for contract automata (cf. Section 3) and enables us to introduce strongly safe contract automata, that is those automata accepting only computations that are in strong agreement. Strong agreement and safety are key to establish a correspondence from contract automata to communicating machines.
Indeed if a contract automaton enjoys strong safety (and it is well-behaved on branching constructs) then the corresponding communicating machines are a well-formed choreography.
Structure of the paper. We recall contract automata and communicating finite-state machines in Section 2. The new notion of agreement on contract automata is in Section 3. The translation of contract automata into communicating machines is given in Section 4 where we also prove our main theorem. In Section 5 we discuss possible extensions of our results to other notions of agreement for contract automata and semantics for communicating machines. Finally, concluding remark are in Section 6.

Background
This section summarises the automata models we use in the paper. Both models envisage distributed computations as enacted by components that interact by exchanging messages. As we will see, in both cases components, abstracted away as automata, yield systems also formalised as automata.

Contract Automata
Before recalling contract automata (introduced in [3]), we fix our notations and preliminary definitions. Given a set X , as usual, X * def = n≥0 X n is the set of finite words on X (ε is the empty word, ww ′ is the concatenation of words w, w ′ ∈ X * , w (i) denotes the i-th symbol of w, and |w| is the length of w); write x n for the word obtained by n concatenations of x ∈ X and x * for a finite and arbitrarily long repetition of x ∈ X . It will also be useful to consider X n as a set of tuples and let x to range over it. Sometimes, overloading notation (and terminology), we confound tuples on X with words on X (e.g., if w ∈ X n , then | w| = n is the length of w and w (i) denotes the i-th element of w).

Transitions of contract automata will be labelled with elements in the set
• requests of components will be built out of R while their offers will be built out of O, • ∈ R ∪ O is a distinguished label to represent components that stay idle.
We let a, b, c, . . . range over L and fix an involution · : L → L such that A contract automaton (cf. Def. 2) represents the behaviour of a set of participants (possibly made of a single participant) capable of performing some actions; more precisely, as formalised in Def. 1, the actions of a contract automaton allow them to " advertise" offers, "make" requests, or "handshake" on simultaneous offer/request matches.
We define the relation ⊲⊳⊆ L * × L * as the symmetric closure of • a 1 and a 2 are actions of the same length We write a 1 ⊲⊳ b a 2 when there is b ∈ R ∪ O such that a 1 and a 2 are actions on b and a 1 ⊲⊳ a 2 .
Fact 1 ⊲⊳ is an equivalence relation on L * . Definition 2 (Contract Automata) Let Q (ranged over by q 1 , q 2 , . . .) be a finite set of states. A contract automaton of rank n is a (finite-state) automaton A = Q n , q 0 , L n , T, F , where • q 0 ∈ Q n is the initial state • F ⊆ Q n is the set of accepting states , the i-th participant stays idle) and -a is either a request, or an offer, or else a match action A principal is a contract automaton A of rank 1 such that, for any two transitions (q 1 , a 1 , q ′ 1 ), (q 2 , a 2 , q ′ 2 ) in A , it is not the case that a 1 ⊲⊳ a 2 .

Example 1
The principals of Alice, Bob, and Carol in Section 1 are given below

Automaton of Alice Automaton of Bob Automaton of Carol
Given a contract automaton A = Q n , q 0 , L n , T, F of rank n, usual definitions and constructions of finite-state automata apply. In particular, where → * is the reflexive and transitive closure of →. As usual, s 1 − →s m+1 (for some s 2 , . . . , s m ) and s → iff for no s ′ it is the case that s → s ′ .
We now borrow from [3] the product operation of contract automata. Given a finite set of contract automata, this operation basically yields the contract automaton that interleaves all their transitions while forcing synchronisations when two contract automata are in states ready to "handshake" (i.e. , they can fire complementary request/offer actions).

Definition 3 (Product) Let
The product of A 1 , . . . , A h , denoted as i∈{1,...,h} A i , is the contract automaton Q n , q 0 , L n , T, F of rank n = n 1 + . . . + n h where: or c (i) = a i , c (l) = n l for each l = i ∈ {1, . . . , h}, and q ′ = q 1 . . . q i−1 q ′ i q i+1 . . . q h when ( q i , a i , q ′ i ) ∈ T i and for all j = i and ( q j , a j , q ′ j ) ∈ T j it does not hold that a i ⊲⊳ a j .

Example 2
The contract automaton below is the product of the contract automata in Example 1.
Notice that from the states q 0 and q 6 (where participants can handshake) only match actions depart; offer and request actions are not included in the product.

Remark 1
Notice that the product in Def. 3 is not associative; an alternative (but more complex) definition of associative product can be given by "breaking" existing matches when composing automata [3].
Hereafter, we assume that all contract automata of rank n > 1 are the product of n principals. Also, we consider deterministic contract automata only. Such assumptions could be relaxed at the cost of adding some technical intricacies.

Communicating Machines
Communicating machines [4] are a simple automata-model introduced to specify and analyse systems made of agents interacting via asynchronous message passing. We adapt the original definitions and notation from [4] and [7] to our needs; in particular, the only relevant difference with the original model is that we have to add the set of final states. Let P be a finite set of participants (ranged over by p, q, r, s, etc.) and C def = {pq p, q ∈ P and p = q} be the set of channels.

Remark 2
The set P can be thought of as the set of integers {1, . . . , n} (and likewise for contract automata). However, we adopt a different notation to make the translation from contract automata to communicating machines clearer.
The set of actions is Act def = C × (R ∪ O) and it is ranged over by ℓ; we abbreviate (sr, a) with a@sr when a ∈ O (representing the sending of a from machine s to r) and, similarly, we shorten (sr, a) with a@sr when a ∈ R (representing the reception of a by r).

Definition 4 (CFSM) A communicating finite-state machine is an automaton
where Q is a finite set of states, q 0 ∈ Q is the initial state, δ ⊆ Q × Act × Q is a set of transitions, and F ⊆ Q is the set of final states. We say that M is deterministic iff for all states q ∈ Q and all actions ℓ ∈ Act, if (q, ℓ, q ′ ), (q, ℓ, q ′′ ) ∈ δ then q ′ = q ′′ . Also, we write L (M) ⊆ Act * for the language on Act accepted by the automaton corresponding to machine M.
We will consider only deterministic CFSMs. The notion of deterministic CFSMs adopted here differs from the standard one which requires that, for any state q, if (q, a@sr, q ′ ) ∈ δ and (q, b@sr, q ′′ ) ∈ δ then a = b and q ′ = q ′′ (see e.g., [7]). The reason for the definition is to reflect the semantics of contract automata.
The communication model of CFSMs (cf. Definitions 5 and 6) is based on (unbounded) FIFO buffers -the channels in C -used by participants to exchange messages. To spare another syntactic category and cumbersome definitions, we draw the messages appearing in the buffers of CFSMs from the set of requests R. Recall that the set of participants P is finite.

Definition 5 (Communicating systems) Given a CFSM M
Hereafter, we fix a machine M p = (Q p , q 0p , R ∪ O, δ p , F p ) for each participant p ∈P and let S = (M p ) p∈P be the corresponding system.
We write s − → s ′ for ∃ℓ : s ℓ − →s ′ and denote with → * the reflexive and transitive closure of →. The set of reachable configurations of S is RS(S) = {s s 0 → * s}. A sequence of transitions is k-bounded if no channel of any intermediate configuration on the sequence contains more than k messages.
Condition (1) in Def. 6 puts the content a on a channel sr, while (2) gets the content a from sr.

Notational Synopsis
To avoid their continuous repetition, through the paper we assume fixed a contract automaton A = Q n , q 0 , L n , T, F of rank n.
For readability we summarise the notations introduced so far in the following table.
X * set of finite words on a set X ; ε is the empty word x concatenated n-times (resp. arbitrarily many) with itself contract automata of rank n P set of participants (ranged over by p, q, i, j,A, B,C, etc.) C set of channels (ranged over by pq) M p communicating machine of participant p S a system of communicating machines Finally, we assume that the states of any automaton/machine are build out of a universe Q (of states).

Enforcing Agreement
This section introduces a new notion of agreement on contract automata -called strong agreement -that elaborates the notions of agreement and weak agreement introduced in [3]. The three notions differ on the conditions for the fulfillment of an interaction between different principals. Briefly, an agreement exists if all the requests, but not necessarily all the offers, are satisfied synchronously. Intuitively, this means that the orchestrator "simultaneously" guarantees two participants that their complementary actions are matched. Instead, a weak agreement exists when request actions can be performed "on credit". In other words, a computation yelds weak agreement when the fulfillment of a request action can happen after the action has been taken. Intuitively, this corresponds to an asynchronous communication admitting actions taken on credit provided that obligations will be honored later on.
Here, we focus on strong agreement, which strengthens the previous notion of agreement by requiring the fulfillment of all offers and requests in a synchronous way. In Section 4 we will show how this condition corresponds to interactions between communicating machines.

Definition 7 (Strong Agreement and Safety) A strong agreement on L is a finite (non-empty) sequence of match actions. We let Z to denote the set of all strong agreements on L.
A contract automaton A is strongly safe if L (A ) ⊆ Z, otherwise it is strongly unsafe. We say that A admits strong agreement when L (A ) ∩ Z = / 0.
Note that ε does not belong to Z; the reason is that ε would not be an interesting agreement because it does not require any interaction (neither with the controller nor between principals). For this we require that the initial states of contract automata are not accepting states. We show how to generate a strongly safe composition of contracts with an approach borrowed by the supervisory control theory for discrete event systems [6]. In this theory, discrete event systems are basically automata where accepting states represent the successful termination of a few tasks while forbidden states are those that should not be traversed in "good" computations. The purpose is then to synthesize a controller that enforces this property. The supervisory control theory distinguishes between controllable events (those events that the controller can disable) and uncontrollable events (those that are always enabled). Moreover, the theory partitions events in observable and unobservable; the latter being a subset of uncontrollable events. It is known that if all events are observable then a maximally permissive controller exists that never blocks a good computation [6].
Since the behaviors that we want to enforce in A are exactly those traces labeled by words in Z ∩ L (A ), we specialise the notions of supervisory control theory by defining • observable events to be all offer, request, and match actions; • forbidden events to be non-match actions.

Definition 8 (Controller) A (strong) controller of A is a contract automaton KS
Note that the most permissive controller is unique up-to language equivalence.

Example 3
The MPC of the contract automaton in Example 2 consists of the states q 0 , q 1 , q 3 , and q 4 with transitions ( q 0 , (a, a, ),

Proposition 1 If KS
is the intersection of two regular languages and all actions are controllable, there exists a contract automaton KS ′ A accepting it (cf. [6]). By definition, KS ′ A is a controller of A strictly containing L (KS A ), contradicting the hypothesis that L (KS A ) is the most permissive controller.
A state q of a contract automaton A is called redundant if, and only if, from q no accepting state of A can be reached.

is a match transition}, F is the sub-automaton of A consisting of the match transitions of A only.
Proof. By construction, the transitions of KS A are a subset of the transitions of A , hence L (KS A ) ⊆ Z ∩ L (A ). Therefore KS A is a controller of A and we have just to prove that L (KS A ) = Z ∩ L (A ). We proceed by contradiction.
Let w ∈ (Z ∩ L (A )) \ L (KS A ). Since Z does not contain the empty string we have w = ε and there must be a transition t = ( q, a, q ′ ) not in KS A in the accepting path of w (which is unique since we consider deterministic contract automata only), otherwise w ∈ L (KS A ). We know that a is a match action because w ∈ Z, and q, q ′ are not redundant states of A because the transition belongs to an accepting path. Hence there must be t ∈ KS A , since by construction match transitions between non-redundant states are in KS A .

Example 4
The MPC of Example 3 is obtained from the CA in Example 2 by applying the construction of Lemma 2.
The controlled system of a contract automaton A identifies the match transitions of A and those transitions that lead "outside" of the controller; for this we use a distinguished state ⊥ ∈ Q n (for any n) in the following definition.

Definition 9 (Controlled system) Let KS
The controlled system of A under KS A is defined as the automaton ( q 1 , ( , , a), q 2 ), ( q 0 , (a, , a), q 6 ) to the MPC of Example 3.

Example 5 The controlled system of the CA in Example 2 is obtained by adding the transitions
It is worth remarking that the transitions reaching ⊥ in the controlled system of A identify the start of the computations in A which lead to violations of strong agreement.
In the next definition, we introduce a notion of strong liability, to single out the principals that are potentially responsible of the divergence from the expected behaviour.
Definition 10 (Strong Liability) Given a controlled system KS A /A , the set of liable participants on a trace w ∈ L (A ) is given by: We let TLiable(KS A /A ) to denote the set of transitions of A that make principals liable.
Note that the transition labelled by a in Definition 10 is the first which diverges from the expected path (since, by Definition 9, state ⊥ does not have outgoing transitions). Indeed a liable index identifies a principal that fires an action taking the computation away from agreements.

Example 6
The liable indexes of the contract automaton in Example 2 are 1 and 3, corresponding to Alice and Carol respectively; the transitions that make them liable are respectively q 0 , (a, , a), q 6 and q 1 , ( , , a), q 2 . The former liable transition is a match that leads to a non-match transition.
Note that labels allow us to track participants firing actions so to find (the indexes of) the liable principals. Our aim is to restrict the behaviour of principals so that they follow only the traces of the automaton which lead to strong agreement, while avoiding the others.

From Contract Automata to Communicating Machines
The translation of a principal into a communicating machine is conceptually straightforward. Indeed, the translation just yields a machine isomorphic to a principal in the composed contract automaton; the only difference are the labels. To account for the "openness" nature of contract automata -where principals can fire transitions not matched by other principals -in Definition 11 below we use the '−' symbol representing a special ("anonymous") participant distinguished by the participants corresponding to the principals and playing the role of the environment. For this reason, we will assume from now on that actions in Act are built on C ∪ {−}.
Definition 11 (Translation) The translation a p ∈ Act of an action a on L n respect to a participant p (with 1 ≤ p ≤ n) is defined as: a@ij if a is a match action and i and j are such that a (i) ∈ O and a ( j) ∈ R and p = i a@ij if a is a match action and i and j are such that a (i) ∈ O and a ( j) ∈ R and p = j a@i− if a is an offer action and i is such that a (i) ∈ O and p = i a@−j if a is a request action and j is such that a ( j) ∈ R and p = j ε otherwise The translation of A to a CFSM is given by the map ..,n} the communicating system obtained by translating the contract automaton A .
Given ϕ ∈ L n * , we define The product is the contract automaton below with initial state q 0 = q 01 , q 02 , q 03 a, ) ( , , c) By applying Lemma 2 on the product automaton we obtain the MPC: We introduce the 1-buffer semantics of communicating machines, recall that w is the vector of buffers. Intuitively, this semantics forbids a machine to send a message to one of its partners if there is a non empty channel in the system.

Definition 12 (1-buffer, deadlock,convergent) A configuration ( q; w) of a CS S = (M p ) p∈P is stable if
and only if w = ε, while is final if it is stable and q ∈ (F p ) p∈P . The 1-buffer semantics of S is given by the relation where → is the relation introduced in Definition 6 and We say that the system S is convergent if and only if for every reachable configuration ( q; w) it is possible to reach a final configuration in the 1-buffer semantics.

Moreover a configuration ( q; w) is a deadlock if and only if is not final and ( q; w) ։
Note that if a system is convergent than it is deadlock-free. The 1-buffer semantics above is instrumental to the relation we establish between strong agreement of contract automata and convergence of CFMSs.

Remark 3
Note that by considering only finite traces, we rule out all the unfair traces. For example, consider the following strongly safe CA: If the first and second participants could execute the transition ( q 0 , (a, a, ), q 0 ) infinitely often then the third participant would be prevented from reading the message b. This behaviour is ruled out by considering only finite traces. Indeed all the possible traces generated by the automaton above are described by the regular expression (a, a, )  *  (b, , b), where the third participant will eventually reach its goal.
We define snd( a) def = i when a is a match action or an offer action such that a (i) ∈ O and, similarly, rcv( a) def = j when a is a request or a match and j is such that a ( j) ∈ R.

Property 3 Let S(KS A ) be a CS obtained by Definition 11, and s 0 be its initial configuration. Then for
all f such that s 0 f ։ there is a strong agreement ϕ such that f = ϕ or f = ϕ a@ij for some a, i, j. Proof. The proof follows trivially by observing that KS A contains only match transitions and that the 1-buffer semantics does not allow other behaviours for the CS.
Before providing the main results, we introduce a notion of well-formedness of contract automata. We require that an output action of a participant in a particular state is independent from the states of the other participants in the system.  ( q 1 , (a, a, ), q i ) ∈ T KS . The next theorem characterizes the relations between a CA and the corresponding CS. It states that the CS is capable of performing all the moves of the controller of the CA, while the CA is capable of performing those traces of the CS that are in strong agreement. Moreover, if a CA has the branching condition, the runs of the CS leading to a deadlock configuration correspond in CA to runs traversing liable transitions, and likewise when the CS reaches a non-deadlock configuration which does not reach a final configuration. 1 with a match action on a where principal i makes the offer and principal j makes the request on a. Let q 0(i) and q 0( j) be the initial states of participants i and j in S(KS A ). By Definition 11, we have for some q 1 and q 2 that ( q 0(i) , a@ij, q 1(i) ) and ( q 0( j) , a@ij, q 2(i) ) are transitions of participants i and j, respectively. We have s 2 a@ij ։ a@ij ։ s ′ 2 since after the first transition participant j remains in its initial state. 2. The proof is again by induction. Assume s 2 a ։ s ′ 2 , where a is a match on a which involves (the principals i and j corresponding to) participants i and j. As before let i perform the offer and j the request. By Definition 3 (of product), we have that there is a transition ( q 0 , a, q) in A from its initial state.

Theorem 1 Let S(KS
When |ϕ| > 1, we have s 2 ϕ ։ s ′′ 2 a ։ s ′ 2 and there is w ′ ∈ (L n ) * such that (by the induction hypothesis) Reasoning as in the base case, we conclude that A has a transition of the form ( q ′ , a, q ′′ ).
3. Let s ′ 2 = ( q; w) be the deadlock configuration reached from s 2 with f .
We distinguish two cases: • if w = ε (namely some buffer in w is not empty) thenφ is not a strong agreement (in fact, if it were a strong agreement then the 1-buffer semantics of S(KS A ) would yield w = ε). Then by Property 3 we have f = ϕ a@ij andφ = ϕ a. Moreover, Theorem 1.1 guarantees that a run s 0 ϕ − →s ′ 0 = ( q ′ , w ′ ) exists in A and, by Definition 11 and the branching condition, there is a transition ( q ′ , a, q ′′ ) in A where a is a match action on a. By contradiction, assume that there is no liable transition in the run s 0  Definition 12), the state q of configuration s ′ 2 = ( q; w) is not final, there is no participant ready to fire an output, and there is a participant waiting for an input on one of its buffers. The latter condition is guaranteed by the construction of CFSMs from controllers. Since w = ε, we have f = ϕ andφ = ϕ where ϕ ∈ Z and there is a run s 0 ϕ − →s ′ 0 = ( q 1 , w ′ ) in A (by Theorem 1.2). Note that q 1 is redundant in KS A (otherwise by Theorem 1.1, s ′ 2 would not be a deadlock configuration) and, by construction (Lemma 2), q 1 is removed from KS A . This implies that a liable transition has been traversed in s 0 ϕ − →s ′ 0 .
4. Wlog we can assume that ϕ is a strong agreement ( otherwise we have s 2 ϕ a@ij ։ s ′ 2 for some i, j, a and since s ′ 2 is not a deadlock it is possible to perform the step s ′ 2 a@ij ։ s ′′ 2 and we have that ϕ a is a strong agreement where a is a match action with a (i) = a, a ( j) = a). Moreover, from s ′′ 2 is not possible to reach a final state, and we apply the following reasoning to s ′′ 2 , ϕ a instead of s ′ 2 , ϕ. Note that the converse of Theorem 1.3 does not hold. Indeed if a CA A passes through a liable transition, it can be that S(KS A ) never reaches a deadlock configuration.

Example 9 Consider the CAs and CMs of Example 7. A possible trace belonging to the system S(KS A⊗B⊗C )
is generated by the transitions: (q 01 , a@AB, q 11 ), (q 01 , a@AB, q 21 ). By using Theorem 1.2 this trace corresponds to the liable transition ( q 0 , (a, a, ), q 7 ) of the product automaton.
However after this two steps the system S(KS A⊗B⊗C ) will never reach a deadlock configuration. Indeed, it is always possible to perform the transitions:(q 1 1 , a@AB, q 11 ), (q 21 , a@AB, q 21 ). Note that S(KS A⊗B⊗C ) is deadlock-free but not convergent.
We are now ready to state our main result: the controller of a CA has the branching condition if and only if the corresponding CS is convergent.   ( q, w). We distinguish two cases:

Theorem 2 Let A be a contract automaton, KS A be its MPC, and S(KS
• s ′ 2 is not a deadlock configuration. Then by applying Theorem 1.4 we have ϕ = ϕ 1 aϕ ′′ for some ϕ 1 , a, ϕ ′′ such that q 0 Note that a is a match action, otherwise a participant in S(KS A ) has fired an action to the environment in ϕ. Since S(KS A ) is derived from KS A and all the transitions of KS A are match, this is not possible. Assume a is an action on a with snd( a) = i, rcv( a) = j for some i, j ∈ P.
By hypothesis we know that s 2 ։ , hence in the configuration s ′ 2 the participant i is able to fire the action a@ij. By Definition 11, 3 there must be a state q 2 in KS A such that ( q 2 , a, q 3 ) is a transition in KS A (recall that S(KS A ) is derived from KS A ) and q 2(i) = q 1(i) (otherwise we would not have s ′ 2 a@ij ։ ), and since ( q 1 , a, q ′ 1 ) ∈ TLiable(KS A /A ) we conclude that the branching condition does not hold in KS A , obtaining a contradiction.  ( q 1 , w). As the previous case, by Definition 11, 3 there must be a state q 2 in KS A such that ( q 2 , a, q 3 ) is a transition in KS A where a is a match an action on a with snd( a) = i, rcv( a) = j and q 2 (i) = q 1 (i) . Moreover since s ′ 2 is a deadlock, it must be that there is no transition ( q 1 , a, q 4 ) in KS A , otherwise by Theorem 1 . 1 we have s ′ A consequence of Theorem 2 is that a strongly safe CA has the branching condition if and only if the corresponding CS is convergent.

Corollary 4 Let A be a contract automaton, then A is strongly safe and has branching condition if and only if S(A ) is convergent.
Proof. The statement follows trivially by notice that if A is strongly safe then A = KS A , hence KS A has the branching condition and we can apply Theorem 2.   ( , a, , a) which is not available in state q 3 , and from state q 3 we have the match transition ( , a, a, ) which is not available from state q 1 . The translation yields the CMs: A deadlock configuration is generated by the trace a@AC.a@AC.a@BC.
Example 11 Figure 1 ( q 9 , (d, , d), q ′ ) in KS A for some q ′ . Moreover there is a liable transition with label ( q 9 , ( , , d), ⊥) in Figure 1 which represents the possible deadlock in the system.

depicts the automaton KS
A deadlock configuration in S(KS A ) is given by the trace ϕ d@CA where: In the configuration s ′ 0 = ( q, w) the buffer w is not empty, because w (CA) = d. Moreover the machine A is prevented to read the message on the buffer since its configuration in q is ok@BA.d@CA.

On extending the approach
We discuss possible extensions of our approach to other existing types of agreement on CAs, and on different semantics of CMs, where there are no constraints on the number of messages in a buffer. We start by comparing the other existing types of agreement with the 1-buffer semantics for CMs.

On agreement
The property of agreement requires that all the requests are matched. It allows strings made by match and offer actions only. In the following we discuss a correspondence similar to Theorem 2 for the property of agreement.
Example 12 Consider the CAs corresponding to the regular expressions A = b.d + c.e+ d.e and B = d.e. The controller K A⊗B for the property of agreement is given by the CA: The translation in Definition 11 yields the CMs: Under the 1-buffer semantics, the system S(K A⊗B ) always reaches a deadlock configuration since in every execution there are messages in the buffer with no receiver, corresponding to the offer actions in the controller.
If we assume that the unmatched offers are consumed instantaneously by an artificial participant representing the environment, we still have possible deadlock configurations in S(K A⊗B ), for example if the participants execute the sequence of transitions ( q 0 1 , b@A−, q 1 1 ), ( q 0 2 , d@B−, q 2 2 ), ( q 2 2 , e@BA, q 3 2 ).
Note that K A⊗B has no branching condition: in q 1 , q 3 the participant B is the state q 0 2 , but from q 3 there is no match transition on action d.
Under the assumptions that the offer actions are consumed by the environment, that it is possible to prove that the controller of the CA A has a slightly modified version of the branching condition if and only if the corresponding system S(K A ) is convergent. The proof is obtained by noticing that in the 1-buffer semantic a deadlock configuration is reached only if a participant A send a message a to a participant B and B is unable to consume the message. By Definition 11 this can happen only if there are two different states in the CA where A is in the same internal state and the match transition is available only in one of the two states, i.e. K A has no branching condition. We also need to consider those configurations which are not convergent nor deadlocks as done in Theorem 2.
On weak agreement For the property of weak agreement things are more intricate, indeed it is necessary to modify the actual translation. This is due to the possibility for a participant to fire a request if in the future the offer will be available, while in the CMs if the buffer is empty it is not possible to perform an input action.
To overcome this problem it is possible to synthesize one or more CMs which act as brokers. They receive as input all the actions of the participants, which are now translated into outputs, and reply with messages in a way to drive the participants through the trace in weak agreement.

On different semantics
We now discuss the relations between CAs and other semantics for CMs.
Example 13 Consider the following CA A ⊗ B: We have A = a + b, B = b + a. This CA is strongly safe and has the branching condition. However, by considering the non 1-buffer semantics for CMs, the translated system is not deadlock free. Indeed a possible deadlock in S(K A⊗B ) is generated if the first participant performs the action a@AB and then the second performs the action b@BA. This is because participant B can ignore the message received by the participant A and follow the other branch of the CA. These behaviours is not permitted by the 1-buffer semantics, which forces participants to follow the successful branch.
The previous example shows that if we allow a less constrained semantics for CMs then Theorem 2 does not hold any more. Indeed, we need to introduce other constraints on the behaviour of the CAs to obtain a correspondence with convergent systems.
Note that in the previous example, from state q 0 both participants contain a branch where they can execute an input or an output action. This is called a mixed choice state. It is possible to prove that if a CA has the branching condition, it is strongly safe and has no mixed choice states then the corresponding system is convergent with non 1-buffer semantics. However the converse does not hold. Indeed there exists systems with mixed choice states that enjoy convergence.
Example 14 Consider the following CA A ⊗ B: We have A = a.b + b.a, B = b.a + a.b. This CA is strongly safe, has the branching condition, and contains a mixed choice state, i.e. q 0 . Nevertheless, the corresponding system is convergent.
As showed by the previous example, for obtaining a correspondence similar to Theorem 2, we need to consider those bad mixed choices, where the participants behave differently in the different branches.

Concluding Remarks
We have established a formal correspondence between contract automata, an orchestration model, and communicating machines, a model of choreography. An interesting implication of our results is that contract automata can be seen as an alternative semantics of communicating machines. In fact, the product of communicating machines could be built as a contract automaton once match-actions are properly defined as tuples where output messages appear before the corresponding input ones. However, contract automata are more general in the sense that they would also admit matches where a request appears before its corresponding offer. Exploring those alternative semantics is of interest and it is scope for future work.
The dichotomy orchestration-choreography has been discussed in many papers (see e.g., [9]). The only formal results (we are aware of) that link a choreography to an orchestration framework is in [5]. A precise comparison with [5] is not straightforward as the models use a bisimulation-like relation to exhibit a conformance relation between choreographed and orchestrated computations. Here, we study the conditions to "force" orchestrated computations to well-behave (strong safety), and convergence in a choreography framework in terms of strong safety in the orchestration one.
A practical outcome of our result is that strong safe contract automata can execute without controller (if they are trusted). In fact, one can translate them into communicating machines that run without central control.
For the time being, our result only states that strong agreement corresponds to the 1-buffer semantics of communicating machines. In other words, the execution of the machines is basically synchronous. (We note that this has some advantages since communicating machines with 1-buffer semantics are more computationally tractable [7].) We conjecture that results similar to the one presented in this paper can be achieved for weaker notions of agreement (for example, the ones in [3]) when considering asynchronous behaviours of communicating machines. This is nonetheless left as future work.


extfieldsofstudy:
Computer Science
Mathematics

text:
Matrix Completion in Colocated MIMO Radar: Recoverability, Bounds&Theoretical Guarantees

It was recently shown that low rank matrix completion theory can be employed for designing new sampling schemes in the context of MIMO radars, which can lead to the reduction of the high volume of data typically required for accurate target detection and estimation. Employing random samplers at each reception antenna, a partially observed version of the received data matrix is formulated at the fusion center, which, under certain conditions, can be recovered using convex optimization. This paper presents the theoretical analysis regarding the performance of matrix completion in colocated MIMO radar systems, exploiting the particular structure of the data matrix. Both Uniform Linear Arrays (ULAs) and arbitrary 2-dimensional arrays are considered for transmission and reception. Especially for the ULA case, under some mild assumptions on the directions of arrival of the targets, it is explicitly shown that the coherence of the data matrix is both asymptotically and approximately optimal with respect to the number of antennas of the arrays involved and further, the data matrix is recoverable using a subset of its entries with minimal cardinality. Sufficient conditions guaranteeing low matrix coherence and consequently satisfactory matrix completion performance are also presented, including the arbitrary 2-dimensional array case.

4)
We then generalize our coherence results for the more general case of arbitrary 2-dimensional transmission and reception arrays, showing that the coherence of the corresponding data can be easily and tightly bounded by simply looking at the values of the squared magnitude of a 2-dimensional complex function over a properly chosen subset of the x/y plane, directly related to the target angles. Essentially, by choosing a candidate pair of transmission/reception array topologies, this general result produces coherence bounds in a straightforward way, also holding true almost surely. An important implication of the results presented in this paper is that the performance of matrix completion in colocated MIMO radar systems is completely independent of any other system design specification or target characteristic, except for the transmission/reception array topology, the target angles and possibly the wavelength of the carrier. That is, as far as matrix completion is concerned, the values of various important quantities, such as target reflection coefficients, Doppler shifts, pulse repetition intervals and the choice of the waveform dictionary are completely unconstrained. This fact makes matrix completion very appealing for reducing the number of samples needed for accurate detection and estimation in real world colocated MIMO radar systems. Also, compared to Compressive Sensing (CS) based MIMO radar, matrix completion has at least the same advantage in terms of sample reduction, justified by the strong theoretical guarantees presented here, while at the same time it avoids the angle discretization and basis mismatch issues inherent in CS-based approaches [12], [13], [14].
The paper is organized as follows. In Section II, we briefly introduce the required background in both noiseless and noisy matrix completion. We also restate the problem formulation for the MIMO radar case in a slightly more general form compared to [10]. In Section III, we present our coherence and recoverability results for ULA transmitter/receiver pairs, complete with detailed proofs and explanations. In Section IV, we present the generalization to the aforementioned coherence results for arbitrary 2-dimensional transmission/reception arrays, along with an instructive example. In Section IV, we state and prove a result for some special cases of spatial target configurations, completing our theoretical analysis. Finally, in Section V, we discuss further implications of our previously stated results and we present some simulations, validating their correctness.

A. Noiseless Matrix Completion: Problem Statement and Recoverability Conditions
Consider a generic complex matrix M ∈ C N 1 ×N 2 of rank r, whose compact Singular Value Decomposition (SVD) is given by M = UΣV H ≡ i∈N + r σ i (M) u i v H i and with column and row subspaces denoted as U and V respectively, spanned by the sets u i ∈ C N 1 ×1 i∈N + r and v i ∈ C N 2 ×1 i∈N + r , respectively.
Let P (M) ∈ C N 1 ×N 2 denote an entrywise sampling of M. In all the analysis that follows, we will adopt the theoretical frameworks presented in [4] and [5], according to which one hopes to reconstruct M from P (M) by solving the convex program minimize X * subject to X (i, j) = M (i, j) , ∀ (i, j) ∈ Ω , where the set Ω contains all matrix coordinates corresponding to the observed entries of M (contained in P (M)) and where X * represents the nuclear norm of X. In the following, we will refer to (1) as the Matrix Completion (MC) problem. Also in [4], the authors introduce the notion of subspace coherence, in order to derive specific conditions under which the solution of (1) coincides with M. The formal definition of subspace coherence follows, in a slightly more expanded form compared to the original definition stated in [4].

Definition 1. (Subspace Coherence [4])
Let U ≡ C r ⊆ C N be a subspace spanned by the set of orthonormal vectors . Also, define the matrix U [u 1 u 2 . . . u r ] ∈ C N ×r and let P U UU H ∈ R N ×N be the orthogonal projection onto U . Then, the coherence of U with respect to the standard basis As explained in [4], an intuitive motivation for defining subspace coherence stems from the fact that, in some sense, the singular vectors of the matrix under consideration need to be "sufficiently spread", or more precisely, need to be uncorrelated to the standard basis, in order for the matrix to be fully recoverable using only a small number of its entries.
The following assumptions regarding the subspaces U and V are of particular importance [4].
Indeed, if the constants µ 0 and µ 1 associated with the singular vectors of a matrix M are known, the following theorem holds.

Theorem 1. (Exact MC [4])
Let M ∈ C N 1 ×N 2 be a matrix of rank r obeying A0 and A1 and set N max {N 1 , N 2 }. Suppose we observe m entries of M with locations sampled uniformly at random. Then there exist constants C, c such that if for some β > 2, the minimizer to the program (1) is unique and equal to M with probability at least with the same probability of success.
If a matrix M obeys the assumptions A0 and A1 with parameters µ 0 and µ 1 , we will say that it obeys the incoherence property or, equivalently, that it is incoherent with parameters µ 0 and µ 1 .
In [5], the respective authors introduce a stricter assumption on the singular vectors of a generic matrix M, as a replacement for A0, enabling them to prove tighter -in fact, almost optimal-bounds on the number of observations required in order to achieve exact reconstruction of M by solving (1). Implicitly, they replace subspace coherence with a closely related quantity, which we will refer to as strong subspace coherence, whose definition is presented below.

Definition 2. (Strong Subspace Coherence)
Consider the hypotheses of Definition 1. Then, the strong coherence of U with respect to the standard basis Using the definition stated above, the authors in [5] essentially replace A0 by the following assumption, concerning the singular vectors of M.
If M obeys the assumptions A1 and A2 with a parameter µ ≥ max {µ s 0 , µ 1 }, we will say that it obeys the strong incoherence property or, equivalently, that it is strongly incoherent with parameter µ.
In addition, the following 2-in-1 theorem holds.

Theorem 2. (Exact MC I & II [5])
Let M ∈ C N 1 ×N 2 be a matrix of rank r obeying the strong incoherence property with parameter µ and set N max {N 1 , N 2 }. Suppose we observe m entries of M with locations sampled uniformly at random. Then, there exist positive numerical constants C 1 and C 2 such that if the minimizer to the program (1) is unique and equal to M with probability at least 1 − N −3 .
Further, it is easy to show that, in fact, incoherence implies strong incoherence (stated relatively informaly in [5]), as the following lemma asserts. Lemma 1. If a matrix M ∈ C N 1 ×N 2 of rank r is incoherent with parameters µ 0 and µ 1 , it is also strongly incoherent with parameter µ ≤ µ 0 √ r.
Proof of Lemma 1: See Appendix A.

B. Noisy Matrix Completion: Stability
In the previous subsection, we have focused on cases in which the matrix observations are perfectly noiseless. Of course, in any realistic setting, these observations will be corrupted by noise, yielding the observation model (for the same generic matrix M) where Z ∈ C N 1 ×N 2 constitutes a noise matrix with P (Z) F ≤ δ for some known constant δ > 0. If Z is random, then δ is such that P (Z) F ≤ δ with high probability. Then, instead of (1), the authors in [15] propose solving the program Indeed, under the same hypotheses of Theorem 2, it can be shown that the error norm M − M F is bounded from above as [15] with very high probability, where M denotes the solution to (9). In a nutshell, as the authors in [15] aptly explain, "when perfect noiseless recovery occurs, then matrix completion is stable vis a vis perturbations". Consequently, if M exhibits favorable coherence properties, both noiseless and noisy matrix completion will be more realistic. Therefore, in order to guarantee satisfactory performance for matrix completion, it suffices to study the conditions under which the coherence of M will be as low as possible.

C. Matrix Completion in Colocated MIMO Radar
We consider the respective problem formulation proposed in [10] (see Subsection A of Section II in [10]). Extending the problem to the case of arbitrary 2-dimensional arrays in an obvious way [16], the matrix to be completed at the fusion center of the receiver, P (Y), obeys the special observation model where M r and M t denote the numbers of reception and transmission antennas, respectively, Z is an interference/observation noise matrix as defined above and where X r ∈ C M r ×K (respectively for X t ∈ C M t ×K ) constitutes an alternant matrix defined as with the sets [x r l y r l ] T l∈N M r −1 and {θ k } k∈N K−1 containing the 2-dimensional antenna coordinates of the reception array and the target angles, respectively and λ denoting the carrier wavelength utilized for the communication, and where D ∈ C K×K constitutes a non -zero -diagonal matrix defined as where the sets {ζ k } k∈N K−1 and {ϑ k } k∈N K−1 contain the target reflection coefficients and target speeds, respectively and q and T P R denote the pulse index and the pulse repetition interval, respectively. For the simplest ULA case (as treated in [10]), where d r(t) denotes the respective array antenna spacing, and X r and X t degenerate to Vandermonde matrices.
In the next sections, we focus almost exclusively on bounding the coherence of ∆, first for the ULA case and then for the more general arbitrary 2-dimensional array case. Also, when possible, we derive sufficient conditions under which the coherence the aforementioned matrix is small.

III. COHERENCE AND RECOVERABILITY OF ∆ FOR ULA TRANSMITTER -RECEIVER PAIRS
In this section, we present our coherence and recoverability results for the case in which ULAs are utilized for transmission and reception. In short, we prove: • Asymptotic and approximate optimality of the coherence of ∆ with respect to the number of transmission/reception antennas and • Near optimal recoverability of ∆ via matrix completion.
A. Coherence of ∆ Theorem 3. (Coherence for ULAs) Consider a Uniform Linear Array (ULA) transmitter -receiver pair and assume that the set of target angles {θ k } k∈N K−1 consists of almost surely distinct members. Then, for any fixed M t and M r , as long as the associated matrix ∆ obeys the assumptions A0 and A1 with with probability 1. In the above, for k ∈ {t, r} and (25) Further, if ξ min {ξ r , ξ t } = 0, then, for any fixed K, as long as min i∈{t,r} where (21) and (22) hold replacing both β ξ t (M t ) and β ξ r (M r ) by the constant β ξ (that is, independent of both M t and M r ). Additionally, in the limit we respect to M t and M r , we have that is, the coherence of ∆ is asymptotically optimal. Finally, if ξ is safely bounded away from zero, then, for sufficiently large M t and M r , it is true that that is, the smallest possible coherence for ∆ can be approximately attained even for finite values of M t and M r .
Before we proceed with the proof of the theorem, let us state the following standard result, which will help us develop our arguments easily and concretely.
Then, it is true that Further, equality holds on the left (right) of (31) if and only if equality holds on the left (right) of (32) if and only if the N − 1 largest (smallest) eigenvalues are equal.
Proof of Theorem 3: In order to make it more tractable, we divide the proof into the following two subsections. In the first subsection, we present a suitable characterization of the SVD of ∆ which will come in handy in identifying the essential actions needed to be taken in order to bound its coherence. However, the methodology presented is very general and can be applied to any given rank-L matrix M, as long as it can be explicitly written as the product M = M 1 DM 2 ∈ C M 1 ×M 2 , with D ∈ C L×L being an arbitrary full rank matrix. In the second subsection, we use the results from the first, as well as the special structure of ∆ in order to derive quantitatively useful results regarding its coherence.

1) Characterization of the SVD of ∆:
We would like to study the coherence of the almost surely rank-K matrix where the Vandermonde matrix X r ∈ C M r ×K (respectively for X t ∈ C M t ×K ) is defined by the generating vector with and D ∈ C K×K is an arbitrary non -zero -diagonal matrix. Since ∆ is assumed to be of rank-K almost surely, we implicitly consider the case where the set of angles {θ k } k∈N K−1 consists of almost surely distinct members. In general, the compact SVD of ∆ can be expressed as where U ∈ C M r ×K , V ∈ C M t ×K such that U H U = I K , V H V = I K and Σ ∈ R K×K constitutes a diagonal matrix containing the (non zero) singular values of ∆.
Respectively for X t , consider the thin QR decomposition of X r given by respectively for Q r ) and Λ ∈ R K×K is non -zero -diagonal, containing the singular values of A r DA T t . Thus, we arrive at the expression consequently, by the uniqueness of the singular values of a matrix, Λ ≡ Σ. Therefore, we can set or, equivalently, where (39) stems from the fact that the columns of X r are linearly independent almost surely and, as a result, A r is almost surely invertible. Likewise, regarding the coherence of the row space of ∆, we get 2) Effective Bounding of λ min X H t(r) X t(r) : In the following, we will mainly focus on the matrix X H t X t , since the respective analysis for X H r X r is identical. Due to (41), we need a strictly positive lower bound for λ min X H t X t , with where Let us now apply Theorem 4 to the almost surely positive definite matrix M X H We also need the trace of M 2 . Since M is a Hermitian matrix, it is true that At this point, it is instructive to at least qualitatively study the behavior of the square of φ M (x) (for a general parameter M ∈ N + ) defined above 1 . Fig. 1 shows the square of the function for three different values of M . We can directly identify the following useful fact: then the entire sequence of local maxima of φ 2 M (x) is strictly decreasing. Next, define the function g : and let ξ t min The motivation for defining ξ t stems from the fact that the function φ 2 M (x) is both periodic with unitary period and symmetric and thus it suffices to study its behavior only for x ∈ 0, 1 2 . Then, due to Fact 1, we can upper bound (46) as Consequently, by Theorem 4, and consequently we can bound λ min (M) ≡ λ min X H t X t from below as Respectively, we get Therefore, for fixed M t and M r , as long as and (56) both hold true with probability 1. Consequently, Now, assume that ξ min {ξ r , ξ t } = 0. Then, we can write Since ξ = 0 by assumption and due to Fact 2, the supremum appearing in (59) will be always finite and, consequently the respective bound will be non trivial. Therefore, in this case, for fixed K, (55) becomes min i∈{t,r} Passing to the limit with respect to M t (respectively M r ), we get lim sup and since µ (U ) ≥ 1 by definition [4], it must be true that, in the limit, µ (U ) ≡ 1. Likewise, it will also be true that, in the limit, µ (V ) ≡ 1.
If additionally ξ is safely bounded away from zero, then β ξ will be small (due to Fact 1) and thus for sufficiently large but finite M t and M r , An experimental calculation of the square root of the supremum β ξ for ξ ∈ 10 −3 , 0.5 shown in Fig. 3 (in logarithmic scale) can validate and possibly strengthen our theoretical arguments presented above. We observe that β ξ over ξ constitutes a hyperbolic function, converging rapidly to 1 (linear scale), which corresponds to its minimum value. Finally, regarding the Assumption A1, by a simple argument involving the Cauchy -Schwarz inequality, it can be shown that [4], in the general case, one can choose holding true also with probability 1. The results presented in the statement of Theorem 3 readily follow.
In colocated MIMO Radar systems, due to the need for unambiguous angle estimation (target detection), it is very common to assume that θ i ∈ [−π/2, π/2] , ∀ i ∈ N K−1 . Also, especially for the case where ULAs are employed for transmission and reception, another common assumption is to choose d r ≡ d t = λ/2. Under this setting, the following lemma provides a simple sufficient condition, which guarantees that the asymptotics of Theorem 3 hold true and, as a result, that for a sufficiently large number of transmission/reception antennas, the coherence of ∆ will be small.

Lemma 2. (ULA Pairs Coherence Control) Consider the hypotheses and definitions of Theorem 3. Set d r ≡ d t = λ/2. If additionally
∀ (i, j) ∈ N K−1 × N K−1 with i = j and for some apriori chosen η ∈ 0, π 2 , then and the asymptotics of Theorem 3 always hold true. In particular, the higher the value of η, the higher the value of ξ and the lower the coherence of ∆.
Proof of Lemma 2: See Appendix B.

B. Near Optimal Recoverability of ∆
Using Lemma 1, we can now directly combine Theorem 2 with the coherence results presented in the previous subsection, producing (asymptotic) bounds regarding the number of observations required for the exact reconstruction of the matrix ∆ by solving the convex program (1). Specifically for ULA transmitter/receiver pairs, we present the following interesting result. Since the proof is straightforward, it is omitted.

Theorem 5. (Near Optimal Recoverability for ULA Pairs) Consider the hypotheses of Theorem 3 and assume that
for a fixed number of targets K, ∆ is strongly incoherent with parameter and there exist positive numerical constants C 1 and C 2 such that if the minimizer to the program (1) is unique and equal to ∆ with probability at least 1 − M −3 .
Roughly speaking, Theorem 5 implies that as long as ULAs are concerned, for a sufficiently large number of transmission and reception antennas and for a fixed and relatively small number of targets, matrix completion is exact if the number of observations is at least of an order of M polylog (M ), that is, matrix completion is exact for a slightly larger number of observations than the information theoretic limit (see [5] for details).

IV. COHERENCE OF ∆ FOR ARBITRARY 2D ARRAYS
It is possible to generalize Theorem 3 for a far more general case, that is, when the transmitter and the receiver employ arbitrary 2-dimensional arrays. However, in this case, since our knowledge about the specific characteristics of the topologies of the arrays involved is very restricted, our bounds, although tight, are not expected to be as easily handleable as in the ULA case (see Theorem 3 and Lemma 2). Next, we state and prove the following theorem in this respect.

Theorem 6. (Coherence for Arbitrary 2D Arrays)
Consider an arbitrary array transmitter -receiver pair equipped with M t and M r antennas, respectively. Assume that the set of target angles {θ k } k∈N K−1 consists of almost surely distinct members and that where A constitutes a nominal point set for all admissible angle pair combinations. Also, let the abstract sets T and R contain all the essential information regarding the transmitter and receiver topologies, also assumed fixed and known apriori. Then, for any M t and M r , as long as the associated matrix ∆ obeys the assumptions A0 and A1 with with probability 1 and where with ϕ t(r) : A → C given by where Proof of Theorem 6: Again, we divide the proof into the following subsections, in similar fashion as in the proof of Theorem 3.
1) Characterization of the SVD of ∆: We now consider the almost surely rank-K matrix exactly as defined in Subsection C of Section II. Of course, since ∆ is assumed to be of rank-K almost surely, the members of the set of angles {θ k } k∈N K−1 are implicitly assumed to be almost surely distinct. By almost identical reasoning as in the proof of Theorem 3, the coherences of the column and row spaces of ∆, U and V , can be upper bounded using (41) and (42), respectively.
2) Bounding λ min X H t(r) X t(r) : We directly focus on the matrix X H t X t ∈ C K×K defined as in (43), where this time, Applying Theorem 3 to M X H t X t ∈ C K×K , we get τ ≡ M t and, concerning the trace of M 2 , it is true that Let all the assumptions of the statement of Theorem 6 hold true. Then, we can define a bivariate function ϕ t : A → C given by 2 whose norm can be bounded as Observe that in the expressions above, the supremum is taken conditional on the set T and, as a result, it is highly dependent on the array topology of the transmitter and therefore also on M t , but of course independent of any combination of the angles. Then, we can bound tr M 2 as and the results follow using similar procedure to the respective part of the proof of Theorem 3. Remark 1. Indeed, one may claim that Theorem 6 is mostly of theoretical value and that its practical applicability is limited. On the one hand, this is true, since, except for the ULA case, for which explicit results are available (see Theorem 3  bounding norms of sums of complex exponentials, whose exponents are arbitrary real variable functions constitutes a difficult mathematical problem. However, from an engineering point of view, for a given pair of transmitter -receiver topologies, we can always compute the aforementioned supremum empirically, as it becomes clear by the following example. suggests that in order to bound the coherence of the respective matrix ∆, a uniformly sampled version of which is available at the receiver's fusion center, we have to specify the supremum given by (75), which, of course, cannot be computed analytically. Fig. 4(a) shows the function ϕ t(r) (x, y |T (R) ) 2 with respect to (x, y) ∈ [−π, π] 2 . We observe that this function is periodic in the 2-dimensional plane, with period equal to 2π in each dimension.
Let us now assume that for some η ∈ (0, π), that is, every pair of distinct angles θ i and θ j are such that the magnitudes of their differences are lying in two non intersecting halfplanes, one above and one below the hyperplane y = x, within a margin of η. Empirically, using the graph of ϕ t(r) (x, y |T (R) ) 2 , we can easily specify its supremum over the set A, which is required in order to bound the coherence of ∆. Additionally, it is obvious that if η is sufficiently large, the coherence of ∆ will be essentially relatively small. Interestingly, this fact draws immediate connections regarding the coherence between the UCA and the ULA case (see Theorem 3 and Lemma 2). The function ϕ t(r) (x, y |T (R) ) 2 resulting from the application of Theorem 6 for the ULA case is shown in Fig. 4(b). We observe that the sufficient condition for low coherence of ∆ presented in Lemma 2 can be immediately validated.
Comparing the two graphs shown in Fig. 4, we can infer that in the UCA case the allowable region for the magnitudes of the differences of the angle pairs, given by the set A, is larger than the respective region for the ULA case (Lemma 2). On the other hand, the values of ϕ t(r) (x, y |T (R) ) 2 for the ULA case in the interior of the allowable region are considerably smaller than the values of the respective function in the interior of the respective set for the UCA case. Consequently, regarding our choice of transmission/reception arrays, there is an obvious trade -off between "resolution" and coherence.
Remark 2. There are other fancier types of 2-dimensional arrays that can achieve a much better "resolution/coherence ratio". For instance, we have found experimentally that carefully designed spiral arrays, whose antenna positions constitute a sampling of the usual Archimedean Spiral, possess the advantages of both the aforementioned cases and, additionally, they exhibit very good asymptotic properties, guaranteeing low coherence for a sufficiently large number of antennas.
Until now, in all the results we have presented, we have assumed that the target angles θ k , k ∈ N K−1 are almost surely distinct. Apparently, this required property of distinctness is far weaker than (statistical) independence. In fact, our results presented in detail in the previous sections continue to hold without any modification for any set of dependent target angles, as long as they are all different from each other with probability 1 (recall the Vandermonde/alternant structure of the matrices X r and X t in the proofs of Theorems 3 and 6). Therefore, regarding the coherence of ∆ for arbitrary 2-dimensional arrays (and thus also for ULAs), the only case that needs special treatment is when θ i ≡ θ j for some (i, j) ∈ N K−1 × N K−1 with i = j, for which we present and prove the following result.

Theorem 7. (Coherence for Non -Distinct Angles)
Consider an arbitrary 2-dimensional array transmitter -receiver pair equipped with M t and M r antennas, respectively. Assume that the set of angles Θ {θ k } k∈N K−1 is such that it can be partitioned as where D ⊆ Θ contains almost surely distinct members and Let ∆ and ∆ D be the matrices associated with the angle sets Θ and D, respectively. Then, it is true that Proof of Theorem 7: Consider the matrix where X r ∈ C M r ×K , X t ∈ C M t ×K and D ∈ C K×K are defined as in the proof of either Theorem 3 or Theorem 6. Let the assumptions of the statement of Theorem 7 hold true. Then, only |D| L columns of both X r and X t will be almost surely linearly independent, whereas the rest |R| ≡ K − L columns of both matrices constitute repetitions of the aforementioned L ones. As a result, ∆ will be almost surely of rank L.
Let us re-express ∆ as where P ∈ R K×K constitutes an appropriately chosen permutation matrix such that where X D r ∈ C M r ×L (respectively for X D t ∈ C M t ×L ) contains the columns of X r associated with the almost surely distinct angles in D and X R r ∈ C M r ×K−L (respectively for X R t ∈ C M t ×K−L ) contains the rest of columns of X r , associated with the rest of the angles in R. Of course, D ∈ C K×K constitutes a non -zero -diagonal matrix.
Respectively for X t , the thin QR decomposition of X r can be expressed as A r ∈ C K×K is a specially structured singular upper triangular matrix (see expressions above) of rank L and A D r ∈ C L×K constitutes a rectangular matrix also of rank L.
Let V D Then, based on (93) and using an almost identical procedure as in the first part of the proof of Theorem 3, we can directly show that the coherence of the column space of ∆, U , is given by Respectively, the coherence of the row space of of ∆, V , is given by Now, consider the almost surely rank-L matrix where the diagonal matrix D D ∈ C L×L is defined in an obvious way (see (90) -(92)). Then, by construction of the QR decomposition, it must be true that where, A D t ∈ C L×L and A D r ∈ C L×L constitute almost surely full rank matrices. Recall (38) and adapt it appropriately for expressing the coherences of the column and row spaces of ∆ D , U D and V D , respectively. Our claims follow. Remark 3. Indeed, in many applications (Radar and non -Radar), it is very likely that the situations Theorem 7 is dealing with may correspond to events of zero measure. However, we feel that stating this result is important, in order for the coherence analysis we presented in the previous chapters to be entirely complete. Also, interestingly, the simple implication of Theorem 7 is somewhat not intuitive: As the difference between two angles is decreasing, the coherence of ∆ becomes worse (that is, increases), but if the difference is exactly zero, then the coherence of ∆ is identical to the coherence of the variation of ∆ resulting from simply removing the information corresponding to any of the two identical angles. Clearly, this result does not in any way contradict the ones presented in the previous sections.

VI. DISCUSSION AND SOME SIMULATIONS
In this section, we present some simulations, validating our main results presented above and discuss some further implications of our respective theoretical analysis.
For simplicity, we consider a MIMO radar system equipped with identical ULAs for transmission and reception, with d r ≡ d t = λ/2 and M r ≡ M t M . We also consider K = 4 targets in the far field, with angles independently distributed in − π 2 , π 2 . In this synthetic example, in order to demonstrate the validity of Theorem 3, we assume that the target angles are known apriori. By Lemma 2, we know that the condition ξ = 0 will always hold and consequently the asymptotics of Theorem 3 must also hold true. Of course, ξ can be computed either using (24) or (66) (for some sufficiently chosen value of η), with the latter producing a worst -case bound regarding the coherence of the associated matrix ∆. Also, in this example, we obviously have µ (U ) ≡ µ (V ).
Using (24) for the computation of ξ, Fig. 5 shows the behavior of both the coherence of ∆ and its bound µ 0 , which results by directly applying Theorem 3, as a function of the number of transmission/reception antennas M . We observe that, clearly, the proposed bound is tight and it tracks the convergence of the coherence of ∆ to unity very accurately. We should mention here that for very small angle differences, the bound becomes somewhat looser. However, our numerical simulations have shown that our bound constitutes a very reasonable coherence estimate in all cases.  Apparently, in any realistic situation, the actual values of the target angles are unknown. Assuming generically that each of the angle differences belongs to a set given by (65) for some η ∈ 0, π 2 -η depends on the specific radar application-, we can invoke Lemma 2 in order to bound the coherence of ∆ in this more general case. Fig. 6 depicts a number of bounds produced by Lemma 2 for various values of η, as functions of the number of antennas M . One can observe that, as the value of η increases, the respective coherence bound converges much faster to unity, therefore increasing our confidence that the performance of matrix completion will be satisfactory for a relatively smaller number of transmission/reception antennas.
However, we should stress that Lemma 2 essentially produces worst case bounds, which might be too pessimistic for specific applications. If this is the case, one could use Theorem 6, which provides greater versatility for deriving more accurate bounds for more specific target configurations and for given number of antennas or, alternatively, one could derive variants of Lemma 2 for special target configurations.
Another important ULA configuration in MIMO radar systems results by choosing d t = M r λ/2 and d r = λ/2. It is well known that this particular choice for the transmitter antenna spacing increases the degrees of freedom of the system to M t M r using only M t + M r physical antenna elements and consequently, higher spatial resolution can be obtained (see, for instance, [18]). If we are interested in the performance of matrix completion, as far as µ (V ) is concerned, associated solely with the reception array, we can directly use Theorem 3 in conjunction with Lemma 2 as explained above in order to derive the respective coherence bound. However, the behavior of µ (U ) is much more complicated and the application of Theorem 3 leads to an unreasonably involved analysis. But one could invoke Theorem 6 in this case. Fig. 7(a) shows the function |ϕ t (x, y |T )| with respect to (x, y) ∈ [−π, π] 2 . Assuming that the angles are independently and uniformly distributed in − π 2 , π 2 and that the contours of |ϕ t (x, y |T )| 2 are sufficiently dense (for M r properly chosen), then the respective values of the aforementioned function will be essentially small, since, technically speaking, the probability of any θ i , θ j belonging to the union of the strict subsets of − π 2 , π 2 2 corresponding to the contours of |ϕ t (x, y |T )| 2 shown in Fig. 7(a) will be essentially zero. Therefore, a low value for µ (U ) is guaranteed with very high probability.

VII. CONCLUSION
In this paper, we have presented a detailed analysis regarding the recoverability of the data matrix in colocated MIMO radar systems via convex optimization (matrix completion), for a number of commonly used array configurations. We showed that, in most cases, the data matrix is indeed recoverable from a minimal number of observations, as long as the number of transmission and reception antennas is sufficiently large and under common assumptions on the DOAs of the targets. Consequently, the matrix completion approach for reducing the sampling requirements in colocated MIMO radar is indeed theoretically robust and also appealing for practical consideration in real world applications. However, although we have explicitly shown that the choice of ULAs for transmission and reception leads to asymptotically and approximately optimal coherence of the data matrix, the important and more general problem of optimally choosing the array topologies for minimizing matrix coherence still remains open, clearly suggesting new directions for further research.

APPENDIX A PROOF OF LEMMA 1
Let the hypothesis of the statement of Lemma 1 hold true. In the following, we consider only the column space of M, U , since, for V the procedure is identical. First, consider the set G (i, j) ∈ N + N × N + N |i ≡ j . Then, In all cases, it is true that µ s (U ) ≤ µ 0 and µ s (V ) ≤ µ 0 .
In the following, our goal will be to explicitly specify the infimum and the supremum appearing in (103), or equivalently the set F .


extfieldsofstudy:
Computer Science
Mathematics
Physics

text:
Variational Pseudolikelihood for Regularized Ising Inference

I propose a variational approach to maximum pseudolikelihood inference of the Ising model. The variational algorithm is more computationally efficient, and does a better job predicting out-of-sample correlations than $L_2$ regularized maximum pseudolikelihood inference as well as mean field and isolated spin pair approximations with pseudocount regularization. The key to the approach is a variational energy that regularizes the inference problem by shrinking the couplings towards zero, while still allowing some large couplings to explain strong correlations. The utility of the variational pseudolikelihood approach is illustrated by training an Ising model to represent the letters A-J using samples of letters from different computer fonts.

Statistical mechanical models constructed from experimental observations provide a valuable tool for studying complex systems. The utility of the statistical mechanics approach to data-driven modeling is especially apparent in biology, providing insights into the behavior of flocking birds [1], the organization of neural networks in the brain [2][3][4], the structure and evolution of proteins [5][6][7][8][9], and many other topics [10,11]. Generally, the 'inverse' statistical mechanics approach refers to the construction of statistical models using the principle of maximum entropy [12,13]. In this approach, one constructs the probability distribution with the maximum entropy subject to constraints on its moments, which are derived from observations. Although maximum entropy modeling has been applied successfully to many different problems, it is still not clear how to estimate the parameters of the resulting probability distribution in an optimal way.
In this work, I consider the problem of estimating the parameters of an Ising model (see [14] for a review). The Ising model describes the statistics of a vector σ of N spin variables σ i ∈ {−1, +1}, and can be derived from the principle of maximum entropy with constraints on the moments σ i and σ i σ j . The probability distribution for σ is given by P ( σ) = Z −1 exp(−U ( σ)) where the energy is U ( σ) = − i h i σ i − i<j J ij σ i σ j and Z is a normalization constant. Here, h i is a local field that biases σ i towards the +1 or −1 configuration, and J ij is a coupling that describes the strength of the interaction between spins i and j. The goal of the inverse Ising problem is to infer the parameters, i.e. h i and J ij , from a set of n observed configurations σ (l) for l = 1 . . . n.
The Ising model presents two obstacles that make the inverse problem quite difficult. First, computing the partition function (or its derivatives) is computationally intractable for large spin systems. As a result, the inverse Ising problem has to be solved approximately. A number of approximate methods for inferring the parameters of the Ising model have been introduced including naive mean field theory [15], the Thouless-Anderson-Palmer (TAP) approximation [16], the isolated spin pair approximation [14], the Sessak-Monasson expansion [17], and others [5,[18][19][20][21][22][23][24][25][26][27]. The second obstacle -overfitting -is more fundamental and generally affects all high dimensional problems in statistical inference.
Overfitting is a simple concept to illustrate for the Ising model. All of the moments, i.e. σ i and σ i σ j , are noisy because they are computed from a finite sample of n observed configurations. Thus, fitting all of the moments exactly necessarily incorporates noise from the finite sample size. As a consequence, parameters obtained by fitting the moments of one dataset may not provide a good description of a new dataset derived from the same system. In general, overfitting becomes a serious problem when the number of parameters (i.e. N 2 ) exceeds the number of independent observations (i.e. n).
A common approach to mitigating the effects of overfitting is to penalize parameters with large values [28]. For example, the Ising model can be 'regularized' by adding an L 2 penalty λ i<j J 2 ij (as in [28]) or an L 1 penalty λ i<j |J ij | (as in [18,21]) to the objective function that describes the fit to the data. Alternatively, the empirical moments can be modified using a 'pseudocount' according to the rules σ i → (1 − α) σ i and σ i σ j → δ ij + (1 − δ ij )(1 − α) σ i σ j [28]. The intuition for why regularization works comes from the law of total variance, which implies that the error in a statistical estimator is error 2 = variance + bias 2 . Thus, a regularization method that decreases the variance in an estimator more than it increases the squared bias will have a smaller error and, therefore, better out-of-sample predictive ability.
The free parameter (λ ≥ 0 or 0 ≤ α ≤ 1) that penalizes large couplings must be carefully chosen to ensure that the regularization method actually improves out-of-sample performance. Typically, the choice of the regularization parameter and subsequent testing of predictive ability are performed using cross-validation. To perform cross-validation, the observed data are randomly partitioned into three mutually exclusive datasets. The first dataset, usually called the 'training' sample, is used for fitting the model. Here, the training sample will be denoted 'F' for 'fitting'. The resulting parameters are used to predict the data contained in the second dataset, called the 'validation' sample ('V'). The optimal value FIG. 1.
for the regularization parameter is chosen to maximize the predictive performance of the model on the validation sample. Finally, the out-of-sample performance of the resulting model is tested by measuring the agreement between the predictions of the model and the data contained in the third dataset, called the 'test' sample ('T').
Focusing on out-of-sample predictive ability provides a different metric than most previous papers on the inverse Ising model, which have studied the ability to reconstruct a coupling matrix from sampled configurations (e.g. [14]). In general, the performance of various algorithms for the inverse Ising model have been studied by defining a set of couplings, simulating configurations from the resulting Ising model, and then asking how well the couplings inferred by various methods reproduce the true J ij 's. By contrast, this work will compare the performance of different approaches to the inverse Ising model by their outof-sample predictive performance using a dataset of images developed for testing machine learning algorithms.
In order to compare the predictive performance of various inference methods for the Ising model, it is necessary to have a metric that quantifies the agreement between the model and the data in the test sample that can be easily computed. Here, I will use the negative log-pseudolikelihood, L data p (h, J) = − log i P (σ i |σ j =i ) data , where the angular brackets denote an average over the spin configurations in dataset 'F', 'V', or 'T'. Recently, Aurell and Ekeberg [18] demonstrated that the couplings of the Ising model can be inferred by minimizing the negative log-pseudolikelihood, which is given by (ignoring constant terms): is the effective field acting on spin i due to the configurations of the other n − 1 spins. The derivatives of L p (h, J) are easy to calculate: Note that these expressions assume J ii = 0 and J ij = J ji . Thus, the Ising model can be fit to the training sample by minimizing L F p (h, J) using gradient descent. While the computing the pseudolikelihood is certainly tractable it is, neverthless, computationally challenging to compute the averages over the training sample at every step of gradient descent if the sample size is large. Therefore, I propose a variational approach to maximum pseudolikelihood inference of the Ising model that is more computationally efficient and, as I will show, performs better out of sample. The variational pseudolikelihood approach minimizes an energy that provides an upper bound on L F p (h, J), given by: The upper bound follows from log(cosh(φ i )) ≤ log(cosh(µ i )) + log(cosh(ν i )) if φ i is Gaussian distributed with mean µ i and standard deviation ν i ; this inequality is illustrated in Fig. 1. Since φ i is a sum of many random variables, I will assume that it is approximately Gaussian distributed with mean After plugging in the estimate for h i , it is only necessary to minimize a function of J given by: The derivatives are given by: where D ij = tanh(ν i )δ ij /ν i and the diagonal elements of J are constrained to J ii = 0. The couplings can be estimated by minimizing Eq. 3 using the gradient descent update J ij (t + 1) = J ij (t) − (G ij (t) + ρG ij (t − 1)), where is a small step size and ρ is a 'momentum'. The variational pseudolikelihood approach was compared to ( [14]): direct pseudolikelihood maximization (with and without an L 2 penalty on the couplings), naive mean field (NMF) inversion (with and without pseudocount regularization), and the isolated spin pair (ISP) approximation (with and without pseudocount regularization). For the regularized methods, the penalty parameters were chosen by cross-validation to minimize L V p (h, J) on the validation sample. The performances of these methods was assessed using training, validation, and test samples con structured from the 'notMNIST' dataset, which consists of 28 × 28 pixel images of the letters A-J compiled from a large number of different fonts (see Appendix). The 'notMNIST' dataset contains roughly 50000 images for each letter, and the samples of each letter are very diverse. Examples of binarized images for letters A-J are shown in Fig. 2. Mutually exclusive training, validation, and test samples were constructed, each containing 500 randomly chosen images for each letter. Table I shows a comparision of these methods according to L F p (h, J) for the training set images, and L T p (h, J) for the test set images. As one would expect, ranking by the pseudolikelihood ensures that direct pseudolikelihood maximization is the best performing method on the training data. However, the variational pseudolikelihood approach presented here outperforms all other methods, including direct pseudolikelihood maximization, when compared by out-of-sample performance on the test set. In addition, a simple implementation of variational pseudolikelihood inference was approximately an order of magnitude faster than direct pseudolikelihood maximization running on a desktop computer, even ignoring the time spent choosing the penalty parameter for L 2 regularized pseudolikelihood.
Comparing the out-of-sample results for the unregularized and regularized versions of maximum pseudolikelihood, NMF, and ISP estimates in Table I demonstrates the importance of regularization for the inverse Ising model. Histograms of the couplings inferred with direct pseudolikelihood maximization, pseudlikelihood maximization with an L 2 penalty, and the variational pseudolikelihood method (Fig. 2) illustrate that the methods which performed better out-of-sample had smaller estimates for the couplings. However, adding the L 2 penalty to the pseudolikelihood resulted in an inferred Ising model with many weak couplings, and no strong couplings. The variational approach, by contrast, produced both strong and weak couplings, which resulted in improved out-of-sample prediction performance relative to other methods. The analysis presented above demonstrates that variational pseudolikelihood inference can be used to train an Ising model so that it makes good out-of-sample predictions. Here, I provide an example to illustrate how the variational pseudolikelihood method can be used in practice. I examined a simple question: what features does the Ising model learn when trained on images of the letters A-J? Using the variational pseudolikelihood approach, it is simple to infer coupling matrices with a specific structure, such as that of a Hopfield neural network [5,21,26,29]. The couplings in a Hopfield network are described by a Hebbian rule such that where ξ (s) for s = 1 . . . p are 'patterns' stored in the memory. These patterns describe features in the correlation structure of the data. The derivatives of the variational energy with respect to the patterns can be computed using the chain rule: Thus, the patterns can be inferred quite easily by minimizing the variational energy using gradient descent. Note, however, that the patterns are unconstrained with respect to orthogonal transformations [30], and the symmetry is broken by the initial conditions of the optimization.
The letters in the notMNIST dataset are quiet diverse, and hundreds of patterns are required to approach the performance of the unconstrained variational pseudolikelihood method (Fig. 4a). Nevertheless, the p = 10 Hopfield model provides a useful visual example. Starting from randomly initialized patterns (shown in the top row of Fig. 4b), the patterns converge after less than 1000 steps of gradient descent to images with recognizable features of letters (shown in the second row of Fig. 4b).
The notMNIST images present a challenging dataset for the Ising model. State-of-the-art machine learning methods for modeling similar types of images include a variety of pre-processing and fine tuning steps [31], and the best performing algorithms are based on deep neural networks that are believed to excel at capturing higher order correlation structure in the data that cannot be described by the Ising model [32]. Nevertheless, Fig.  4 clearly demonstrates an Ising model based on a few Hopfield patterns is able to capture recognizable features from the data.
In summary, I presented a variational approach to maximum pseudolikelihood inference of the Ising model. The variational pseudolikelihood method outperformed all other tested methods at describing the out-of-sample correlation structure in a dataset consisting of images of the letters A-J from various computer fonts. This method has many characteristics that make it attractive in practice: it is fast, accurate, can be used with large spin systems, and can easily be adapted to learn coupling matrices with specific structures such as Hopfield models. Moreover, it should be easy to extend the approach presented here to construct variational pseudolikelihood algorithms for inferring Potts models [6], Restricted Boltzmann Machines [33], and other inverse models for spin systems.
I would like to thank Alex H. Lang, Thomas C. Lang, Pankaj Mehta, Ilya Nemenman, and Javad Noorbakhsh for helpful discussions. Funding for this research was provided by a Simons Investigator Award to Pankaj Mehta.
Appendix: The 'notMNIST' dataset consists of 28×28 pixel images of the letters A-J compiled from a large number of different fonts. The images are available at http://yaroslavvb.blogspot.com/2011/09/notmnistdataset.html. Each image in the original dataset is grayscale, with pixels taking on values between 0 and 255. The images were binarized in the simplest way by defining pixels with intensity less than or equal to 127 as spin −1, and those with intensity greater than 127 as spin +1. Finally, each image was flattened into a vector of N = 784 spins. * charleskennethfisher@gmail.com