9.06.2005

Equations for message passing

Suppose a collection of objects capable of exchanging data is given. If an object has some messages to be sent, let us say it is ready to send, otherwise it is unready to send. If an object has enough capacity to admit some messages, it is ready to receive, otherwise it is unready to receive. Any of these four transient capabilities is called a status of the object. A change of a status occurs on send/receive transactions the object is involved in. It can send (receive) a message if it is ready to do this, and each object in a certain set of its receivers (senders) is ready to receive (send) the message. This recursive phrase is made formal by equations in an algebraic structure called a semiring with addition interpreted as exclusive choice and multiplication as simultaneity, and with a restricted form of idempotency of the latter. The equations have the least (wrt. a natural partial order) solution, which is unique and interpreted as a set of state transformers. In this framework, in particular various kind of Petri nets as state transformers may be generated by solving equations specifying systems based on message passing paradigm.