  The language of poly-modal or dynamic logic introduces a collection of modal operators \(\Box_i\), one for each program \(i\) (Harel, 1984). Then \(\Box_i\)A states that sentence \(A\) holds in every result of applying \(i\). So ideas like the correctness and successful termination of programs can be expressed in this language. Models for such a language are like Kripke models save that LTSs are used in place of frames. A bisimulation is a counterpart relation between states of two such models such that exactly the same propositional variables are true in counterpart states, and whenever world \(v\) is \(i\)-accessible from one of two counterpart states, then the other counterpart bears the \(i\)-accessibility relation to some counterpart of \(v\). In short, the \(i\)-accessibility structure one can “see” from a given state mimics what one sees from a counterpart. Bisimulation is a weaker notion than isomorphism (a bisimulation relation need not be 1-1), but it is sufficient to guarantee equivalence in processing.