Two-thirds simulation indexes and modal logic characterization

Two-thirds simulation provides a kind of abstract description of an implementation with respect to a specification. In order to characterize the approximate two-thirds simulation, we propose the definition of a two-thirds simulation index which expresses the degree to which a binary relation between processes is two-thirds simulation. λ-two-thirds simulation and its substitutivity laws are given in this paper. And, based on λ-two-thirds simulation, we present a measure model for describing the degree of approximation between processes. In particular, we give the modal logical characterization of λ-two-thirds simulation.