Complete, Effective and Abstract System For Reasoning About Networks of Processes
We present a complete recursive set of axioms for reasoning about networks of bounded asynchronous processes with finite resources. We also present an effective procedure for hiding internal channels of a network. Our processes use finite resources and bounded asynchronous communication. Such processes and networks can be physically realized. Our processes can be specified by means of regular expressions and do not require the full theory of arithmetic. The assertion language we use exploits this fact and allows us to specify all such processes and networks and obtain a complete and effective use of Ehrenfeucht games. An algorithm for channel hiding follows from the way these processes can be modeled.