Topological constructions of epsilon-bisimulation

Abstract

ϵ-bisimulation provides a kind of abstraction description for the correctness of software with probabilistic information. ϵ-limit bisimulation had been proposed, which entails that specification is the limit of implementations based on ϵ-bisimulation. In this paper, we only focus on the topological properties of ϵ-limit bisimulation. According to the definition of ϵ-limit bisimulation, several closure constructions are established, such as subnet closure, tail closure, natural extension and iteration. These closure constructions are useful to characterize properties of software.