RECENT RESULTS IN THE STATIC ANALYSIS OF COMMUNICATING FINITE STATE PROCESSES.

The Finite State Process (FSP) is a modeling technique for concurrent programs and network protocols stemming from several recent algebraic treatments of concurrency. We examine the FSP in the context of two problems of static analysis: (1) FSP equivalence, and (2) cooperation vs. antagonism in networks of FSPs. Regarding (1), we analyze two equivalence notions: observation equivalence and congruence. Concerning (2), we characterize the familiar problems of potential blocking, lockout, and termination in terms of cooperative and antagonistic processes. Using this approach, we show that all three problems can be decided efficiently for loosely connected networks of tree FSPs.