Note on Undecidability of Bisimilarity for Second-Order Pushdown Processes

TL;DR

This paper discusses the undecidability of bisimilarity for second-order pushdown processes, analyzing the proof techniques used in prior work and their implications for related automata models.

Contribution

It provides insights into the proof method called Defender's forcing and extends understanding of undecidability results for higher-order pushdown automata.

Findings

Undecidability of bisimilarity for second-order pushdown automata confirmed.

Analysis of Defender's forcing proof technique.

Comparison with first-order pushdown automata undecidability proofs.

Abstract

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).