Bisimulation for Lattice-valued Transition Systems

In this paper, we define lattice-valued labeled transition systems (LLTS) as a general framework for allowing imprecise or incomplete specifications to be expressed. We introduce a lattice-valued bisimulation between LLTSs that measures the degree of closeness of two systems as elements of residuated lattice, in contrast to the traditional boolean yes/no to bisimulation. Also, we show that our bisimulation is compositional for a synchronous composition operator. Moreover, we also consider lattice-valued extension of Kripke structures, define a lattice-valued bisimulation between lattice-valued Kripke structures (LKSs), and establish the correspondence between lattice-valued bisimulation in LLTS and lattice-valued bisimulation in LKS.