Conclusion

Abstract

As indicated by the title of this book, the driving idea is to find useful methods for reasoning about approximate correctness and infinite evolution of programs. We focus on concurrent systems and choose R. Milner’s process calculus [Milner 1980, 1989] as the formalization of systems. Our approach is to introduce topological structures into process calculus. These topological structures represent approximation relations among processes. The idea of introducing topological structures into models of computation can be traced back to the early stage of computing theory. The structural operational semantics of process calculus is generally given as labeled transition systems. Obviously, a labeled transition system is a nondeterministic automaton [Hopcroft and Ullman 1979] in which initial and final states are canceled such that it is suitable to serve as an abstract model of nonterminating systems. As early as the 1960s, the idea of obtaining a topological machine by adding some mathematical structure to an abstract machine was formulated by S. Ginsburg [1962]. Shortly after, a compact automaton, a special topological machine, was proposed by A. Shreider [1964] in order to study dynamic programming. A general study of topological automata was carried out by W. Brauer [1970]. To regularize some fixed-point semantics for concurrent interacting systems, R.E. Kent [1987] introduced the concept of metric transition systems in which states are equipped with an ultrametric.