Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes

Broadbent and G"oller (FSTTCS 2012) proved the undecidability of bisimulation equivalence for processes generated by epsilon-free second-order pushdown automata. We add a few remarks concerning the used proof technique, called Defender’s forcing, and the related undecidability proof for first-order pushdown automata with epsilon-transitions (Jan\v{c}ar and Srba, JACM 2008).