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₀ M₁ N₁ C₁ M₂ N₂ C₃ ... 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 ~ⁱ 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.

CategoryDistributedComputingNotes