Deciding bisimulation equivalence and semantic finiteness of first-order grammars

The plan is to briefly recall the ideas of the decidability proof for bisimulation equivalence of first-order grammars; the proof (presented at ICALP'14) is an alternative for Senizergues's proof for equational graphs with finite out-degree that generalized his famous decidability proof for DPDA (deterministic pushdown automata) equivalence. The decidability of equivalence will be then used in demonstrating the decidability of semantic finiteness (w.r.t. bisimilarity) of first-order grammars; this answered an open question and was presented at MFCS'16.