CONCUR 2004 – Concurrency Theory- P5: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 106 N. Baudru and R. Morin Fig. 7. Netchart Ni and some non-FIFO behaviour N 0 Cfifo N Definition . The MSC language fifo M is the set of FIFO basic MSCs obtained from an MSC of its low-level Petri net by the labelling flfo N We stress here that tt maps FIFO basic MSCs onto FIFO basic MSCs. The situation with non-FIFO basic MSCs may be more complicated as we will see in the last section. 3 Netcharts vs. Implementable Languages In this section we study how netcharts relate to communicating systems. We consider the set of channels K. that consists of all triples i j x el xl x A A channel state is then formalized by a map x JC N that describes the queues of messages within the channels at some stage of an execution. The empty channel state xo is such that each channel maps to 0. Definition . A message passing automaton MPA S over A consists of a family of local components Af ieI and a subset of global final states F such that eachcomponent Ai is a transition system Qi u i over where Qi is a finite set of z-local states with initial state ii e Qi iQ Qi x x Qi is the z-local transition relation and F C x ixo - Semantics of MPA A global state is a pair s x where s e IJiei 2 is a tuple of local states and x is a channel state. The initial global state is the pair z s x such that s ii ieI and x xo is the empty channel state. The system of global states associated to S is the transition system As Q z over S where Q Jliei Qi x is the set of global states and the global transition relation Q x S x Q satisfies m - for all i j m e K qk k iI X - q Oc if 1. qi i q i and q k qk for all k e I z 2. x fif m x fih 1 and x x x for all x e 0 z j m - for all i j m e K qk keI x q x if 1. qj q j and qk qk for all k e 1 J 2. x i j m 1 x Am and x x x x for all x e K. i j m . Please purchase PDF Split-Merge on to remove this watermark The Pros and Cons of Netcharts 107 As usual with transition systems for any u c we write q q if there are some global .
