Deciding semantic finiteness of first-order grammars w.r.t. bisimulation equivalence
The plan is to explain the main ideas of the MFCS'16 paper
by figures (and without formalities).
The presented decidability proof for semantic finiteness (or "regularity") of first-order grammars (that encompass pushdown automata) w.r.t. bisimulation equivalence relies on the decidability of bisimulation equivalence (which was first proven by Senizergues).