Bisimulation Indexes Induced by Metrics on Actions
In the last chapter we introduced an approximate version of bisimilarity, namely, near bisimilarity, which can serve as a formal tool for describing a kind of approximate correctness of concurrent programs. In this chapter we intend to loosen the concept of bisimilarity from another direction. It is well known that bisimulation expresses the equivalence of processes whose external actions are identical. The condition of possessing the same actions is quite rigorous, and sometimes we meet two processes that fail to fit this condition but are still more or less bisimilar in the sense that whenever a process makes an action, another process can make an action different from but very similar to the action the first process made. The purpose of this chapter is to provide some mathematical tools that are suitable for describing this kind of approximate bisimilarity.
KeywordsInduction Hypothesis Transition System Label Transition System Agent Schema Communication Rule
Unable to display preview. Download preview PDF.