We will recall a generic technique for proving lower bounds for bisimulation equivalence checking (for which there was not enough time in my last LAAG talk) . First, we will introduce bisimulation equivalence and recall Jancar’s and Srba’s Defender’s Forcing lower bound technique. Then, we will apply this technique to different classes of infinite state systems for showing the following hardness results : (1) undecidability for prefix-recognizable graphs, (2) undecidability for vector addition systems, (3) nonelementary hardness for pushdown graphs, and (4) Ackermann hardness for equational graphs of finite out-degree.