  Bisimulation provides a good example of the fruitful interactions that have been developed between modal logic and computer science. In computer science, labeled transition systems (LTSs) are commonly used to represent possible computation pathways during execution of a program. LTSs are generalizations of Kripke frames, consisting of a set \(W\) of states, and a collection of \(i\)-accessibility relations \(R_i\), one for each computer process \(i\). Intuitively, \(wR_i w'\) holds exactly when \(w'\) is a state that results from applying the process \(i\) to state \(w\).