Equational Reasoning About Nondeterministic Processes

A deterministic message-communicating process can be characterized by a “continuous” function f which describes the relationship between the inputs and the outputs of the process. The operational behavior of a network of deterministic processes can be deduced from the least fixpoint of a function g, where g is obtained from the functions that characterize the component processes of the network. We show in this paper that a nondeterministic process can be characterized by a “description” consisting of a pair of functions. The behavior of a network consisting of such processes can be obtained from the “smooth” solutions of the descriptions characterizing its component processes. The notion of smooth solution is a generalization of least fixpoint. Descriptions enjoy the crucial property that a variable may be replaced by its definition.

• Type: Conference
• Year: 1989
• Where: PODC
• Authors: Jayadev Misra
• Keywords: Component Processes, Deterministic Message-communicating Process, Deterministic Processes, Distributed And Parallel Computing, PODC 1989