Edith Elkind

Blaise Genest

Doron Peled

Paola Spoletini

Quantifying the Discord: Order Discrepancies in Message Sequence Charts

Message Sequence Charts (MSCs) and High-level Message Sequence Charts (HMSCs) are formalisms used to describe scenarios of message passing protocols. We propose using Allen's logic to represent the temporal order of the messages. We introduce the concept of discord to quantify the discrepancies between the intuition and the semantics of the ordering between messages in different nodes of an HMSC. We study its algorithmic properties: we show that while the discord of a pair of messages is hard to compute in general, the problem becomes polynomial-time computable if the number of nodes of the HMSC or the number of processes is constant. Moreover, for a given HMSC, it is always computationally easy to identify a pair of messages that exhibits the worst-case discord and compute the discord of this pair.

, where ' is the transitive closure of the edge set ' .

According to this definition, one can compute § © ¨£! ¦ by computing the dis- cords for all pairs of messages in !. However, in general, computing

is coNP-hard, so this method is not efficient. Quite surprisingly, it turns out that there exists a different approach that allows us to compute § © ¨£! ¦ in polynomial time.

It is based on the fact that while it may be hard to check whether there exists a chain between two events, it is easy to prove that there is no chain between two extremal events, for a suitable definition of extremality.

Introduction

Message Sequence Charts (MSCs) and High-level Message Sequence Charts (HMSCs) are very useful tools for describing executions of communication protocols. They provide an intuitive visual notation, which is widely used in practice and has been formally described in the MSC standard [START_REF]ITU Z120[END_REF]. Moreover, a related notation was adopted as a part of the UML standard. Informally, an MSC is described by a set of processes and a set of messages between these processes. The notation allows one to specify the (partial) order in which each process sends and receives messages. Furthermore, MSCs can be generalized to HMSCs, which are graphs whose nodes are labeled with MSCs. An execution of an HMSC is a concatenation of MSCs that appear on a path in this graph.

Using HMSC notation, one can describe alternative behaviors of systems, or even use it as a scenario-based programming formalism [START_REF] Harel | Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine[END_REF]. The reader is referred to Section 2 for formal definitions.

Besides being used in practice, MSCs and HMSCs have been extensively studied from theoretical perspective over the past few years. This research has pointed out several difficulties with these formalisms. One such example is the problem of detecting race conditions in MSCs [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF], i.e., the possibility that messages arrive out of order due to lack of synchronization. This problem has also been studied in the more general context of HMSCs [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF] and sets of MSCs [START_REF] Elkind | Detecting Races in Ensembles of Message Sequence Charts[END_REF]. Another problem is related to global choice [START_REF] Ben-Abdallah | Syntactic Detection of Process Divergence and Non-local Choice in Message Sequence Charts[END_REF][START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF], where some processes behave according to one MSC scenario and other processes behave according to another MSC scenario, resulting in new behaviors.

Continuing this line of research, in this paper we identify another ambiguity of the MSC notation. Namely, in the definition of an HMSC, a concatenation of MSCs along a path intuitively suggests that messages that appear in an earlier MSC precede in time any message that appears in a later MSC. In fact, in some frameworks such as live sequence charts [START_REF] Damm | LSCs: Breathing Life into Message Sequence Charts[END_REF] there is a hidden assumption of such synchronization (its implementation would probably require additional mechanism or extra messages). However, according to the MSC semantics, this is is not the case: concatenation of events according to a path in the HMSC graph is done process by process. Thus, independence among events happening in different sets of processes may allow messages in later MSCs to (partially) overlap or sometimes even precede messages in previous MSCs. Clearly, this discrepancy between intuition and semantics may result in users misinterpreting the notation and, as a result, designing protocols that do not work as intended. Protocol design could be helped if the user can check his intuition on MSC executions exhibiting such discrepencies. Algorithms are thus needed to find (worst-case) discrepencies. This is reminiscent of the concept of race conditions: the straightforward visual interpretation of concatenation is different from the intended semantics. However, unlike race conditions, the aforementioned discrepancy has not been studied before.

In this paper, we provide a formal treatment of this issue. We introduce the notion of discord of a pair of messages in different nodes of an HMSC. Intuitively, the discord of two messages is the worst possible discrepancy between their order in an execution and their "ideal" order, in which the message in the MSC that appears earlier on the path precedes the message in the MSC later on the path. To formalize this intuition, we need several tools that we introduce below.

We start our study of the message order in MSCs and HMSCs by defining the concept of a chain. Informally, a chain is a sequence of events where any adjacent pair of events is ordered either by being a send-receive pair or by belonging to the same process line. Hence, a chain represents a possible flow of information. Clearly, the order between messages is determined not only by the relevant messages themselves, but also by chains between their endpoints. We characterize the possible message orders by describing the possible communication patterns between their endpoints. We then project each such pattern onto the global timeline, thereby obtaining an interval, and classify the resulting scenarios.

To compare message intervals, we employ a subset of Allen's interval logic [1]. Allen's logic is a formalism for describing the relative order of time intervals. For example, Allen's logic formula ¡¢ expresses the fact that happens during ¢ , i.e., starts after ¢ starts and ends before ¢ ends. Allen's logic has been widely studied in the context of artificial intelligence and knowledge representation, and its expressive power and computational properties are well understood [START_REF] Krokhin | Reasoning about Temporal Relations: The Tractable Subalgebras of Allen's Interval Algebra[END_REF]. Since messages can be seen as time intervals, it provides a convenient language for describing the message order. Indeed, for any pair of messages £ ¤ ¥ ¤ ¡¦ in an HMSC, we can identify the sub- set of primitive predicates £ ¤ ¥ ¤ ¡¦ of Allen's logic (such as "during", "precedes" or "overlaps") such that for any predicate ¡ ¢ £ ¤ ¥ ¤ ¡¦ the relationship ¤ ¡ ¤ ¡ is consistent with the HMSC semantics. There is also another primitive predicate that can be associated with messages occuring in different nodes of the HMSC, namely, the one that is suggested by the HMSC structure. More specifically, if ¤ and ¤ ¡ appear in two HMSC nodes that are connected by a path, the HMSC structure suggests that one of them precedes the other (even though this is not necessarily implied by the HMSC semantics).

In this paper, we introduce a natural ordering on Allen's logic primitive predicates.

We then define the discord of a pair of messages £ ¤ ¥ ¤ ¡¦ in an HMSC as the elemen- t of the set £ ¤ ¥ ¤ ¡¦ that is the furthest away (according to our ordering) from the primitive predicate suggested by the HMSC structure. For example, if ¤ appears in some HMSC node, while ¤ ¡ appears in a successor node (and thus the HMSC suggests that ¤ precedes ¤ ¡ , written as ¤ £ ¤ ¡ ), the discord between ¤ and ¤ ¡ tells us whether all or part of ¤ ¡ may appear before ¤ . In the extreme case, when there are no other events in the system and ¤ and ¤ ¡ belong to different processes, it may happen that ¤ ¡ appears entirely before ¤ . In this case, the discord between the two messages is described by the Allen's logic's primitive predicate £¤ ("is preceded by"). To sum- marize, the discord measures how much the actual order of appearance of messages can deviate from the order within the HMSC graph.

We study the concept of discord from the algorithmic perspective. First, we show that computing the discord of a pair of messages is coNP-complete. Our reduction assumes that both the number of nodes in the HMSC and the number of processes are part of the input. We show that this is inevitable: if either of these numbers is fixed, the discord can be computed in polynomial time. We then focus on characterizing the global properties of discord in an HMSC. To this end, we define the discord of an HMSC as the worst possible discord of a pair of messages in this HMSC. Surprisingly, it turns out that this quantity can be computed in time polynomial both in the size of the HM-SC graph and the number of processes. Intuitively, the reason for that is that it is easy to identify a pair of messages that exhibits the worst-case behavior for a given HMSC and compute the discord of such a pair. Our work also provides a general study of the existence of communication chains, which we believe will be useful in its own right in studies of layered combination of communication algorithms.

A preliminary version of this paper (with Section 5.2 omitted and Section 5.1 shortened) appeared in ATVA'07 [START_REF] Elkind | Quantifying the Discord: Order Discrepancies in Message Sequence Charts[END_REF].

Preliminaries

Message Sequence Charts

Following [START_REF]ITU Z120[END_REF], we formally define message sequence charts (MSCs), MSC concatenation, and high-level message sequence charts (HMSCs).

Definition 1. A Message Sequence Chart (MSC) is a tuple ¥ ¦ £ § ¥¨¥©¥¥ ¦ , where - §
is a finite set of processes; -¨is a finite set of events; -© ¨¡ ¢ § is a function that maps every event to the process on which it occurs; -is a finite set of messages. Each message ¤ ¢ consists of a pair of events £ £ ¥¤¦ for send and receive;

-For each process ¥ ¢ § , is a total order on the events of that process.

We define a relation as ¦ ¦ §¨£ £ ¥¤¦ © £ £ ¥¤¦ ¢ and let be the transitive closure of . We require to be acyclic. We assume that MSCs are FIFO, that is, if two messages £ £ ¥¤ ¦ and £ £ ¡ ¥¤¡¦ are between the same processes, i.e., © £ £ ¦ ¦ © £ £ ¡¦ and © £ ¤ ¦ ¦ © £ ¤¡ ¦ , then £ £ ¡ implies ¤ ¤¡ .

We will occasionally abuse notation and write

¤ ¢ ¥ instead of ¤ ¢ . Definition 2. Let ¥ ¥ ¥ ¡ be two MSCs where ¥ ¦ £ § ¥¨ ¥© ¥ ¥ ¦ , ¥ ¡ ¦ £ § ¡ ¥¨¡¥© ¡ ¥ ¡ ¥ ¡ ¦ with § ¦ § ¡ ¦ §
and ¨ ¨¡ ¦ . Define their

concatenation as an MSC £¥ ¥ ¡¦ ¦ £ § ¥¨¥©¥¥ ¦ , where ¨¦ ¨ § ¨¡, ¦ § ¡ , the function © is given by © £ ¦ ¦ © £ ¦ if ¢ ¨ and © £ ¦ ¦ © ¡ £ ¦ if ¢ ¨¡, and for each ¥ ¢ § we define ¦ § ¡ §¨£ ¥ ¡¦ © ¢ ¨ ¥ ¡ ¢ ¨¡¥© £ ¦ ¦ © ¡ £ ¡¦ .
Notice that there are no messages that are sent in one MSC and received in the other (an extention of the HMSC notation in [START_REF] Gunter | Compositional message sequence charts[END_REF] allows a message to span several MSC nodes). Definition 2 can be naturally extended to sequences ¥ ¥ ¥ ¡ ¥ ¥ ¥ of three or more MSCs by setting £¥ ¥

¡ ¥ ¦ = ££ £¥ ¥ ¡¦ ¥ ¢¦ ¦ . Definition 3. A High-level Message Sequence Chart (HMSC) is a tuple ! ¦ £ " ¥#¥ $ % ¥&¦ , where " ¦ £ $ ¥'¦ is a directed graph with the vertex set $ ¦ ¨( ¥ ¥ (
and the edge set ' ) $ 0 $ , # ¦ ¨¥ ¥ ¥ ¥ is a collection of MSCs with a common set of processes and mutually disjoint sets of events, $ % ) $ is a set of initial nodes, and & $ ¡ ¢ # is a bijective mapping between the nodes of the graph and the MSCs in # . To simplify notation, we assume & £ (1 ¦ ¦ ¥ 1 . Each vertex of " is reachable from one of the initial nodes. An execution of the HMSC is a finite MSC £¥ 1 ¥ 2 ¦ obtained by concatenating the MSCs in the nodes of a path (1 ¥ ¥ ( 2 of the HMSC that starts with some initial node (1 ¢ $ % . The size © ! © of an HMSC ! is defined as © ! © ¦ ©¨ © 3 4 4 4 3 ©¨ © 3 © $ © 3 ©' © , where ¨1 is the set of events of the MSC ¥ 1 .

Given a path 5 ¦ £ (1 ¥ ¥ ( 2 ¦ in " of length at least 6, we denote by & £5 ¦ the MSC that is obtained by concatenating the MSCs along 5, i.e., £¥ 1 ¥ 2 ¦ . The set of executions of an HMSC is also referred to as the set of MSCs generated by that HMSC.

We can define infinite executions in a similar way. This requires defining the concatenation of an infinite sequence of MSCs, which is the limit of the sequence of finite concatenations of prefixes. As the concepts studied in this paper are defined for finite executions only, we chose not to present the background on infinite executions here; the interested reader is refered to, e.g., [START_REF] Genest | Specifying and Verifying Partial Order Properties using Template MSCs[END_REF]. Figure 1 shows an example of an HMSC. The node in the upper left corner, denoted by 7, is the starting node, hence it has an incoming edge that is connected to no other node. Initially, process © 7 sends a message to © 6, requesting a connection (e.g., to an internet service), according to the node 7. This can result in either an approval message from © 6, according to the node 6, or a failure message, according to the node . In the latter case, a report message is also sent from © 6 to some supervi- sory process © . There are two progress choices, corresponding to the two arrows out of the node . We can decide to try and connect again, by choosing the arrow from to 7, or to give up and send a service request (from process © 7 to process © ), by choosing to progress according to the arrow from to ¡. Note how the HM-SC description abstracts away the internal process computation, and presents only the communications. Consider the path £7 ¡ ¦ . According to the HMSC seman- tics, process © 6 does not necessarily have to send its Report message in before process © 7 has progressed according to ¡ to send its Req service message. How- ever, process © must receive the Report message before the Req service message.

An implementation which fully adheres to this HMSC specification will thus need, upon receiving ReqServices, to ensure that all Report messages have been received beforehand. The usual idea would be that process © is polling on both channel from P1 and from P2, giving the latter the priority. That is, if there is a message in both channels, then the message from P2 to P3 is first processed. Unfortunately, this idea does not work out, as it is possible that the last report message has not been yet sent (hence the channel is empty), while the ReqService has been sent, hence P3 would process the message ReqService before the last Report, which would contradict the HMSC specification. A designer which would only follow its (wrong) intuition (Report is sent before ReqService because it is in a previous node) would miss the problematic case and may perform a wrong design using the implementation with the polling technique described. Our aim is to detect discrepencies -which is, potential problems -and provide the designers with warnings (MSC executions of path of the HMSC) such that he can ensure that what he is doing adheres with the specification -or that he should change either the implementation or the specification (e.g. adding an acknowledgement message from © to © 7 after each reception of a report).

Allen's logic

Allen's logic [1] is a formalism that allows one to express temporal relationships between time intervals. It has 13 primitive predicates (relations) that correspond to possible relationships between two intervals, such as " precedes ¢ " or " happens during ¢ ". Each primitive predicate describes a total order between the endpoints of these intervals. When working with MSCs, we normally assume that no two events can happen at the same time, i.e., no two intervals have a common endpoint. Therefore, to represent relationships between two messages ¤ ¦ £ £ ¥¤ ¦ and ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ , we will only use 6 of these primitives, namely:

£ -¤ precedes ¤ ¡ (i.e., £ ¤ £ ¡ ¤¡ ); £¤ -¤ is preceded by ¤ ¡ (i.e., £ ¡ ¤¡ £ ¤ ); -¤ overlaps ¤ ¡ (i.e., £ £ ¡ ¤ ¤¡ ); ¤ -¤ is overlapped by ¤ ¡ (i.e., £ ¡ £ ¤¡ ¤ ); ¡ -¤ is during ¤ ¡ (i.e., £ ¡ £ ¤ ¤¡ ); ¡ ¤ -¤ contains ¤ ¡ (i.e., £ £ ¡ ¤¡ ¤ ).
Observe that for

¡ ¢ ¨£ ¥ ¥ ¡ the predicate ¡¢ is equivalent to ¢¡ ¤ . A B A B A B Fig. 2.
Allen's logic relationships: ¢ £¤ , ¢ ¥¤ , and ¢¦ § ¤ ¤ An Allen's logic formula is a concatenation of one or more of these six letters, and is interpreted as a disjunction of the corresponding predicates. For example, the formula £ ¡ ¤ ¢ says that either precedes ¢ , or overlaps ¢ , or ¢ happens during . Given the semantics of the primitive predicates, it is easy to see that this formula says that starts before ¢ , but may end before ( £ ), during ( ), or after ( ¡ ¤ ) ¢

. There are several operations that can be performed on Allen's logic formulas, such as composition and intersection. However, in this paper we only use the Allen's logic as a means to describe the relationships between the duration of messages. Therefore, we will not formally define these operations.

Relationships between Messages

In this section, we will show how to use Allen's logic to reason about the relationship between a given pair of messages.

Given an MSC ¥, a chain from an event ¨¢ ¨to an event © ¢ ¨is a sequence of events £¨¦ ¥ ¡ ¥ ¥ ¤ ¥ ¦ © ¦ such that 2 ¢ ¨for ¦ 7 ¥ ¥ , and every adjacent pair £ 2 ¥ 2 ¦ in the chain is either (i) a send and the corresponding receive, or (ii) 2 appears before (above) 2 in the same process line. Clearly, ¨ © if and only if there is a chain of messages from ¨to ©. Now, consider a pair of messages £ £ ¥¤ ¦ and £ £ ¡ ¥¤¡¦ . By definition, there is always a chain from £ to ¤ and from £ ¡ to Fig. 3. Impossible relationship between messages ¤¡ . Moreover, for any £ ¥¡¦ ¢ ¨£ ¥¤ 0 ¨£¡ ¥¤¡ , we have one of the following three cases: (1) there is a chain of messages from to ¡ ; (2) there is a chain of messages from ¡ to ; (3) there is no chain in either direction. As there are four pairs of points, this corresponds to £ ¦ ¢7 combinations. However, not all of them are possible, as MSCs do not admit cycles (see Figure 3). In fact, for two messages there are exactly twenty possible combinations of orders between their endpoints. We list them in Figure 4. In these figures, the two messages correspond to the full vertical arrows. Other arrows correspond to chains of messages that begin and end at the endpoints of these messages. Dotted arrows represent redundant information, i.e., chains that can be inferred from other chains (denoted by the dashed arrows). The patterns in Figure 4 correspond to the following Allen's logic relationships:

(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k)
(a) ££¤ ¤ ¡¡ ¤ ; (b) £ ; (c) £ ¡ ¤ ; (d) £ ; (e) ; (f) ¡ ¤ ; (g) ¡ ¤ ; (h) £ ¤ ¡¡ ¤ ; (i) ¡ ; (j) £ ¡ ; (k)
¤ ¡¡ ¤ . Except for cases (a) and (k), both of which are sym- metric, each other case has a symmetric twin that can be obtained by swapping the left and the right message.

Given two messages, we can decide according to which of the patterns they are ordered by calculating the transitive closure relation . While in general transitive closure algorithms run in cubic time [START_REF] Floyd | Algorithm 97 (Shortest Path)[END_REF][START_REF] Warshall | A Theorem on Boolean Matrices[END_REF], it has been observed [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] that in the MSC case one can be more efficient since each event has at most two successors. Formally, we have the following proposition.

Proposition 1. [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] Given an MSC with messages ¤ ¥ 4 4 4 ¥ ¤ , one can decide in time

¡ £ ¢ ¡ ¦ the relation between every ¤1 ¥ ¤ 2 , 7 £ ¤ ¥ £ ¢ .
We will now derive a corollary that will be useful in bounding the running time of our algorithms.

Corollary 1. Given an HMSC

! ¦ £ " ¥#¥ $ % ¥&¦ , ©# © ¦ ¥, one can compute the re- lation for all MSCs in # in time ¡ £ © ! © ¡ ¦ . Moreover, one can compute in time ¡ £¥ © ! © ¡ ¦ the relation
for all concatenated MSCs of the form £¥ 1 ¥ 2 ¦ , as well as every Allen's logic relationship for all pairs of messages ¤ ¢ ¥ 1 , ¤¦ ¢ ¥ 2 , where

¥ 1 ¥ ¥ 2 ¢ # .
Proof. Let ¨1 be the set of events of the MSC ¥ 1 . By Proposition 1, we can compute for ¥ 1 in time

¡ £ ©¨1 © ¡ ¦ . Therefore, computing for all ¥ 1 , ¤ ¦ 7 ¥ ¥ ¥, takes time ¡ £ ©¨ © ¡ 3 4 4 4 3 ©¨ © ¡ ¦ ¦ ¡ ££ ©¨ © 3 4 4 4 3 ©¨ ©¦ ¡ ¦ ¦ ¡ £ © ! © ¡ ¦ .
Similarly, computing the relation

for £¥ 1 ¥ 2 ¦ can be done in time ¡ ££ ©¨1 © 3 ©¨2 ©¦ ¡ ¦ . As £ ©¨1 © 3 ©¨2 ©¦ ¡ £ 6 ©¨1 © ¡ 3 6 ©¨2 © ¡ , computing
for all MSCs of the form

£¥ 1 ¥ 2 ¦ , ¤ ¥ ¦ 7 ¥ ¥ ¥, can be done in time ¡ £¥£ ©¨ © ¡ 3 4 4 4 3 ©¨ © ¡ ¦¦ ¦ ¡ £¥ © ! © ¡ ¦ . Now, fix 7 £ ¤ ¥ £ ¥. Given the relation for £¥ 1 ¥ 2 ¦ , the Allen's logic relationship for any pair £ ¤ ¥ ¤¦ ¦ , ¤ ¢ ¥ 1 , ¤¦ ¢ ¥ 2 ,
can be computed in constant time. As there are ¡ £ ©¨1 ©©¨2 ©¦ such pairs, computing the Allen's logic relationship for all of them can be done in time

¡ £ ©¨1 ©©¨2 ©¦ ¦ ¡ ££ ©¨1 © 3 ©¨2 ©¦ ¡ ¦ . Summing over all ¤ ¥ ¦ 7 ¥ ¥ ¥,
we obtain the bound of

¡ £¥ © ! © ¡ ¦ , as claimed. §

Definition of Discord

Concatenating two MSCs ¥ and ¥ ¡ does not necessarily mean that all messages of ¥ precede in time all messages of ¥ ¡ : for example, if ¥ consists of a single message from ¥ to ¥ ¡ , and ¥ ¡ consists of a single message from ¥ ¢ to ¥ £ , the relation does not provide any information about the relative order of these two messages. In what follows, we propose an Allen's logic-based formalism that allows us to quantify the ordering discrepancies that occur when concatenating MSCs. We start by considering sequences of MSCs, and then extend our analysis to HMSCs. Consider a concatenated MSC £¥ ¥ ¡¦ . For any two messages ¤ ¦ £ £ ¥¤ ¦ ¢ ¥ and ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ ¥ ¡ , we know that £ ¤ and £ ¡ ¤¡ . Now, the scenario that best matches our intuition about concatenation is when all messages in ¥ precede all messages in ¥ ¡ . In this case, we also have ¤ £ ¡ , and thus we obtain £ ¤ £ ¡ ¤¡ . This corresponds to case (b) in Figure 4. Note that this scenario is only possible when ¥ has a unique maximal event , ¥ ¡ has a unique minimal event ¦ , and and ¦ occur on the same process, i.e., © £ ¦ ¦ © £ ¦ ¦ .

Conversely, the most unintuitive situation is when the relation for £¥ ¥ ¡¦ provides no information about the relative order of some message ¤ ¡ ¢ ¥ ¡ and another message ¤ ¢ ¥ . That is, for some ¤ ¢ ¥ and ¤ ¡ ¢ ¥ ¡ , the situation is described by case (a) in Figure 4, or by the Allen's logic formula ¤ ££¤ ¤ ¡¡ ¤ ¤ ¡ . In this case, the Allen's logic formula allows ¤ ¡ to actually precede ¤ , since the disjunction permits in particular that ¤ £¤ ¤ ¡ . We consider this case to be the worst among all orders between ¤ and ¤ ¡ , because it can be the most deceiving when observing the structure of the HMSC, and hence leads to design errors. As in [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF], where the problem of conflicts is identified and diagnosed, these are potential problems that arise from the HMSC semantics. All remaining scenarios lie, as will be formulated below, between these two cases. We will now introduce a measure of discrepancy, which we call the discord, that allows us to order them more precisely.

Given a concatenation of two MSCs £¥ ¥ ¡¦ , two messages ¤ ¦ £ £ ¥¤ ¦ ¢ ¥ and ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ ¥ ¡ are said to be out of order if ¤ does not precede £ ¡ , i.e., ¤ £ ¤ ¡ . In Figure 4, this happens in cases (a), (c), (d), (h), and (j). Note that in our setting, the cases (e), (f), (g), (i), and (k) are impossible: in each of these cases, there are chains of messages starting from events of ¤ ¡ and ending in events of ¤ , which cannot happen under concatenation.

We now classify all primitive Allen's logic predicates according to how well they order the endpoints of the projected intervals, i.e., represent the order between the events of the two messages ¤ and ¤ ¡ . Recall that in the ideal case, i.e., when the order between the intervals is described by Allen's logic predicate £ , we have £ ¤ £ ¡ ¤¡ . In this case, there are zero events in ¨£¡ ¥¤¡ that precede those in ¨£ ¥¤ . In the worst case, i.e., if ¤ ¡ fully precedes ¤ , there are four inversions: namely, £ ¡ £ , ¤¡ ¤ , ¤¡ £ and £ ¡ ¤ . We thus order the predicates according to how many of these four relationships are inverted. In case of a tie, we give preference to the relationships that involve £ to those that involve ¤ . Definition 4. The total order ¡ is the transitive closure of the partial order ¡ % given by ¡ % ¦ ¨££ ¥ ¦¥ £ ¥ ¡ ¤ ¦¥ £ ¡ ¤ ¥ ¡ ¦¥ £ ¡ ¥ ¤ ¦¥ £ ¤ ¥£¤ ¦ . We denote by ¢£ ¤¥¦ the maximum element of the set ¦ with respect to ¡ . Remark 1. Observe that the number of inversions in £¤ is 4, as explained above, in ¤ it is , in ¡ and ¡ ¤ it is 2, in it is 1, and in £ it is 0. Therefore, our decision that ¡ ¤ ¡ ¡ may appear quite arbitrary. We made this choice for two reasons. First, we do think that the time when the messages are sent is more important than the time when they are received, as the designer has more control over the former, and second, it is convenient to have a total order to work with. Definition 5. Consider a sequence of MSCs £¥ ¥ ¥ ¥ ¦ and a pair of messages ¤ ¢ ¥ , ¤ ¡ ¢ ¥ such that in the MSC ¥ ¦ £¥ ¥ ¦ we have ¤ § ¤ ¡ , where § is a (possibly non-primitive) Allen's logic predicate. The discord of ¤ and ¤ ¡ with respect to ¥ is the largest possible primitive predicate, according to ¡ (i.e., the "worst") that appears in § , i.e.,

¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ , where ¡ ¢ ¨£ ¥£¤ ¥ ¥ ¤ ¥ ¡ ¥ ¡ ¤ , ¡
appears in § , and for all ¡ ¦ that appear in § we have ¡ ¦ ¡ .

Let us now apply this definition to the six cases that can occur for a pair of messages in a concatenated MSC, as illustrated in Figure 4. In case (a) the messages are in relationship ££¤ ¤ ¡¡ ¤ . The worst primitive predicate in this formula is £¤ , so we conclude that the discord between the messages is £¤ . For case (b), there is only one relation £ . Similarly, for case (c) the discord is ¡ ¤ , for case (d) it is , for (h) it is ¤ , and for (j) it is ¡ . We conclude that the value of ¨© ¨ £ ¤ ¥ ¤ ¡¦ can be any primitive Allen's logic predicate.

We now extend the definition of a discord to messages in HMSCs.

Definition 6. Given an HMSC ! ¦ £ " ¥#¥ $ % ¥&¦ and a pair of messages

¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ , let ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¢£ ¤¥ ¨¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ © 5 ¦ £ ( ¥ ¥ (¦ ¦ .
Consider now the HMSC in Figure 1. For the path £7 6 ¦ , the discord is £ , since the maximum event of 7, which is a receive, precedes the minimum event of 6, which is the send of message Approve. On the other hand, for the path £7 7 ¦ , the Report message of corresponds to the Connect message of 7 as in case (h) of Figure 4, which means a discord of ¤ . The discord of £ ¡ ¦ is ¡ due to the relative ordering between Report in and ReqService in ¡.

We will now state an observation that allows us to compute

¨© ¨ £ ¤ ¥ ¤ ¡¦ .
Recall that given a graph

" ¦ £ $ ¥'¦ , a path £ ( ¥ ¥ ( ¦ in " is called simple if it contains no cycles, i.e., (1 ¥ ¦ ( 2 for any 7 £ ¤ £ ¢ . Similarly, a cycle £ ( ¥ ¥ ( ¦ ( ¦ in " is called simple if (1 ¥ ¦ ( 2 for any 7 £ ¤ £ ¢ , £¤ ¥ ¦ ¥ ¦ £7 ¥ ¢ ¦ .
Claim 1 Consider an HMSC ! ¦ £ " ¥#¥ $ % ¥&¦ . For any ( ¥ (¦ ¢ $ , ( ¥ ¦ (¦ , and any

¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ , we have ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¢£ ¤¥ ¨¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ © 5 ¦ £ ( ¥ ¥ (¦ ¦ is a simple path. Also, for two messages ¤ ¥ ¤ ¡ ¢ & £ ( ¦ , we have ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¢£ ¤¥ ¨¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ © 5 ¦ £ ( ¥ ¥ ( ¦ is a simple cycle.
Proof. Clearly, removing a cycle from a path between ( and (¦ can only worsen the discord between ¤ and ¤ ¡ , as this may eliminate some of the chains between the endpoints of ¤ and ¤ ¡ . Hence, the path that exhibits the worst-case discord is cycle- free. The same argument applies for two messages in the same node of an HMSC. §

Observe that Claim 1 implies that the discord of the HMSC ! in Figure 1 is ¦ ¤ .

Computing the Discord of a Pair of Messages

For a simple path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ , computing ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ for ¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ is easy. Namely, first we run the transitive closure algorithm to determine the causal relationships between the endpoints of ¤ and ¤ ¡ . We then identify the corresponding scenario of Figure 4 and apply the case analysis presented after Definition 5. The running time of this algorithm is quadratic in the total number of messages in & £5 ¦ .

For HMSCs, Definition 6 and Claim 1 suggest a straightforward algorithm for computing the discord: given two messages ¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ , we can consider each simple path from ( to (¦ (or each simple cycle, if ( ¦ (¦ ), compute the discord along this path, and output the maximum discord obtained in this way. This naive algorithm runs in exponential time in the input size. In the next subsection, we show that this is perhaps inevitable: we prove that in general the problem of computing § © ¨ £ ¤ ¥ ¤ ¡¦ is coNP-hard. However, we will now provide an alternative way of verifying whether § © ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ , where ¡ ¢ ¨£ ¥£¤ ¥ ¥ ¤ ¥ ¡ ¥ ¡ ¤ . As we will see later, this can be used to construct an efficient algorithm for computing § © ¨ £ ¤ ¥ ¤ ¡¦ in the important special case when the number of processes is constant.

We will first define a related problem that will be useful for stating our results.

PATH WITH NO CHAIN: Given an HMSC ! ¦ £ " ¦ £ $ ¥'¦¥#¥ $ % ¥&¦ , a pair of nodes ( ¥ (¦ ¢ $

, and a pair of events ¢ & £ ( ¦¥ ¦ ¢ & £ (¦ ¦ , is there a path 5 from ( to (¦ in " such that in the MSC & £5 ¦ there is no chain of events from to ¦ ? We will write ¡¢ £ ¥ ¦ ¦ ¦ 7 if such path exists and ¡¢ £ ¥ ¦ ¦ ¦ £ otherwise.

Proposition 2. Given an HMSC ! ¦ £ " ¦ £ $ ¥'¦¥#¥ $ % ¥&¦ , a pair of nodes ( ¥ (¦ ¢ $ , and a pair of messages

¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ , we have - ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ £ if and only if ¡¢ £ ¤ ¥ £ ¡¦ ¦ £. - ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ if and only if ¡¢ £ ¤ ¥ £ ¡¦ ¦ 7, ¡¢ £ £ ¥ £ ¡¦ ¦ £, and ¡¢ £ ¤ ¥¤¡¦ ¦ £. - ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ ¤ if and only if ¡¢ £ ¤ ¥¤¡¦ ¦ 7 and ¡¢ £ £ ¥ £ ¡¦ ¦ £. - ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡
if and only if ¡¢ £ £ ¥ £ ¡¦ ¦ 7 and for any path 5 ¦ £ ( ¥ ¥ (¦ ¦ in "

, the MSC & £5 ¦ contains a chain from £ to £ ¡ or a chain from ¤ to ¤¡ . -¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¤ if and only if there exists a path 5 ¦ £ ( ¥ ¥ (¦ ¦ in " such that the MSC & £5 ¦ contains no chain from £ to £ ¡ and no chain from ¤ to ¤¡ , and ¡¢ £ £ ¥¤¡¦ ¦ £.

- ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ £¤ if and only if ¡¢ £ £ ¥¤¡¦ ¦ 7.
Proof. The analysis for £ , , and £¤ is straightforward.

If

¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ ¤ , then there is a path 5 ¦ £ ( ¥ ¥ (¦ ¦ that satis- fies ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¦ ¡ ¤ . Clearly, & £5 ¦ contains no chain from ¤ to ¤¡ , so ¡¢ £ ¤ ¥¤¡¦ ¦ 7. Also, for any path 5 ¦ from ( to (¦ , we have ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ , so 5 ¦ contains a chain from £ to £ ¡ . Hence, ¡¢ £ £ ¥ £ ¡¦ ¦ £. Con- versely, if ¡¢ £ ¤ ¥¤¡¦ ¦ 7, then there is a path 5 from ( to (¦ with no chain from ¤ to ¤¡ , so it cannot be the case that ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ . Hence, ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¥ ¡ ¤ . On the other hand, ¡¢ £ £ ¥ £ ¡¦ ¦ £ means that any path 5 ¦ from ( to (¦ contains a chain from £ to £ ¡ , so we have ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¡¦ ¥ ¢ ¨¡¥ ¤ ¥£¤ . Other cases can be analyzed similarly. § Note that to check if ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ for ¡ ¢ ¨£ ¥£¤ ¥ ¡ ¤ ¥ , it suffices to make a small number of calls to ¡¢ . However, to check if ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ for ¡ ¢ ¨¡¥ ¤ , calling ¡¢ is not enough. Indeed, to verify, e.g., whether ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ , we have to check that any path between the corresponding nodes contains either one of two chains: a chain from £ to £ ¡ or a chain from ¤ to ¤¡ , and this check cannot be simulated by calls to ¡¢ .

Computational hardness

We will now show that for HMSCs the problem of upper-bounding ¨© ¨ £ ¤ ¥ ¤ ¡¦ is coNP-complete. Formally, we consider the following problem: DISCORD £! ¥ ¡ ¥ ¤ ¥ ¤ ¡¦ : Given an HMSC !, a predicate ¡ ¢ ¨£ ¥£¤ ¥ ¥ ¤ ¥ ¡ ¥ ¡ ¤ , and two messages ¤ ¥ ¤ ¡ in !, is it the case that ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¡ ? Theorem 1. The problem DISCORD £! ¥ ¡ ¥ ¤ ¥ ¤ ¡¦ is coNP-complete. Proof. To see that DISCORD £! ¥ ¡ ¥ ¤ ¥ ¤ ¡¦ is in coNP, observe that the complementary problem of checking whether ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¡ is in NP: a certificate can be provided by a path 5 such that ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¡ . In particular, for ¡ ¦ £ a certificate is a path with no chain from ¤ to £ ¡ , for ¡ ¦ it is a path with no chain from ¤ to ¤¡ , for ¡ ¦ ¡ ¤ it is a path with no chain from £ to £ ¡ , for ¡ ¦ ¡ it is a path with no chain from £ to £ ¡ and no chain from ¤ to ¤¡ , and for ¡ ¦ ¤ it is a path with no chain from £ to ¤¡ .

The coNP-hardness proof is by reduction from 3SAT. Suppose that we are given a 3CNF formula with a set of variables ¨ ¥ ¥ ¨ and a set of clauses ¡ ¥ ¥ ¡¢.

Let £ 2 ¥ £ ¡ 2 ¥ £ ¢ 2 be the literals that appear in the th clause, i.e., ¡ 2 ¦ £ 2 ¤ £ ¡ 2 ¤ £ ¢ 2 , £ 2 ¢ ¨¨ ¥ ¥ ¨ ¥ ¥ ¨ ¥ ¥ ¥ ¨ . We construct an HMSC ! as follows. Set § ¦ ¨¥ ¥ ¥ ¡ ¥ ¥ ¢ ¥ ¥ £ ¥ ¥ ¦ ¥ ¥ § ¦ ¥ ¥ ¥ ¦¨¥¥ § ¦¨¥¥© ¥ ¥ ¥ ©.
The HMSC ! has the following structure. Its underlying graph " has a source node ( % , a sink node ( , and ¥ 3 ¤ gadget subgraphs, namely ¥ variable gadgets ¥ ¥ and ¤ clause gadgets ¥ ¥ ¢. The variable gadget 1 consists of four vertices

% 1 , 1 , ¡ 1 , ¢ 1 and four edges £ % 1 ¥ 1 ¦ , £ % 1 ¥ ¡ 1 ¦ , £ 1 ¥ ¢ 1 ¦ , £ ¡ 1 ¥ ¢ 1 ¦ . The clause gadget 1 consists of five vertices % 1 , 1 , ¡ 1 , ¢ 1 , £ 1 and six edges £ % 1 ¥ 1 ¦ , £ % 1 ¥ ¡ 1 ¦ , £ % 1 ¥ ¢ 1 ¦ , £ 1 ¥ £ 1 ¦ , £ ¡ 1 ¥ £ 1 ¦ , £ ¢ 1 ¥ £ 1 ¦
. The source, the vertex gadgets, the clause gadgets, and the sink are all connected in series as depicted in Figure 5. More precisely, there is an edge from ( % to the vertex % , for all ¤ ¦ 7 ¥ ¥ ¥ 7 there is an edge from It remains to define the MSCs that are placed in the vertices of " . The MSC in ( % consists of a single message £ £ ¥¤ ¦ from ¥ to ¥ ¡ . The MSCs in the vertices

£ ¢ to ( . v 0 v 1 X 1 X n Y 1 Y m X 2
% 1 , ¢ 1 , % 2 , £ 2
are empty for all ¤ ¦ 7 ¥ ¥ ¥, ¦ 7 ¥ ¥ ¤ . For ¤ ¦ 7 ¥ ¥ ¥, the MSC in 1 consists of a message from ¥ ¡ to ¥ ¦, and the MSC in

¡ 1 consists of a message from ¥ ¡ to ¥ § ¦. For ¦ 7 ¥ ¥ ¤ , ¦ 7 ¥ 6 ¥ , the MSC in
2 contains a message from ¥ to ¥ © , where £ 2 is the th literal of ¡ 2 . Finally, the MSC in ( has ¤ 3 7 messages: a message from each ¥ © , ¦ 7 ¥ ¥ ¤ , to ¥ ¢ , and a message ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ from ¥ ¢ to ¥ £ that is sent after all messages from all ¥ © are received.

We claim that the original 3CNF formula is satisfiable if and only if the tuple £! ¥£¥ ¤ ¥ ¤ ¡¦ constitutes a "no"-instance of DISCORD £! ¥£¥ ¤ ¥ ¤ ¡¦ , i.e., there is a path 5 from ( % to ( such that the MSC & £5 ¦ contains no chain from ¤ to £ ¡ . Indeed, suppose that our formula is satisfiable, and let ¤ ¦ £ ¢ ¥ ¥ ¢ ¦ , ¢ 1 ¢ ¨¥ ¥¦ be a satisfying assignment for it. Consider a path 5 that satisfies the follow- ing conditions:

-5 starts at ( % and ends at ( ;

-5 1 ¦ ¨% 1 ¥ 1 ¥ ¢ 1 if ¢ 1 ¦ ¦ and 5 1 ¦ ¨% 1 ¥ ¡ 1 ¥ ¢ 1 if ¢ 1 ¦ ¥ ; -5 2 ¦ ¨% 1 ¥ 2 ¥ £ 2 for some ¢ ¨7¥ 6 ¥ such that £ 2 is true under ¤ , i.e., £ 2 ¦ ¨ § and ¢ § ¦ ¥ or £ 2 ¦ ¥ ¨ § and ¢ § ¦ ¦ . Note that such £
2 is guaranteed to exist since ¤ has to satisfy ¡ 2 . First, note that in the corresponding MSC & £5 ¦ there is no chain from ¤ to any event of any of the processes ¥ © , ¦ 7 ¥ ¥ ¤ . Indeed, the only message received by ¥ © in & £5 ¦ is from some ¥ such that £ 2 is true under ¤ . Since £ 2 is true under ¤ , in & £5 ¦ the process ¥ receives no messages whatsoever. As ¥ ¢ only receives messages from ¥ © , ¦ 7 ¥ ¥ ¤ , we conclude that in & £5 ¦ there is no chain from ¤ to £ ¡ .

Conversely, suppose that there is a path 5 such that in the corresponding MSC & £5 ¦ there is no chain from ¤ to £ ¡ . Consider a satisfying assignment ¤ ¦ £ ¢ ¥ ¥ ¢ ¦ such that

¢ 1 ¦ ¦ if 5 1 ¦ ¨% 1 ¥ 1 ¥ ¢ 1 and ¢ 1 ¦ ¥ if 5 1 ¦ ¨% 1 ¥ ¡ 1 ¥ ¢ 1 .
Note that for any

¦ 7 ¥ ¥ ¤ , if 5 2 ¦ ¨% 1 ¥ 2 ¥ £ 2
for some ¦ 7 ¥ 6 ¥ , it must be the case that ¥ receives no message from ¥ ¡ in & £5 ¦ , because otherwise there would be a chain of messages from ¤ to £ ¡ . Hence, the literal £ 2 is true under ¤ , i.e., ¡ 2 is satisfied. As this holds for any ¦ 7 ¥ ¥ ¤ , we have successfully constructed a satisfying assignment for our instance of 3CNF. § Remark 2. Clearly, the proof of Theorem 1 implies that PATH WITH NO CHAIN is NPhard. Moreover, we can consider a weaker version of DISCORD, in which the Allen's logic predicate is not part of the input. Namely, for ¡ ¢ ¨£ ¥£¤ ¥ ¥ ¤ ¥ ¡ ¥ ¡ ¤ , let DISCORD¨£! ¥ ¤ ¥ ¤ ¡¦ be the problem of checking whether ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¡ . Obviously, for ¡ ¦ £¤ this problem is trivially in P: the answer is always "yes". The proof of Theorem 1 shows that this problem is coNP-hard for ¡ ¦ £ . To show that it is hard for ¡ ¦ , we can modify the reduction by changing the direction of ¤ (i.e., setting © £ £ ¦ ¦ ¥ ¡ , © £ ¤ ¦ ¦ ¥ ) and adding to the MSC in ( % a message ¤¦ ¦ £ £¦ ¥¤ ¦ ¦ from ¥ to ¥ £ with ¤ £¦ . Then in any path in ! there is a chain from ¤ to ¤¡ , and there is a path with no chain from £ to £ ¡ if and only if the 3CNF formula has a satisfying assignment. Similarly, to show that DISCORD ¡ £! ¥ ¤ ¥ ¤ ¡¦ is coNP-hard, we change the direction of ¤ , to show that DISCORD £! ¥ ¤ ¥ ¤ ¡¦ is coNP-hard, we change the direction of ¤ ¡ , and to show that DISCORD¢¡ £! ¥ ¤ ¥ ¤ ¡¦ is coNP- hard, we change the direction of both ¤ and ¤ ¡ . We conclude that all five non-trivial versions of the problem are coNP-hard.

Polynomial-time algorithms for bounded number of processes

In our hardness result, both the size of the graph " and the number of processes § are unbounded. It turns out that this is necessary: if either of these parameters is constant, there is an algorithm whose running time is polynomial in the other parameter. This is easy to see if the size of the graph is constant. In particular, the naive algorithm described in the beginning of this section will run in polynomial time: in a graph with a constant number of vertices, there is a constant number of simple paths and cycles, and one can compute the discord along a path in polynomial time.

The case when the number of processes is constant is considerably more complicated. Our algorithm for this setting is based on Dijkstra's shortest path algorithm combined with dynamic programming approach. The underlying idea is that given a pair of events ¢ & £ ( ¦ , ¦ ¢ & £ (¦ ¦ and a subset of processes £ , we can check if there is a path 5 from ( to (¦ such that the set of processes reachable from in & £5 ¦ is exactly £ . A generalization of this idea allows us to compute the discord of any pair of messages in an HMSC in polynomial time for any fixed value of © § © . Formally, we prove the following result.

Theorem 2. It is possible to compute

¨© ¨ £ ¤ ¥ ¤ ¡¦ in time ¡ £¥ ¢ 6 £¤ ¤ © ! © ¡ ¦ , which
is polynomial in ¥ ¦ © $ © and © ! © for any fixed value of © § © .

We start by describing an algorithm for PATH WITH NO CHAIN. Next, we show how to generalize it to compute ¨© ¨ £ ¤ ¥ ¤ ¡¦ . Note that just like in Dijkstra's algorithm, we simultaneously check whether there is a path with no chain from a given event ¢ ¥ ¦ & £ ( ¦ to all other events. Therefore, this algorithm can be easily adapted to compute the discords for all pairs of messages in ! in time

¡ £¥ ¢ 6 £¤ ¤ © ! © ¢ ¦ .
Let ¥ be a strict upper bound on the number of events on any process line in any MSC in !. Re-number all events so that 1¦ 2 , ¦ 7 ¥ ¥ ¥ 7, is the th event on the process line ¥ 2 in the MSC ¥ 1 . For the purposes of the algorithm, we will introduce two dummy events §¨© 1¦ 2 and § 1¦ 2 on each process line of every MSC in !. The event §¨© 1¦ 2 precedes all events 1¦ 2 , and the event § 1¦ 2 follows all events 1¦ 2 . It is important to note that these are not send or receive events, so they have no effect on the information flow in !. However, we will occasionally talk about chains to and from these events, where a chain is defined in the same way as for regular events. We say that a process ¥ 2 is reachable from along a path ( ¦ £ ( ¥ ¥ (1

¦ if in the MSC £¥ ¥ 1 ¦ there is a chain from to § 1¦ 2 .
The outline of the algorithm is presented in Figure 7. First, for each MSC ¥ 1 and all £ ¦ 7 ¥ ¥ © § © , the procedure ComputeX() checks whether there is a chain from §¨© 1¦ to all other events in this MSC. More precisely, for ¦ 7 ¥ ¥ ¥ 7, ComputeX() sets £¤ ¥ ¥¥ £ ¦ ¦ 7 if in ¥ 1 there is a chain from §¨© 1¦ to 1¦ 2 and £¤ ¥ ¥¥ £ ¦ ¦ £ otherwise. Also, it sets £¤ ¥ ¥ ¥ ¥ £ ¦ ¦ 7 if in ¥ 1 there is a chain from §¨© 1¦ to § 1¦ 2 , and £¤ ¥ ¥ ¥ ¥ £ ¦ ¦ £ otherwise. Note that for ¥ ¦ £ there can be no chain from §¨© 1¦ 2 to §¨© 1¦ . By Corollary 1, we can implement ComputeX()

in time ¡ £ © ! © ¡ ¦ . ¡¢£ ¤ ¥¦¥ § ¡¨£ © ; 1. ComputeX(); 2. ComputeY(); 3. forall such that ¤ ¡ ¤ ¦ ¡ © 4. forall 5. if ¦ ! " break; 6. forall #$ % 7. if ¤ ¦&¦ '¦( © ! ) break; 8.
return ''yes''; Fig. 7. The algorithm for ¡¢£ ¤ ¥¦¥ § ¡¨£ © , with ComputeY() given in Figure 8.

Further, for any £ ) § let £ £ ¥ ¤ ¦ be a variable that indicates whether there is a

path 5 in " from ( to (1 such that in & £5 ¦ none of the processes in £ is reachable from
. We set £ £ ¥ ¤ ¦ ¦ 7 if such a path exists and £ £ ¥ ¤ ¦ ¦ £ otherwise. The values of £ £ ¥ ¤ ¦ are computed by the procedure ComputeY() given in Figure 8. We will discuss how to implement ComputeY() later on. Now, assume that we have computed £ £ ¥ ¤ ¦ , £¤ ¥ ¥¥ £ ¦ , for all £ ) §

, ¤ ¦ 7 ¥ ¥ ¥, ¤ ¥ ¦ 7 ¥ ¥ © § © , ¦ 7 ¥ ¥ ¥.
Then there is a path with no chain from to 1¦ 2 if and only if the conditions in the lines 3-7 hold, i.e., there is a path 5 of the form

£ ( ¥ ¥ (1 ¤ ¥ (1 ¦ and a set £ ) §
such that for any process ¥ that is reachable from along 5 ¦ ¦ £ ( ¥ ¥ (1 ¤¦ (i.e., a process in § 0 £

), there is no chain from §¨© 1¦ to 1¦ 2 .

For a fixed event

1¦ 2 this condition can be verified in time ¥6 ¤ ¤ © § © .
It remains to argue that the procedure 12 34567 8 £ ¦ in Figure 8 correctly computes the values of £ £ ¥ ¤ ¦ . The procedure starts by initializing the variables 89£ ¥ ¤ @ (lines 1-6). For ¤ ¥ ¦ 7, it sets 89£ ¥ ¤ @ ¦ £ for all £ ) §

. For ¤ ¦ 7, it computes £ £ ¥ 7 ¦ (recall that £ £ ¥ 7 ¦ ¦ 7 if and only if there is no chain from to § ¦ 2 for any ¥ 2 ¢ £ ) and sets 89£ ¥ ¤ @ ¦ £ £ ¥ ¤ ¦ . The algorithm then repeats a Dijkstra-like "relaxation" step ¥ times. During each step, the value of each 89£ ¥ ¤ @ may be changed from 0 to 1. The correctness of the algorithm follows from two simple claims.

Claim 2 If £ £ ¥ ¤ ¦ ¦ £, we have 89£ ¥ ¤ @ ¦ £ at any point in the execution of 12 34567 8 £ ¦ .

Proof. The proof is by induction on the execution of the algorithm. The claim is clearly true after the initialization step. Now, suppose that at some point we change the from 0 to 1 for some £ ¥ ¤. This means that we have discovered some

¤ ¦ ¥ £ ¦ such that £ (1 ¤ ¥ (1 ¦ ¢ ' , 89£ ¦ ¥ ¤ ¦ @ ¦ 7.
By inductive assumption, this means that there exists a path 5 from ( to (1 ¤ such that in the MSC £¥ ¥ 1 ¤¦ there is no chain from to any of the processes in £ ¦ . Moreover, we also have £¤ ¥ ¥ ¥ ¥ £ ¦ ¦ £ for any ¥ ¢ § 0 £ ¦ and any ¥ 2 ¢ £ , i.e., in the MSC £¥ ¥ 1 ¤ ¥ 1 ¦ there is no chain from §¨© 1¦ to § 1¦ 2 . Now, suppose that in £¥ ¥ 1 ¤ ¥ 1 ¦ there is a chain from to some ¥ 2 ¢

£

. As there are no events that are sent in one MSC and are received in another MSC, this chain would have to go through some § 1¤ ¦ , §¨© 1¦ , £ ¦ 7 ¥ ¥ © § © . If ¥ ¢ £ ¦ , this means that there is a chain in £¥ ¥ 1 ¤¦ from to ¥ , a contradiction. On the other hand, if ¥ ¢ § 0£ ¦ , there is a chain from §¨© 1¦ to § 1¦ 2 , a contradiction again. We conclude that £ £ ¥ ¤ ¦ ¦ 7. § Claim 3 If for some £ ¥ ¤, there exists a path £ ( ¥ ¥ (1 ¤ ¥ (1 ¦ of length £ such that in the MSC £¥ ¥ 1 ¤ ¥ 1 ¦ there is no chain from to any of the processes in £

, then after £ steps, ComputeY() sets 89£ ¥ ¤ @ ¦ 7.

Proof. The proof is by induction on £. The claim is obviously true for £ ¦ 7. Let £ ¦ be the set of all processes that are not reachable from along £¥ ¥ ¥ ¥ 1 ¤¦ . By inductive assumption, after £7steps we have 89£ ¥ ¤ ¦ @ ¦ 7. Also, by construction, in £¥ ¥ 1 ¤¦ there is a chain from to § 1¦ for any £ ¢ § 0 £ ¦ . Hence, we have £¤ ¥ ¥ ¥ ¥ £ ¦ ¦ £ for any ¥ ¢ § 0 £ ¦ , ¥ 2 ¢ £ . Therefore, during the £th step, our algorithm will set 89£ ¥ ¤ @ ¦ 7. § It is not hard to verify that the running time of 12 34567 8 £ ¦ is ¡ £¥ ©' © 6 ¡¤ ¤ © § © ¡ ¦ . Indeed, the running time of this procedure is dominated by the cycle in lines 8-16, which is repeated ¥ times. During each such cycle, we consider each edge of ' exactly once (in lines 8 and 11), for each such edge we consider two subsets of § , and for each choice of these subsets we consider a pair of processes and do a constant-time check for this pair. The overall running time of our algorithm can then be expressed as

¡ £¥ ©' © 6 ¡¤ ¤ © § © ¡ 3 © ! © ¡ ¦ ¦ ¡ £¥ ¢ 6 ¡¤ ¤ © ! ©
¡ ¦ . Now, suppose that we are given a pair of messages ¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ . By Proposition 2, we can check whether ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ for ¡ ¢ ¨£ ¥ ¥ ¡ ¤ ¥£¤ by making at most three calls to ¡¢ £ ¦ . However, to decide between ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ and ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¤ , we need additional tools. Fortunately, it turns out that one can modify ¡¢ £ ¦ to solve this problem.

To verify whether

¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¡ , we first compute ¡¢ £ £ ¥ £ ¡¦ . If we have ¡¢ £ £ ¥ £ ¡¦ ¦ £, then ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¡ ¡
, so the answer is negative. Otherwise,

¨© ¨ £ ¤ ¥ ¤ ¡¦ ¥ ¦ ¡
if and only if " contains a path 5 from ( to (¦ such that in & £5 ¦ there is no chain from £ to £ ¡ and no chain from ¤ to ¤¡ . To find such a path, we first compute £¤ ¥ ¥¥ £ ¦ using ComputeX(). We then define ¦ £ £ ¥ £ ¦ ¥ ¤ ¦ as follows: for any

£ ¥ £ ¦ ) § and any ¤ ¦ 7 ¥ ¥ ¥, set ¦ £ £ ¥ £ ¦ ¥ ¤ ¦ ¦ 7 if
£ £ ¥ £ ¦ ¥ ¤ ¦ for all £ ¥ £ ¦ ) § , ¤ ¦ 7 ¥ ¥ ¥.
Assume that

(¦ ¦ (1 and £ ¡ ¦ 1 ¦ 2 , ¤¡ ¦ ¤ 1 ¦ 2 ¤ We have ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¡ if and only if there exists a triple £ ¥ £ ¦ ¥ ¤ ¦ such that (1) £ (1 ¤ ¥ (1 ¦ ¢ ' ; (2) ¦ £ £ ¥ £ ¦ ¥ ¤ ¦ ¦ ¦ 7;
(3) for any ¥ ¢ § 0 £ we have £¤ ¥ ¥¥ £ ¦ ¦ £; (4) for any ¥ ¢ § 0 £ ¦ we have £¤ ¥ ¦ ¥ ¦ ¥ £ ¦ ¦ £.

These conditions can be verified in time

From Pairs of Messages to HMSCs

It is desirable to be able to characterize the discord of an HMSC with a single parameter rather than list the discords for all pairs of messages in this HMSC. To this end, we extend the definition of discord from pairs of messages to entire HMSCs by defining the discord of an HMSC ! to be the worst discord over all pairs of messages in

In the rest of the section, we describe polynomial-time algorithms for checking that § © ¨£! ¦ ¦ ¡ for ¡ ¢ ¨£ ¥£¤ ¥ ¥ ¤ ¥ ¡ ¤ . To check whether § © ¨£! ¦ ¦ ¡ , we can simply run all these algorithms and return "yes" if all of them return "no". We analyze the efficiency of these algorithms in terms of ¥ ¦ © $ © , © § © and © ! © ; observe that we can assume ¥ ¦ ¡ £ © ! ©¦ , © § © ¦ ¡ £ © ! ©¦ .

For the cases ¡ ¢ ¨£ ¥ ¥ ¡ ¤ , we will make use of a set ' ¡ $ 0 $ , constructed as follows: £ ( ¥ (¦ ¦ ¢ ' if and only if £ ( ¥ (¦ ¦ ¢ ' or there exists a path £ ( ¦ ( ¥ ( ¡ ¥ ¥ ( ¤ ¥ ( ¦ (¦ ¦ such that for ¦ 6 ¥ ¥ 7 the MSC & £ ( 2 ¦ has an empty message set. Note that ' is a subset of the transitive closure of ' , i.e., £ ( ¥ (¦ ¦ ¢ ' implies that in " there is a path from ( to (¦ . To construct ' , we can run the depth-first search from each node of $ , backtracking as soon as we discover a node whose MSC has a non-empty message set. Clearly, this algorithm finds a path from ( to (¦ if and only if £ ( ¥ (¦ ¦ ¢ ' . Moreover, as the depth- first search runs in time ¡ £ © $ ©3 ©' ©¦ ¦ ¡ £ © ! ©¦ , the total running time of this procedure is ¡ £¥ © ! ©¦ .

¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦
¦ and any path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ . We show by induction on that if our condition holds then ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¦ £ . The proof is based on the fact that for any three time intervals ¥ ¢ ¥ ¥, we have £ ¢ ¢ £ ¥ ¦ £ ¥. For ¦ 6, the statement is obvious. Now, suppose 6. If for each ¦ 6 ¥ ¥ 7, the MSC & £ ( 2 ¦ has an empty message set, then we have £ ( ¥ (¦ ¦ ¢ ' and & £5 ¦ ¦ £ & £ ( ¦& £ (¦ ¦¦ , so ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¦ £ . Now suppose that for some ¢ ¨6¥ ¥ 7 the MSC & £ ( 2 ¦ has a non-empty message set and consider some ¤ ¦ £ £ ¥¤¦ ¢ & £ ( 2 ¦ . Set 5 ¦ ¦ £ ( ¥ ¥ ( 2 ¦ , 5 ¦¦ ¦ £ ( 2 ¥ ¥ ( ¦ . By the induction hy- pothesis, ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¦ ¦ £ , ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¡¦ ¦ £ , so in & £5 ¦ ¦ there is a chain from ¤ to £ , and in & £5 ¦¦ ¦ there is a chain from ¤ to £ ¡ . We conclude that in & £5 ¦ there is a chain from ¤ to £ ¡ , i.e., ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¦ £ . This algorithm can be implemented in time ¡ £¥ © ! © ¡ ¦ as follows: we first construct ' (as shown above, this can be done in time ¡ £¥ © ! ©¦ ), and then for each £ ( ¥ (¦ ¦ ¢ ' we compute the relation for the concatenated MSC £ & £ ( ¦& £ (¦ ¦¦ (this can be done in time ¡ £¥ © ! © ¡ ¦ for all £ ( ¥ (¦ ¦ ¢ ' by Corollary 1) and use it to check the discord of all pairs ¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ (again, by Corollary 1 this takes time ¡ £¥ © ! © ¡ ¦ ).

¢£¤¥ ¦ ¡ §¨©

The algorithm and the analysis are similar to the previous case.

Namely, § © ¨£! ¦ ¦ if and only if § © ¨£! ¦ ¥ ¦ £ (which can be verified in polynomial time, as described above) and for any £ ( ¥ (¦ ¦ ¢ ' and any ¤

¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ we have ¨© ¨¢¡¢ ¤ ¡¢ ¤¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ . The running time of this algorithm is ¡ £¥ © ! © ¡ ¦ .
The proof is based on the fact that for any path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ , any £5 ¦ ¥ 5 ¦¦ ¦ such that 5 ¦ ¦ £ ( ¥ ¥ ( 2 ¦ , 5 ¦¦ ¦ £ ( 2 ¥ ¥ ( ¦ and any ¤

¦ £ £ ¥¤¦ ¢ & £ ( 2 ¦ , if ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¦ ¢ ¨£ ¥ and ¨© ¨¡¢ £¤¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ then ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ .
To see this, note that ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¦ ¢ ¨£ ¥ implies that & £5 ¦ ¦ has chains from £ to £ and from ¤ to ¤ , and ¨© ¨¡¢ £¤¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ implies that & £5 ¦¦ ¦ has chains from £ to £ ¡ and from ¤ to ¤¡ . Hence, in & £5 ¦ there are chains from £ to £ ¡ and from ¤ to ¤¡ , i.e., ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ .

¢£¤¥ ¦ ¡ §¨© ¡ ¡

The algorithm and the analysis are similar to the previous two cases. Namely, § © ¨£! ¦ ¦ ¡ ¤ if and only if § © ¨£! ¦ ¥ ¦ £¥ (which can be verified in polynomial time, as described above) and for any £ ( ¥ (¦ ¦ ¢ ' and any

¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ we have ¨© ¨¢¡¢ ¤ ¡¢ ¤¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ . The running time of this algorithm is ¡ £¥ © ! © ¡ ¦ .
The proof uses the fact that for any path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ , any £5 ¦ ¥ 5 ¦¦ ¦ such that 5 ¦ ¦ £ ( ¥ ¥ ( 2

¦ , 5 ¦¦ ¦ £ ( 2 ¥ ¥ ( ¦ and any ¤ ¦ £ £ ¥¤¦ ¢ & £ ( 2 ¦ , if ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¦ ¢ ¨£ ¥ ¥ ¡ ¤ and ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ then ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ . Indeed, ¨© ¨¡¢ £¤¤ £ ¤ ¥ ¤ ¦ ¢ ¨£ ¥ ¥ ¡ ¤ im- plies that & £5 ¦ ¦ contains a chain from £ to £ , and ¨© ¨¡¢ £¤¤¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ implies that & £5 ¦¦ ¦ contains a chain from £ to £ ¡ . Hence, in & £5 ¦ there is a chain from £ to £ ¡ , i.e., ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¢ ¨£ ¥ ¥ ¡ ¤ . ¢£¤¥ ¦ ¡ §¨© £ ¡ If § © ¨£! ¦ ¦ £¤ , there exists a pair of nodes ( ¥ (¦ ¢ $ , a pair of messages ¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ and a path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ such that ¨© ¨¡¢ £¤ £ ¤ ¥ ¤ ¡¦ ¦ £¤ , i.e., in & £5 ¦ there is no chain from £ to ¤¡ . Let ¥ ¦ & £ ( ¦ , ¥ ¦ ¦ & £ (¦ ¦ , and ¥ ¥ ¦ & £ ( ¡ ¥ ¥ ( ¤ ¦ . Let £ be a maximal send event in £¥ ¥
¥ ¦ such there is a chain from £ to £ , and let ¤ be the corresponding receive. Set ¥ ¦ © £ £ ¦ , ¢ ¦ © £ ¤¦ . It is easy to see that in 5 there is no chain from £ to ¤¡ , or, equivalently, £ £ ¥¤¦£¤ ¤ ¡ . Therefore, without loss of generality we can assume ¤ ¦ £ £ ¥¤¦ , i.e., £ is a maximal send event in £¥ ¥ ¥ ¦ . This implies that in £¥ ¥ ¥ ¦ there are no send events on ¥ that happen after £ , and there are no send events on ¢ that happen after ¤ (for any such event, there would be a chain from £ to this event). Moreover, in ¥ ¦ there is no chain from any event of ¥ or ¢ to ¤¡ . This suggests the following algorithm. For each pair ( ¥ (¦ ¢ $ and each pair of

messages ¤ ¦ £ £ ¥¤ ¦ ¢ & £ ( ¦ , ¤ ¡ ¦ £ £ ¡ ¥¤¡¦ ¢ & £ (¦ ¦ do the following. Set ¥ ¦ © £ £ ¦ , ¢ ¦ © £ ¤ ¦ . Let ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ be
the HMSC obtained by deleting from ! all nodes other than ( ¥ (¦ that have send events on ¥ or ¢. Output "yes" if all of the following four conditions hold:

(1) in & £ ( ¦ there are no send events on ¥ after £ ;

(2) in & £ ( ¦ there are no send events on ¢ after ¤ ;

(3) in & £ (¦ ¦ there is no chain from any event of ¥ or ¢ to ¤¡ (in particular, © £ ¤¡ ¦ ¥ ¦ ¥ ¥ ¢); (4) the HMSC ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ contains a path from ( to (¦ .

If (1)-( 4) are all true, then the pair £ ¤ ¥ ¤ ¡¦ provides a witness that § © ¨£! ¦ ¦ £¤ . Conversely, by the reasoning above, if § © ¨£! ¦ ¦ £¤ , then there is a pair £ ¤ ¥ ¤ ¡¦ that satisfies (1)-(4).

The running time of this algorithm can be bounded by ¡ £ © ! © ¢ ¦ . To see this, note that there are We can change the order of operations so that the algorithm runs in time

¡ £ © ! © ¡ ¦ pairs of messages ¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ .
¡ £ © § © ¡ © ! © ¡ ¦ .
This is more efficient if © § © ¡ © ! © , which is likely to be the case in practice. First, we compute the transitive closure of each MSC in !; by Corollary 1, this can be done in time ¡ £ © ! © ¡ ¦ . Then for each ( ¢ $ , each event in & £ ( ¦ , and each ¥ ¢ §

, we use the information about the transitive closure to check whether in & £ ( ¦ there is a chain from any event of ¥ to . There are ¡ £ © ! ©¦ events, © § © processes, and for each pair £¥ ¥ ¦ , ¢ ¨1, this computation takes ¡ £ © ! ©¦ steps, so this can be done in time ¡ £ © § ©© ! © ¡ ¦ . For any pair ¥ ¥ ¢ ¢ § set % £¥ ¥ ¢ ¦ ¦ ¨( ¢ $ © & £ ( ¦ has no send events on ¥ ¥ ¢.

Consider a modified version of the depth-first search on " that backtracks as soon as it reaches a node in $ 0 % £¥ ¥ ¢ ¦ . This algorithm discovers a path from ( to (¦ if and only if the HMSC ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ contains a path from ( to (¦ . From any given ( , it runs in time ¡ £ © ! ©¦ . For each (1 ¢ $ we find the last send event on ¥, identify the corresponding receive and check whether it is on ¢ and there are no send events on ¢ after it. This can be done in time ¡ £ © ! ©¦ . Then we run from (1 the modified version of the depth-first search described above. For any ( 2 discovered during this search and for each receive event of ¥ 2 ¦ & £ ( 2 ¦ , we check if it is not reachable from any event of ¥ or ¢ using the precomputed information.

For each triple £¥ ¥ ¢ ¥ ( ¦ , we traverse each edge of ' at most twice, and do a constant- time computation for each event of !. Hence, the computation that has to be done for each triple £¥ ¥ ¢ ¥ ( ¦ takes ¡ £ © ! ©¦ steps, and the total running time of our algorithm is ¡ £ © § ©© ! © ¡ ¥ ¦ © £ ¤ ¦ , ¢ ¦ © £ £ ¡¦ . Let ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ be the HMSC obtained by deleting from ! all nodes other than ( and (¦ that have send events on ¥ or receive events on ¢. Output "yes" if the following six conditions hold:

(1) we have ¥ ¥ ¦ ¢, ¢ ¥ ¦ © £ £ ¦ , ¥ ¥ ¦ © £ ¤¡ ¦ ;

(2) in ¥ there are no send events on ¥ after ¤ ;

(3) in ¥ ¦ there are no receive events on ¢ before £ ¡ ; (4) in ¥ there is no chain from £ to any event of ¢;

(5) in ¥ ¦ there is no chain from any event of ¥ to ¤¡ ;

(6) the HMSC ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ contains a path from ( to (¦ . Suppose that for some ( ¥ (¦ ¢ $ , ¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ the conditions (1)-( 6) are all true. By ( 6), there exists a path 5 ¦ £ ( ¦ ( ¥ ¥ ( ¦ (¦ ¦ in ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ . Set & £ ( ¦ ¦ ¥, & £ (¦ ¦ ¦ ¥ ¦ , ¥ ¥ ¦ & £ ( ¡ ¥ ¥ ( ¤ ¦ . Suppose that & £5 ¦ contains a chain from £ to £ ¡ . As ¢ ¥ ¦ © £ £ ¦¥ ¥, this chain must contain a receive event on ¢. By (3), there is no such event in ¥ ¦ , and by construction of ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ , there can be no such event in ¥ ¥. Finally, by [START_REF] Ben-Abdallah | Syntactic Detection of Process Divergence and Non-local Choice in Message Sequence Charts[END_REF] there is no such event in ¥. Hence, in & £5 ¦ there is no chain from £ to £ ¡ . Similarly, a chain from ¤ to ¤¡ must contain a send event on ¥, and there is no such event in ¥ (by ( 2)), ¥ ¦ (by ( 5)), or ¥ ¥ (by construction of ! £ ( ¥ (¦ ¥ ¥ ¥ ¢ ¦ ). Hence, the pair £ ¤ ¥ ¤ ¡¦ provides a witness that § © ¨£! ¦ ¦ ¤ . Conversely, by the reasoning above, if for some pair £ ¤ ¥ ¤ ¡¦ we have ¨© ¨ £ ¤ ¥ ¤ ¡¦ ¦ ¤ , then our algorithm succeeds. As in the previous case, this algorithm can be implemented in time ¡ £ © ! © ¢ ¦ or, by changing the order of operations, in ¡ £ © § © ¡ © ! © ¡ ¦ .

Conclusions

We proposed using Allen's logic for detecting and measuring message order discrepancy in HMSCs. We believe that Allen's logic can be a versatile tool for other message order-related problems in MSCs and HMSCs, such as, e.g., race conditions and message overtake. Allen's logic is very well studied from algorithmic perspective [START_REF] Krokhin | Reasoning about Temporal Relations: The Tractable Subalgebras of Allen's Interval Algebra[END_REF]; while in this paper we did not use these results, they may be very useful for other applications of Allen's logic for message order analysis. We introduced the notion of discord, which measures the difference between the message order in an HMSC and the "ideal" message order for that HMSC. We have shown a coNP-hardness result for computing the discord of a pair of messages in an HMSC, as well as polynomial-time algorithms for restricted versions of this problem. In contrast, we showed how to find the worst-case discord of an HMSC in polynomial time. We believe that the concept of discord will be useful in avoiding design errors in HMSCs. In particular, it can be applied when one wants to partition a large HMSC into smaller components: one should prefer partitions with small discord. Another potential application of this work is in the area of MSC-based programming approaches, such as, e.g., the "play-in, play-out" framework of [START_REF] Harel | Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine[END_REF], which assumes synchronous MSC concatenation. Calculating discords allows one to quantify the potential for relaxing the synchronization assumption and check for possible hazards. This may increase concurrency and efficiency of the implementation and thus can be useful in protocol design.

Fig. 1 .

 1 Fig. 1. An HMSC

Fig. 4 .

 4 Fig. 4. The possible orders between messages (up to symmetry)

1 ,

 1 and finally there is an edge from

Fig. 5 .

 5 Fig. 5. The high-level structure of the HMSC used in the proof of Theorem 1.

Fig. 6 .

 6 Fig. 6. (a) The gadget ¡; (b) The gadget ¢ £

Fig. 8 .

 8 Fig. 8. The implementation of ComputeY()

  For each such pair, conditions (1)-(3) can be verified in time ¡ £ © ! ©¦ assuming that the relation for & £ (¦ ¦ has been precomputed (by Corollary 1, we can precompute for all MSCs that appear in ! in time ¡ £ © ! © ¡ ¦ ). Condition (4) corresponds to solving a single instance of reachability problem, so it can be checked in time ¡ £ © ! ©¦ as well.

  there is a path 5 from ( to (1 such that in & £5 ¦ none of the processes in £ is reachable from £ and none of the processes in £ ¦ is reachable from ¤ . It is straightforward to modify ComputeY() so that it computes ¦ £ £ ¥ £ ¦ ¥ ¤ ¦ instead of £ £ ¥ ¤ ¦ . The running time of

	the modified version is subsets of § in adjacent nodes. ¡ £¥ ©' © 6 £¤ ¤	© § © ¡ ¦ , as we have to consider all possible pairs of
	Now, suppose that we have computed ¦

  ¢£¤¥ ¦ ¡ §¨© £ We will show that § © ¨£! ¦ ¦ £ if and only if for any £ ( ¥ (¦ ¦ ¢ ' and any¤ ¢ & £ ( ¦ , ¤ ¡ ¢ & £ (¦ ¦ we have ¨© ¨¢¡¢ ¤ ¡¢ ¤¤¤ £ ¤ ¥ ¤ ¡¦ ¦ £ .Indeed, if for some such ¤ ¥ ¤ ¡ we have ¨© ¨¢¡¢ ¤ ¡¢ ¤¤¤ £ ¤ ¥ ¤ ¡¦ ¥

	viously § © ¨£! ¦ ¥ ¦ £ . Conversely, consider any pair of messages	¦ £ , then ob-

Acknowledgements

Part of this work was done when the fourth author was visiting Bar Ilan University and the first author was a Lady Davis Fellow at Hebrew University of Jerusalem. This research is partially supported by the ESF project Automatha, the ANR project DOTS, and an NRF Research Fellowship.


Thomas Ulrich

Caterina Negulescu

Evelyne Foerster

Hormoz Modaressi

Samuel Auclair

Comparison of different numerical methodologies to derive

Keywords: SSI, fragility curves, inter-story drift. 1

  L'archive ouverte pluridisciplinaire

INTRODUCTION

The interaction between the structure and the soil during the dynamic loading is named soil-structure interaction (SSI). Two mechanisms of interaction take place between the structure, foundation and soil: 1) inertial interaction, developed in the structure due to its own vibrations gives rise to base shear and moment, which in turn cause displacements of the foundation relative to free-field and 2) kinematic interaction, explained by the presence of stiff foundation elements on or in soil that cause foundation motions to deviate from free-field motion as a results of ground motion incoherence, wave inclination, or foundation embedment [START_REF] Stewart | Seismic soilstructure interaction in buildings. I: Analytical methods[END_REF]. Inertial effects can be described by frequency dependent foundation impedance functions expressed by a complex number: its real part is related to the rigidity and its imaginary part to the damping capacity. The effective damping is a summation of two sources: radiation damping (transmitted by the structure to the soil) and hysteretic damping of the soil. The impedance can be represented by a Kelvin Voigt Model composed of a viscous dashpot and a spring connected in parallel. There are different techniques and software to evaluate the SSI response. Generally, for these studies the soil and the structure are computed in the same model. Anyway, some studies shows that when the slab may be assumed rigid, the soil spring techniques appears sufficient compared to more sophisticated techniques such as the SASSI code [START_REF] Nien | Soil-Structure Interaction Effects on Seismic Response of ISFSI Slabs[END_REF]. In this study both technique are tested to calculate the SSI response.

MODEL DESCRIPTION AND ANALYSIS

Two different approaches to the SSI phenomenon have been considered. Figure 1 presents a simplified representation of each model: 1) the two-step approach -soil analysis using CyberQuake program [START_REF] Foerster | Nonlinear numerical method for earthquake site response analysis II-case studies[END_REF]) and structure analysis using Seismostruct program (SeismoSoft, 2003) and 2) the one-step approach -soil and building in the same model using Gefdyn software. The different colours of the accelerograms indicate its changes. Orléans Cedex 2, France email: t.ulrich@brgm.fr, c.negulescu@brgm.fr, e.foerster@ brgm.fr, h.modaressi@ brgm.fr, s.auclair@ brgm.fr. During Phase 2, we estimate the building behavior under the seismic loading. The target buildings are analyzed twice: first considering rigid base conditions (encasing link) and second considering a movement between the structure and the soil (springs and dashpots link). In this study, two RC buildings with natural periods of vibrations equal to 0.1s and 0.5s were analyzed. A very rigid basement system having 2m depth is considered for each structure. The motion resulting from the Phase 1 is the free-field motion. This motion is different from the motion under the foundation. The input motion for the Phase 2 is the motion under the foundation system. This motion is obtained by applying an empirical adjustment factor to the free-field motion. This adjustment factor results from investigations of the observed records at free-field and at foundation level during the 1995 Hygoken Nanbu Earthquake [START_REF] Yasui | Relationship between Building Damage and Strong Motion Records -Soil-Building Interaction[END_REF]AIJ, 2004) and from the results of analysis performed to investigate the characteristics of input motions on frequency (IAEA, 2003; AIJ, 2004).

Comparison of different numerical methodologies to derive fragility curves of RC buildings with soil-structure interactions

One-step analysis

SSI is also investigated in a unified approach, with the finite element software Gefdyn. In such analyses, the wave propagation from bedrock through the soil layers to the top of the structure is modeled in one step. Contrary to the two-step analysis, soil layers are modeled within a 2D mesh (quadrangle elements) and the structure is represented by simple spring-mass models, whose characteristics have been adjusted to fit with the linear behavior of the Seismostruct structures. Figure 2 presents the geometry used in the analyses:

Figure 2. Geometry of the model.

We assume that the incident wave propagates vertically, so that the mesh is very much refined in that direction to avoid numerical dispersion (25 nodes per wave length λ for a maximum frequency of 20 Hz). Moreover, the soil right beneath the structure, up to 5m away from it, is finely meshed to catch the soil-structure effects more accurately (25 nodes per λ). Then, up to 20m away, the soil is less finely meshed (10 nodes per λ), and finally the soil stretches up to 150m away from the building with a very coarse mesh, to avoid spurious boundary condition effects. This decreasing pattern in the mesh permits to save computational time. Equivalent boundaries conditions are imposed on the vertical boundaries to prevent the incident wave to distort near the boundaries.

As no non-linear effects are considered in these analyses, the impulsional response of the model is computed and is then convoluted with the bedrock accelerograms to compute the inter-storey drift (ISD).

Building description

Regarding the two-step approach, two 3D RC buildings with 1 and 5 stories respectively, are defined for dynamic timehistory analyses. The height floor is 3m. The basement is considered a technical one having 2m height. The foundation is continuous on the building contour and is rigidified by truss elements. The rigidity of the truss elements is calibrated in order to have the same natural period of vibration as for the structure without basement. For each model, the very regular structure consists of 2 spans and 2 bays of 4m each. Cross sections of the columns are rectangular (55 x 55 cm for the 0.1s model and 40 x 30 cm for the 0.5s one).the beams have constant sections: 50 x 35 cm for 0.1s model and 50 x 20 cm for 0.5s model. Buildings' properties are presented in Table 1. The 0.1s model is designed in order to be about 100 times stiffer than the 0.5s model. The frames are made of cast in place reinforced concrete having concrete strength fc=30MPa, Young's modulus for the concrete was taken equal to 27,500MPa. The reinforcement yielding stress is fy=500MPa. Both structures are modelled with Seismostruct software. The beams and columns are inelastic frame elements capable to take into consideration geometrical and material nonlinearities. The sectional stress-strain state of beamcolumn elements is obtained through the integration of the nonlinear uniaxial material response of the individual fibres in which the section has been subdivided, fully accounting for the spread of inelasticity along the member length and across the section depth. The structures have been constructed to have the natural period of vibration 0.1 times the stories number, namely 0.1 and 0.5 seconds.

Figure 3. Models for non-linear time history analysis (twostep approach)

For rigid base analysis all the base nods have encasing link while for the SSI analysis the flexible link (permitting rotation and translation) are used, as presented in Figure 3. The properties of the link elements (rigidity and damping) are calculated using empirical relationship presented in the next paragraph.

Table 1. Properties of the building models

Impedance matrix

The impedance matrix can be conceptually viewed as an assemblage of springs and dashpots [START_REF] Pecker | Soil Structure Interaction. Advanced Earthquake Engineering Analysis[END_REF]. The expressions for stiffness and damping of equivalent springs for rigid foundation on a stratum over rigid bedrock (IAEA, 2003) are presented for various degrees of freedom:

⎟ ⎠ ⎞ ⎜ ⎝ ⎛ + - = h R GR K S 2 1 1 2 8 ν , h/R>1, horizontal direction of motion (1) ⎟ ⎠ ⎞ ⎜ ⎝ ⎛ + - = h R GR K R 6 1 1 ) 1 ( 3 8 3 ν , 4>h/R>1, rocking direction of motion (2) ⎟ ⎠ ⎞ ⎜ ⎝ ⎛ + - = h R GR K V 28 . 1 1 1 4 ν , h/R>2, vertical direction of motion ( 3
)
where h is the substratum thickness; R, an equivalent radius for a rectangular foundation; G and ν, respectively the shear modulus and Poisson's ratio of the soil. For each foundation motion, the reduced radiation damping factor of a soil is calculated from the damping coefficient determined using the above relationships:

G R K C C H S / 1 ρ = , horizontal equivalent damping coefficient (4) G R K C C R R / 2 ρ = , rocking equivalent damping coefficient (5) G R K C C V V
K C SSI 2 5 . 0 = ξ (7)
where C and K are the damping and stiffness coefficients respectively. The 0.5 factor is intended to take into account the fact that the actual radiation damping is less than that for a 'regular' half-space, due to wave's reflection in horizontal soil layers. The overall soil damping factor is obtained as:

ξ S = ξ g + ξ SSI ( 8
)
where ξ g is the hysteretic soil damping. This value is limited to 30%.

Adjustment factor

The dynamic soil-structure interaction effect can be considered by the means of the adjustment factor H SSI (ω) (AIJ, 2004), which is defined as follows:

1 , 2 1 1 ) ( 2 2 2 < + = = d d GL fh SSI U U H δ ηδ ω and 1 , 2 1 1 ) ( 2 2 ≥ + = = d GL fh SSI U U H δ η ω (9)
where η =d/l;

d d ω ω δ / = ; ( ) d V s d 2 / ) (π ω =
, and l is the foundation width; d, the foundation embedment depth; U fh , the foundation motion; U GL , the free field motion; Vs, the shear wave velocity of the soil adjacent to the side wall. Figure 4 presents the adjustment factor for the embedded foundation and for three layers having shear wave velocities of 100, 200 and 300 m/s respectively. The adjustment factor is multiplied by the free-field motion in order to obtain motion under the foundation. The motion under the foundation is then used as input motion in the SSI dynamic time histories analyses of the structure performed with Seismostruct.

Input motions for dynamic analyses

A total number of 246 strong-motions were used for performing dynamic analyses. The histogram of the PGA values is presented in Figure 5. As the structural modeling was faster for the one-step approach, a larger number of calculations were performed in this case. In total, we used 246 strong-motion records as input to time-history analyses for the one-step approach and 108 only for the two-step one.

Fragility curves derivation

The fragility curves are used to represent the probability that a given damage level is reached (or exceeded) for any given level of ground motion characterized by PGA (intensity) value. For each simulation performed (one or twostep and rigid base or SSI), the highest inter-storey drift ratio (ISDR) was extracted as the structure response to the seismic input. An advantage of using the ISDR to evaluate the damage level of a building is that this variable is fairly intuitive and was widely used in previous studies.

The fragility curves are based on the analytical work of Shinozuka et al., 2000 [11], who expresses the fragility curve in the form of a two-parameter lognormal distribution function. The two parameters of the distribution represent the median and the lognormal standard deviation and are computed so as to maximize the likelihood function (Gehl et al., 2009 [3]). Figure 6 presents the results obtained for the 0.1s model considering one of the strong-motion records and the two-step approach. For each substratum thickness h, we plot the Rigid base response in red and the SSI ones in blue (Vs equal to 100 m/s), pink (Vs=200 m/s) and orange (Vs=300 m/s). On this figure, we note that due to SSI effects, the natural period changes from 0.1s (Rigid base condition) to 0.22sfor Vs=100 m/s. This change in natural period almost vanishes with the increasing shear wave velocity: 0.2s for 100m/s, 0.14s for 200m/s and 0.12s for 300m/s. This trend is more visible on the 5m-thick soil profile than on the 10m-thick one. Here, the SSI effect is well explained by the properties of the structures (very big mass and rigidity) and of the soil profile (low share wave velocity).

Figure 7 shows the period modification of the structure considering SSI effect for the 0.5s model and two-step approach. In this case the changes in the natural periods are less visible for the soil profile with different shear wave velocities and even for the different thicknesses. the results of these investigations (Figure 8) confirm globally the conclusion drawn for the first model (Seismostruct).

Figure 8. Influence of SSI on the drift of the 5 story building (spectral intensity, computed from the one-step approach).

In fact, the fundamental frequency of the system {soil, structure} is lower when the soil is softer. The results of the simulations with a 10m-thick soil are quite similar with those of 5m-thick soil, but the effect of the SSI seems a little bit stronger in the 1 st case, contrary to the observations made on the first model. Globally, SSI effects seem to be more predominant in the one-step approach, if we look at the changes in the fundamental frequency observed easily even for the 5 story building. Finally, the observed difference between heights of the intensity peaks is mainly due to the damping produced by SSI, which is greater when Vs increases.

For the 0.1s model, the fragility curves developed when considering SSI effects show damage amplification for both type of approaches (one-step and two-step). This phenomenon is explained by the rocking movement that the SSI phenomenon induces to the structure. In this case, the interstory drift parameter is not adequate for measuring the damage of the building unless the component displacement corresponding to the rocking is extracted from the total displacement obtained at the top of the building. The displacement corresponding to the rocking movement is related to the increase in the rigid movement that does not influence the damage of the structure, but increases the total top displacement of the structure hence the inter-storey drift.

For the 0.5s model, the rocking component of the motion is less important and the inter-storey drift has been used for calculating the fragility curves for both one-step and two-step approaches.

Figures 9 and 10 show the fragility curves obtained for the 0.5s model with two-step and one-step approaches respectively. For the two-step approach, we note that the SSI effect reduces the probability of damage occurrence for PGA values superior to 8 m/s 2 . In the one-step case, the SSI effect reduces the probability of damage occurrence. In Figure 11, we compare the curves obtained by one-step and two-step approaches. The results obtained from dynamic time histories in terms of transfer functions show a good match with the SSI period calculated using empirical relation. For the 0.1s model, the change in the rigid base period due to the SSI effect is obvious. It's difficult to draw general conclusions about the influence of the soil foundation thickness on the fundamental period of the structure from the 2 configurations analysed in this study (5m and 10m). However, previous researches [START_REF] Negulescu | Effect of Soil Structure Interaction on the dynamic response of the building, 14ECEE[END_REF] have shown that the SSI effect diminishes with the increasing soil thickness h. The amplitude of the Fourier spectral ratio decreases with increasing h. If considering only frequency content, there is no concrete evidence of SSI effects for the 0.5 models when performing a two-step analysis.

Regarding fragility curves for the 0.1s model for both onestep and two-step approaches, the SSI effect increases the probability of observing damage. However, this result is not realistic and can be explained by the fact that ISD parameter is not adequate for measuring the damage of the building. Indeed, part of the displacement at the top of the building is produced by a rigid body movement that does not affect the damage of the structure. We must also note that linear assumption for soil behavior under such a building is not realistic: the role of confinement pressure due to the building heavy weight for soils right underneath cannot be neglected. Consequently, the soft soil under such a structure may exhibit nonlinear behaviour. . As a consequence, plastic yielding and damping effects may result from the rocking of the structure, which will decrease the importance of this movement.

For the 0.5s structure and the Gefdyn model (one-step approach), the SSI effects decrease the probability of damage occurrence. For the Seismostruct model, the SSI effects diminish the probability of damage occurrence for PGA superior to 8m/s 2 and increase it otherwise.

Generally the resulting damages are less important for twostep analyses because of the nonlinear behavior considered for the structure that tends to reduce the drift (due to material damping). For the one-step approach, the structure behavior is assumed to be linear.

Figure 1 .

 1 Figure 1. One-step and two-step SSI analysis

  =0.5; C 2 =0.3/(1-B φ ); B φ = the soil bulk density and I 0 , the mass moment of inertia.

Figure 4 .

 4 Figure 4. Adjustment factor (FA) of the embedded foundation for three soil conditions: Vs=100, 200 and 300m/s

Figure 5 .

 5 Figure 5. Histogram of the PGA (m/s 2 ) values for the timehistories used for dynamic analyses

  considered in this study to assess SSI effects are: 1) computation with rigid base hypothesis, 2) computation considering SSI for different combinations of soil profile and structure, and 3) evaluation of SSI effects. Generally, the following parameters were analyzed: a) fundamental frequency of the structure, b) PGA at base and top of the structure, c) Spectral Acceleration SA(T) at base and top of the structure, d) Structure's transfer function with regard to input's frequency content, e) Displacement at base and top of the structure, f) Bending moments and forces in structure's elements, etc. The obtained results are commented first considering the frequency changes of the models and second, considering the fragility curves developed for rigid base and SSI cases and by both one-step and two-step approaches. For frequency domain analyses, the result that seems to be more explicit and that is presented in the following figures is the transfer function between the top and the base of the structure. The figures of the earthquake records are processed using Viewwave software coded by T. Kashima (2005, Building Research Institute, Tsukuba, Japan).

Figure 6 .Figure 7 .

 67 Figure 6. Spectral Ratios computed between top and base of the 0.1s model for three soil conditions (Vs=100, 200 and 300 m/s) and two soil thicknesses (h=5m and 10m)

Figure 9 .Figure 10 .Figure 11 .

 91011 Figure 9. Fragility curves for 5 story buildings developed using two-step approach

  T. Ulrich 1 ,C. Negulescu 1 , E. Foerster 1 , H. Modaressi 1 , S. Auclair 1 1 BRGM (French Geological Survey), Natural Risks and CO2 Storage Safety Division, 3 Avenue Claude Guillemin, 45060

ACKNOWLEDGMENTS

This work was supported by the brgm research department under grant RISR17-VULNERISC.


Akos Banyasz

Ignacio Vayá

Pascale Changenet-Barret

Thomas Gustavsson

Thierry Douki

Dimitra Markovitsi
email: dimitra.markovitsi@cea.fr

Base-pairing enhances fluorescence and favors cyclobutane dimer formation induced upon absorption of UVA radiation by DNA

The photochemical properties of the DNA duplex (dA)20•(dT)20 are compared with those of the parent single strands. It is shown that base-pairing increases the probability of absorbing UVA photons, probably due to the formation of charge transfer states. UVA excitation induces fluorescence peaking at ca. 420 nm and decaying on the nanosecond time-scale. The fluorescence quantum yield, the fluorescence lifetime and the quantum yield for cyclobutane dimer formation increase upon base-pairing. Such behavior contrasts with that of the UVC-induced processes.

The knowledge that absorption of UV radiation by DNA induces carcinogenic mutations has triggered numerous studies aiming at the characterization of its electronic excited states and their relaxation dynamics. 1,2 All these investigations consider UVC or UVB excitation but their UVA counterpart has not yet been addressed. This is due to the fact that individual DNA bases do not absorb UVA radiation. However, a few studies have shown that this is not true for duplexes which indeed present a weak absorption tail above 300 nm. 3,4 Moreover, it has been pointed out that absorption of UVA radiation by natural isolated and genomic DNA and by the synthetic duplex (dA) 20 •(dT) 20 leads to the formation of the highly mutagenic cyclobutane pyrimidine dimers (CPDs). 4,5 This is an important issue because UVA photons are much more abundant than those of UVC or UVB in the solar radiation reaching the surface of the Earth. 6 Here we report the first fluorescence study with UVA excitation performed for (dA) 20 •(dT) 20 and the parent single strands (dA) 20 and (dT) 20 . We also determine the quantum yields for CPD formation for which no information was available so far regarding the UVA range. We show that base-pairing enhances fluorescence and favors CPD formation which contrasts with the effect of UVC irradiation.

The DNA strands dissolved in phosphate buffer (0.1 M NaH 2 PO 4 , 0.1 M Na 2 HPO 4 and 0.25 M NaCl) were studied at room temperature. Strand concentrations ranging from 3x10 -6 M to 10 -4 M were used. In order to rule out that the UVA-induced fluorescence and CPDs are not related to impurities we performed a series of control experiments described in detail in the supporting information. Briefly, we tested nucleic acids from different suppliers, different purification methods and different types of added salts. Fluorescence decays were obtained by time-correlated single photon counting (TCSPC). The excitation source was the second (365 nm) or the third (267 nm) harmonic of a tunable Ti-sapphire laser (120 fs fwhm at 800 nm). Irradiations were carried out using the Xenon arc lamp of a Fluorolog-3 spectrofluorimeter (SPEX, Jobin-Yvon). Formation of thymine dimers was monitored by high performance liquid chromatography coupled to mass spectrometry. Comparison of the absorption spectra of (dT)20 (blue) and (dA)20 (green) with the corresponding monomeric chromophores (black) dT and dA (a and b) on the one hand, and the spectrum of the duplex (dA)20•(dT)20 (red) with that corresponding to the sum of the (dT)20 and (dA)20 spectrum (brown, c), on the other. The molar absorption coefficient  is given per base. In violet: a typical solar spectrum. 6 The absorption spectra of the single strands (dT) 20 and (dA) 20 , (Figures 1a and1b), exhibit a weak long wavelength tail which extends all over the whole UVA region and is absent from the spectra of the corresponding monomeric chromophores, thymidine (dT) and 2'-deoxyadenosine (dA), respectively. The molar absorption coefficient per base determined for the duplex in the UVA spectral domain is higher than that corresponding to the sum of the parent single strands (Figure 1c). These findings clearly show that the UVA absorption arises from interchromophore interactions which are expected to increase in the order: (dT) 20 , (dA) 20 and (dA) 20 •(dT) 20 as a result of a better chromophore organization and reduced conformational motions. Electronic coupling between dipolar * transitions of the DNA bases is known to give rise to exciton states whose properties differ from those of single chromophores. 7 The strength of the dipolar coupling for stacked or paired bases does not exceed a few hundreds of wavenumbers. 8 Consequently, it is very unlikely that Frenkel excitons are encountered at such low energies. Furthermore, n* states, which have the lowest energy for DNA bases in the gas phase, are expected to be strongly destabilized in the presence of water molecules. 1 In contrast, the occurrence of charge transfer (CT) states in the UVA region is quite plausible. Several theoretical studies dealing with small double-stranded structures have reported the existence of CT states, involving bases located either in the same or in different strands, but positioned the related transitions at shorter wavelengths. 9,10 However, CT states can be strongly stabilized in aqueous solution. They are very sensitive to conformational and environmental factors which may modulate their energy and thus spread the corresponding transitions over a larger spectral range. 10 The emission maxima of all the examined oligonucleotides obtained upon UVA excitation range between 415 and 430 nm (Figure 2 and Table 1). Interestingly, similar bands have been observed upon UVC excitation of the alternating duplex (dAdT) 10 •(dAdT) 10 and the adenine dinucleotide; they were attributed to exciplex/excimer emission. 11 They are not altered when the solutions are saturated by nitrogen or oxygen, precluding any emission from triplet states.

The overlap between the UVA-and UVC-induced fluorescence spectra suggests that the excited states emitting at ca. 420 nm could be populated indirectly during the relaxation of * excited states. However, in the latter case, other deactivation routes are dominant, as shown by the fluorescence quantum yields. Those determined upon UVA excitation for the single strands are about ten times higher than their UVC counterpart whereas, in the case of the duplex, the difference amounts nearly to two orders of magnitude (Table 1). In the case of UVA excitation, base pairing enhances fluorescence emission which does not happen for UVC excitation. The UVA-induced fluorescence decays on the nanosecond time scale and is strongly non-exponential. Fits with fourexponential functions (supporting information) allowed us to determine the average fluorescence lifetimes < fl > and estimate the average radiative lifetimes < rad > (Table 1). The < rad > values range from 66 to 320 ns, corresponding to weakly allowed electronic transitions, in line with what is expected for CT excited states. Yet, the < rad > values decrease successively when going from (dT) 20 to (dA) 20 , and further to (dA) 20 •(dT) 20 . This indicates that the greater the structural order the more allowed the electronic transitions related to the emission. We recall that we observed the same trend for the Franck-Condon transitions (Figure 1), which indicates a correlation between the excited states corresponding to photon absorption and photon emission.

The < rad > values determined for (dT) 20 and (dA) 20 •(dT) 20 upon UVC excitation amounts to only a few ns, as expected for emission dominated by allowed * transitions. A much higher < rad > value is found for the UVC induced fluorescence of (dA) 20 which has been attributed to excimers. [START_REF] Kwok | [END_REF] Focusing on (dT) 20 and (dA) 20 •(dT) 20 , in which thymine dimers can be formed, we compare the reaction products induced by UVA and UVC irradiation. As was previously reported for UVA irradiation of (dA) 20 •(dT) 20 , isolated genomic and cellular DNA, 4 only CPDs are detected also in the case of (dT) 20 . Neither (6-4) adducts nor Dewar valence isomers are found. The quantum yields of the UVA-induced CPDs are much lower than those determined following UVC irradiation 13 (Table 1). Despite their low values they are easily detectable by the analytical tools used to this end (supporting information). Taking into account the sensitivity of our measurements, we estimate that the quantum yield for the formation of (6-4) adducts is lower than 10 -7 .

A striking difference between UVC-and UVA-induced CPD formation is that, in the former case, base-pairing results in a twofold decrease of the quantum yield 13 whereas in the latter, the quantum yield increases nearly by one order of magnitude. The UVA case is surprising since, in principle, part of the absorbed UVA photons populate excited states located on adenines. Such an effect, together with the absence of other dimeric photoproducts, proves that UVA induction of CPDs occurs via a different mechanism than in the case of UVC. Theoretical calculations have shown that CPD formation induced by UVC radiation in (dT) 20 and (dA) 20 •(dT) 20 , which populates * states, is governed by the ground state geometry. 13 In the case of UVA, the excited state relaxation obviously plays a crucial role. However, even in this case, the ground state geometry could be involved in an indirect way because it determines the conformations that give rise to UVA absorption.

We hope that the results presented here will inspire further experimental and theoretical work which will provide a detailed mechanism describing the UVA-induced reactivity of DNA. In particular, it would be interesting to explore the possible interconversion between CT and * states, already reported for stacked adenines, 14 in the case of double stranded structures.

Table 1. Effect of UVA and UVC radiation on the properties of the emitting excited states and the reaction products determined for (dT) 20 and (dA) 20 and (dA) 20 •(dT) 20 , noted as T, A and A:T, respectively. fl,max: maximum of the fluorescence spectrum; fl: fluorescence quantum yield; <fl>: average fluorescence lifetime; <rad>: average radiative lifetime; CPD: quantum yield for CPD formation; (6-4): quantum yield for the formation of (6-4) adducts; a) exc: 330 nm; b) exc: 255 nm; c) exc: 365 nm; d) exc: 267 nm; e) from ref. 15 ; f) exc: 335 and 354 nm.

Table of Contents artwork

1 Figure 1 .

 11 Figure 1.Comparison of the absorption spectra of (dT)20 (blue) and (dA)20 (green) with the corresponding monomeric chromophores (black) dT and dA (a and b) on the one hand, and the spectrum of the duplex (dA)20•(dT)20 (red) with that corresponding to the sum of the (dT)20 and (dA)20 spectrum (brown, c), on the other. The molar absorption coefficient  is given per base. In violet: a typical solar spectrum.6

Figure 2 .

 2 Figure 2. UVA-induced fluorescence properties of (dT)20 (a, b; blue), (dA)20 (c, d; green) and (dA)20•(dT)20 (e, f; red). Normalized fluorescence spectra (a, c, e; excitation wavelength: 330 nm) and fluorescence decays (b, d, f; excitation wavelength: 365 nm). The corresponding properties induced by UVC excitation (267 nm) are shown in black. Arrows denote the emission wavelength at which the decays were recorded.

Acknowledgment

We thank Mrs Sz. Karpati and M. Perron for their help, Dr R. Improta for helpful discussions and the French