*For more up-to-date notes see http://www.cs.yale.edu/homes/aspnes/classes/465/notes.pdf.*

See LynchBook Chapter 2, which calls this model a **synchronous network model.** Unlike later models, LynchBook does not use IOAutomata to model this (it's uglier than doing it directly).

Basic ideas:

- Fixed set of n known processes
Each

**process**(an automaton of some sort) can communicate with neighbors in some network, typically represented as directed graph. Nodes in the graph represent processes, edges represent**channels**.Details of processes: i-th process is modeled by a tuple (states

_{i}, start_{i}, msgs_{i}, trans_{i}).states

_{i}is state set, which may be infinite (interpretation: we really don't care at all about local computation)start

_{i}is subset of states_{i}that process can start in (we allow multiple possible start states to represent nondeterminism, inputs, etc.)msgs

_{i}is a function from (states_{i}× out-nbrs_{i}) to M union {null}; specifies message to send to each neighbor.trans

_{i}is a function from (states_{i}× (M union {null})^{in-nbrs[i]}) to states_{i}; specifies response to incoming messages.

**Execution**is a sequence C_{0}M_{1}N_{1}C_{1}M_{2}N_{2}C_{3}... where each C_{i}is a vector of states (the**configuration**), M_{i}is the vector of messages sent in each channel from C_{i-1}, N_{i}are the corresponding messages delivered (possibly omitting some messages from M_{i}).

Notion of **indistinguishability**: a ~^{i} a' if i has the same sequence of states and incoming and outgoing messages in both a and a', where a and a' are executions of the same or even different synchronous systems. Indistinguishability is a key technique for proving impossibility results, as in TwoGenerals.