This research will extend data flow analysis of networks of communicating finite state machines in several promising directions. If the network is represented by a set of flow equations, its behavior can then be described by the exact solution of these equations. Finding this solution is, in general, an undecidable question, Instead, one can propose and verify an approximate solution to the equations. The approximate solution is conservative. Thus, it can be used later to verify that the network's behavior satisfies a number of desirable properties, such as freedom from deadlocks.
