Near Bisimulations Defined by Closures

Abstract

The last two chapters presented a dynamic approach to approximation of processes, which aims at describing infinite evolution of concurrent programs. This chapter and the next one are devoted to a static study of approximation of processes that provides some formal methods for deducing approximate correctness of concurrent programs. In this chapter, we introduce the concept of near bisimilarity as a loosened version of usual bisimilarity. Roughly speaking, it expresses the equivalence of agents whose almost but not quite all (external) actions follow the same pattern—more exactly, whose (external) actions that follow the same pattern are dense in the set of all actions according to some given topology. In Section 5.1, we deal with near bisimulations in general labeled transition systems and their invariance with respect to operations of transition systems, including natural extension, idle modification, restriction, relabeling, product and three different versions of sum. Sections 5.2 and 5.3 are devoted to various properties of near strong and weak bisimulations, respectively, in the basic process calculus. In particular, we show that strong near bisimilarity is preserved by all combinators in our process calculus except Composition, and weak near bisimilarity is preserved by all combinators except Summation and Composition. The substitutivity of weak near bisimilarity under Summation may be repaired in a familiar way; that is, we find the biggest congruence relation included in weak near bisimilarity.