Bisimulation

A binary relation between states of state-based systems (Kripke models, labeled transition systems, processes) that matches their observable behavior stepwise: whenever related states perform a transition labeled a, the related partner can match with an a-transition to related target states, and vice versa; bisimulation equivalence (bisimilarity) means there exists such a relation linking the stat