A THEORY OF PROCESSES (MODEL, PROOF SYSTEM, PROGRAMMING LANGUAGE, PROGRAM SYNTHESIS, TEMPORAL LOGIC)

In recent years, there has been a lot of interest in concurrent programming and distributed computing. This gives rise to the notion of a process. A process is a computing agent that performs some task and communicates with other agents for inputs and outputs.;We also present a simple parallel functional language that incorporates most of the programming constructs in the model. The language enables one to describe processes algorithmically. It combines features of functional and concurrent languages and has a general recursion scheme that makes it more expressive than Hoare's CSP (78). The language also demonstrates how communication and concurrency could be handled in a functional language.;Finally, we give a deductive system for synthesizing asynchronous networks of deterministic processes. Due to the difficulty of the problem, we are not able to do this for more general types of network. The synthesis system uses the deductive tableau method that Manna and Waldinger (80, 82) developed for sequential programs. In this approach, the synthesis of a program is regarded as a theorem-proving problem; the desired program is constructed as a by-product of the proof. This enables us to use such powerful tools like transformation rules and resolution rules in a single framework.;In this thesis, we attempt to give a comprehensive theory of processes. We give a general set-theoretic model of processes that forms the formal basis of our theory. The model is quite simple, and yet it is more expressive than any model of processes that we know of, e.g. by Hoare (83), Pratt (82) and Milner (80). A compositional temporal proof system is defined on the model. This provides a formal language and framework in which processes can be specified and reasoned about. The proof system is simpler than any temporal proof system for processes that we know of, e.g. by Manna-Pnueli (81, 83) and Barringer-Kuiper-Pnueli (84), and yet it is just as expressive. Furthermore, it is as simple as any existing Hoare-like proof systems, e.g. by Chen-Hoare (81), Levin-Gries (81) and Misra-Chandy (81), but is more expressive.