ABSTRACT
A network is shared by several processes that exchange information by sending and receiving messages. A sending process can broadcast a message to all other processes in a single operation. A distinction is made between broadcasting and multicasting. There is a great diversity in the possible choice of signatures and first-order properties that can be used to model networks. One of the decisions to make is to determine which events are terminating. This chapter describes two settings for specifying networks, that is, two signatures and first-order languages in which to express properties of network activity: (1) The Send/Receive Network Signature, and ( 2) the Message Domain Signature.
