Fuzzy labeled transition system vertical bisimulation

Fuzzy Labeled Transition Refinement Tree (FLTRT) is a rigorous refinement model which supports abstraction and handling incomplete information and by the way reducing complexity of refinement process. It is based on Fuzzy Labeled Transition System (FLTS) which is a generalization of well-known Labeled Transition System, enhanced by fuzziness facility. The FLTRT structure serves as a tree of potential concurrent design trajectories of the system. In this paper, we study bisimulation relations on FLTSs which are categorized into two classes: horizontal and vertical bisimulation relations. The former class aims to identify equivalent specifications of the same abstraction level. However, the second one relates specifications that belong conceptually to different abstraction levels. Vertical bisimulation relation aims to check correctness of a given implementation with respect to its initial specification. FLTRT structure preserves the vertical bisimulation relation.