In [Cza 2006] x-point equations specifying synchronous ("hand-shaking") communication in distributed systems have been proposed. Their solution yielded a communication network of agents, directly presented as a Petri net-like structure, and determined the global state of the speci ed system. The net-places represented agents, while transitions - transfer of messages. A special algebra being a semi-ring with "addition" (nondeterministic choice) and "multiplication" (simultaneity) was a formal basis for the equations and their solving procedure. Here, the equations are modi ed to specify asynchronous communication, that is, such that the senders, after sending message, continue their performance without waiting for reception. This required introducing a new type of objects called bu ers or mailboxes - apart from the agents (senders/receivers), and changing the semi-ring into a distributive lattice of the agents and mailboxes. In the asynchronous communication, solution to the x-point equations should determine that: (1) the sender can send message as soon as mailboxes of its simultaneous receivers can store the message, no matter whether the receivers are ready to get it or not. (2) in the resulting net, the mailboxes are included as net-places too, each one collecting messages from its senders (possibly a number of senders) and transferring them to its (exactly one) receiver for which it is the unique mailbox. The proposed modelling of communication takes some (but only some!) ideas from CSP [Hoa 1978, 1985], CCS [Mil 1980, 1989] (e.g. a concept of agents, ports, synchronization between senders and mailboxes or its absence: no synchronization between senders and receivers, communication media or channels), Petri nets [Rei 1985] (e.g. graphical presentation of solution to the communication equations) or practice of computer networks and distributed systems [C-D-K 2005] (e.g. multicasting and broadcasting,
blocking/non-blocking, connection-oriented/connectionless communication mode). The communication equations may be treated as specifying interconnection system among agents, while net-structures resulted from their solution - as "implementation" of this system. The correctness of such implementation is ensured by identity of each group of receivers from a given sender (and, symmetrically, of each group of senders to a given receiver), both in speci cation and implementation. 2
(1) A semiring of terms Let X be a set of atomic arguments partitioned into the set C of constants and the set V of variables: X = C[V, C\V = ;. Each x 2 X is a term; if K and L are terms then strings (K + L) and (K L) are too, called a sum and product. We say \terms over X", their set T[X]. Addition and multiplication of terms is de ned as follows: K L = (K + L); K L = (K L), but + and are used for and . It is required that the system (T[X]; +; ) obeys the following axioms for all K; L; M 2 T[X] : (i) (ii) (iii) (iv) (v) (vi) (vii)
K + K = K K + L = L + K K + (L + M ) = (K + L) + M K L = L K K (L M ) = (K L) M K (L + M ) = K L + K K 2 X ) K K = K
M By assuming that binds stronger than + and by (iii) and (v), some parentheses may be dropped. Two terms are equal (=) i one may be transformed into the other by means of the axioms. A partial order (v) between terms is de ned as K v L i L = L + K. If a term K is composed of atoms x; y; :::; z at the most, we write K(x; y; :::; z). That is, some of them may be absent in K. A power of K is de ned by K1 = K, Kn+1 = K Kn. This algebra enjoys the properties: (a) Each term may be transformed by means of equations (i) (vii) to a sum of products of arguments and then simpli ed. Such form is called canonical (b) If n m then Kn v Km. (2) A distributive lattice of terms over constants For the lattice the same operators + and are used, thus, the algebraic system (T[C]; +; ) of terms with constants only is required to obey axioms (i) (vii) and additionally for K; L 2 T[C]: (viii)
K
L + K = K This algebra enjoys the following: (c) If K = K1 +K2 +:::+Kn where Ki 2 T[X], is a product of arguments, then Kn = Kn+j for j 0. In particular, for any term K there exists a number n such that Kn = Kn+j for j 0: De ne a maximal power of K as p(K) = min(nj 8j 0 : Kn = Kn+j ). For instance, the maximal power of a x + b with a; b 2 C; x 2 V is 2 since (a x + b)2 = a x + a b x + b, (b a + c)2 = (b a + c)2+j for j 0, and a x + b 6= (a x + b)2. Note that if K 2 T[C] then p(K) = 1. (d ) There exist solutions to equation x = K x + L and their general form is x = Kp(K) (L + P ) + L, where p(K) is the maximal power of K and P is arbitrary term not containing x. In particular, general form of solution to equation x = K x is x = Kp(K) P .
Interpretations: In Section 3 constants will play part of agents represented by places in nets obtained as solutions to the speci cation equations, while some products of the constants - transitions meant as actions of message transfer. In Section 4, apart for aforesaid role of constants, some of them will also play part of mailboxes. These products will be monomials in terms, being values of unknowns (send and receive variables) in the speci cation equations presented in the following two sections. 3
Equations of speci cation - synchronous mode Synchronous mode of communication (in a fairly abstract setting) has been introduced in [Hoa 1978], in extended form presented in [Hoa 1985] and implemented in some programming languages, e.g. [OCCAM 1984]. To formulate speci cation equations for such mode, suppose that with each agent-constant c 2 C is bijectively associated: its co-agent denoted c and belonging to C its send-variable denoted c! and belonging to V its receive-variable denoted c? and belonging to V The send and receive variables will get values being solutions to equations set up as follows. For i n, j m, bj ; ai 2 C let Ki(b1?; :::; bm?) be a term composed only of receive-variables bj ? and Lj (a1!; :::; an!) - a term composed only of send-variables ai!. The speci cation equations are of the form: ai! = ai bj ? = bj
Ki(b1?; :::; bm?) Lj (a1!; :::; an!) (agent ai sends to b1; :::; bm) (agent bj gets from a1; :::; an) (1) (2) with the requirement: bj ? occurs in Ki(b1?; :::; bm?) i The requirement is a consistency property of the equations. Variables ai!, bj ? are unknown quantities, while constants ai, bj are known. A region of receivers from the agent-sender ai is a subset of the set fb1; :::; bmg of receivers to which ai sends a message simultaneously. Symmetrically, a region of senders to receiver bj is a subset of the set fa1; :::; ang of senders from which bj receives a message simultaneously. Simultaneous message transfer ("multicast message") is represented by product " " of agents. The constants and variables will also be interpreted as propositional functions of state s of the distributed system such that ai is ready to send a message in a state s i ai(s) is true and it can send message i ai!(s) is true. Similarly, bj is ready to receive a message in a state s i bj (s) is true and it can receive message i bj ?(s) is true. Solutions to equations (1), (2) yield in particular net structures, but also a global information on capability of sending/receiving messages. The information is collected from a local information of agents' readiness to do this. Existence of the solutions to these equations follows from the general fact concerning equations for formal power series (their nite version) considered in [Sa-So 1978]. Remarks and intuitions (1) The speci cation equations formalize the following (recursive) phrases: "an agent a can send a message if it is ready to do this and each agent in a certain region of its receivers can receive this message from a" "an agent b can receive a message if it is ready to do this and each agent in a certain region of its senders can send this message to b" (2) Readiness of an agent to send/receive a message is determined by its internal control pointing to a send/receive instruction within the agent's program. (3) In semiring de ned by axioms (i)-(vii) in Section 2, but without (viii), that make it a lattice, the speci cation equations may have more than one solution. A solution which re ects the communication structure speci ed by equations (1), (2) is the one where each sender (resp. receiver) has the same regions of receivers (resp. senders) as speci ed in these equations. Such solution is unique and in [Cza 2006] called "appropriate". Note that appropriate solution is, in fact, the "correct" one if "correctness" is understood as conformity with speci cation. In this perspective, solving the equations means implementing the speci ed interrelation of communicating agents in terms of net-structures, along with ensuring correctness of the implementation.
Synchronous communication (speci cation): a! = a (x? y? + y?)
(a sends simultaneously to x and y or only to y) b! = b (y? z? + y?)
(b sends simultaneously to y and z or only to y) x? = x a!
(x gets from a) y? = y (a! + a! b! + b!) (y gets only from a or simultaneously from a and b or only from b) z? = z b!
(z gets from b) A solution; products represent transitions in the net representation - Fig.1: y? = a x y + a b y + b y z z? = b y z There are two regions of receivers from agent a: fx; yg; fyg, two regions of receivers from agent b: fy; zg; fyg, as well as one region of senders to agent x: fag, one region of senders to agent z: fbg, and three regions of senders to agent y: fag; fbg; fa; bg. The solution is "appropriate" since the regions of senders and receicers are the same as in the speci cation equations.
A state of the communication structure speci ed by equations (1), (2) is a function s : C ! D where D is a set of data the agents intercommunicate. In particular, if a solution is presented as a place/transition net then D = N (natural numbers). With each agent a propositional function (denoted by the same symbol as the agent and called a readiness condition) of state is associated: For a 2 C: a(s) = For a 2 C: a(s) = The functions are extended to terms over the set of agents: for K; L 2 T[C]: (K + L)(s) = K(s) _ L(s) (K
L)(s) = K(s) ^ L(s) Thus, solutions ai! = K and bj ? = L to the equations (1), (2) become propositional functions of state, de ned by ai!(s) = K(s) and bj ?(s) = L(s). This justi es phrases "sender" and "receiver", since agent a can send (receive) a message, in a state s i a!(s) = true (a?(s) = true).
The products in solutions to equations (1), (2) play part of state transformers. This interpretation is more abstract than interpretation of transitions in Petri nets because of more general meaning of state ("marking") and its transformation. Let t1 + ::: + tp be a solution (in canonical form) to a! or a?, that is ti = (a1 ::: aqi ) (b1 ::: bri ) with a1; :::; aqi ; b1; :::; bri 2 C. The product ti will represent a transition with preset a1; :::; aqi and postset b1; :::; bri . Its ring rule (semantics) is given by a relation [[ti]] S S (S = DC is the set of all states) satisfying: if (s; s0) 2 [[ti]] then (loc) (f ir) sj(Cn ti ) = s0j(Cn ti ) (locality condition) a1(s)^:::^aqi (s)^b1(s)^:::^bri (s) is true ( rability condition) where ti = fa1; :::; aqi ; b1; :::; bri g ("neighbourhood" of ti) and j - "restriction to...". Consequently, by [[a!]] ([[a?]] respectively) is denoted the relation [[t1]] [ ::: [ [[tp]]. We say that ti transforms s into s0. Note that the condition (f ir) may be written "ti(s) is true".
As shown in Example 1, a solution to (1), (2) is directly mapped onto a
net structure with places representing agents and transitions - some of their
products. This net-structure is, in fact, identical with a set of its transitions
de ned above as ti = (a1 ::: aqi ) (b1 ::: bri ). Such a net-structure exhibits
admissible communication network speci ed by the equations. Fixing the set
D of values, the relations [[ti]] and the readiness conditions of agents, various
classes of nets are obtained. For instance, in [Cza 2006], P/T and coloured
nets (with and without capacity of places and arrow weights) are generated
this way. The synchronous
From synchronous to asynchronous mode
In contrast to synchronized communication, in the asynchronous mode
its co-mailbox hai Now, the speci cation equations for the asynchronous mode of communication are: ai! = ai Ki(hb1i?; :::; hbmi?) (senders send to mailboxes of receivers) hbj i? = hbj i Lj (a1!; :::; an!) (mailboxes of receivers get from senders) (mailboxes of receivers send to the latter) (receivers get from their mailboxes) (3) (4) (5) (6) its send-variable denoted hai! its receive-variable denoted hai? hbj i! = hbj i bj ? bj ? = bj hbj i! with the requirement: hbj i! = hbj i bj bj ? = bj hbj i hbj i? occurs in Ki(hb1i?; :::; hbmi?) i Note that equations (5), (6) representing delivery of messages to receivers from their mailboxes have straightforward solutions: Equations (3), (4) are solved like those in (1), (2) in Section 3. The senders' capability of sending message depends here on capability of reception by mailboxes only. The readiness of a mailbox to get messages from senders means that it is not lled up, while its readiness to deliver a message to its receiver means that it is not empty. Therefore we consider:
For hbi 2 C: hbi(s) = For hbi 2 C: hbi(s) = if hbi is ready to deliver a message in state s otherwise if hbi is ready to get a message in state s otherwise The functions are extended to terms as formerly in the case of agents.
Asynchronous communication (speci cation): a! = a (hxi? hyi? + hyi?) b! = b (hyi? hzi? + hyi?) (a sends simultaneously to mailboxes
hxi and hyi or only to hyi) (b sends simultaneously to mailboxes
hyi and hzi or only to hyi) hxi? = hxi a! (hxi gets from a) hyi? = hyi (a!+a! b!+b!) (hyi gets only from a or simultaneously from a and b or only from b) hzi? = hzi b! (hzi gets from b) hxi! = hxi x? (hxi delivers to x) hyi! = hyi y? (hyi delivers to y) hzi! = hzi z? (hzi delivers to z) x? = x hxi! (x gets from hxi) y? = y hyi! (y gets from hyi) z? = z hzi! (z gets from hzi)
a! = a hxi hyi + a b hyi b! = b hyi hzi + a b hyi hxi? = a hxi hyi hyi? = a hxi hyi + a b hyi + b hyi hzi hzi? = b hyi hzi hxi! = hxi x hyi! = hyi y hzi! = hzi z x? = x hxi y? = y hyi z? = z hzi The solution exhibits directly data channels (links) of the agents' communication and their capability to transfer the data in a given state. For instance, agent y can receive a message from its mailbox hyi in a state s i y?(s) = y(s) ^ hyi(s) is true, meaning that the control in y reached its receive statement (instruction) and its mailbox is not empty. The mailbox hyi in a state s can receive a message either from a only or from b only, or one message from a and the other from b simultaneously i hyi?(s) = a(s) ^ hxi(s) ^ hyi(s) _ a(s) ^ b(s) ^ hyi(s) _ b(s) ^ hyi(s) ^ hzi(s) is true, meaning that the control in a reached its send statement and neither of the mailboxes hxi; hyi is lled up or the controls in a and b reached their send statements and the maibox hyi is not lled up or the control in b reached its send statement and neither of the mailboxes hyi; hzi is lled up. 5
Final notes
(1) The role of variables ai!; bj ? is similar to that of "meta variables"
(nonterminals) in BNF: they assume terms, that is strings of constants
(terminals), as values. Also the role of constants is similar: they assume elements
of D, the set of data, as values.
(2) Solutions to speci cation equations for synchronous (blocking) and
asynchronous (non-blocking) mode, describe a kind of intercommunication where
communication lines between the agents are xed for a given computational
session. The lines are pictorialy visible as arcs of nets representing the
solutions. The interesting issue is to adjust the idea to systems where the
lines are being established dynamicaly - during the session. To this end,
the idea of self-modifying nets, introduced by Ruediger Valk [Val 1978], [Val
1981], or perhaps, strati ed nets [B-D 1997], seems promissing. Also,
modelling of the so-called connection oriented (sender and receiver set up a line
and make an arrangement on some details of communication prior to the
communication itself; the line remains as long as it is needed during
communication) and connectionless communication