PineWikiSee 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 (statesi, starti, msgsi, transi).
statesi is state set, which may be infinite (interpretation: we really don't care at all about local computation)
starti is subset of statesi that process can start in (we allow multiple possible start states to represent nondeterminism, inputs, etc.)
msgsi is a function from (statesi × out-nbrsi) to M union {null}; specifies message to send to each neighbor.
transi is a function from (statesi × (M union {null})in-nbrs[i]) to statesi; specifies response to incoming messages.
Execution is a sequence C0 M1 N1 C1 M2 N2 C3 ... where each Ci is a vector of states (the configuration), Mi is the vector of messages sent in each channel from Ci-1, Ni are the corresponding messages delivered (possibly omitting some messages from Mi).
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.