Renomovaný časopis Journal of Computer and Systems Sciences zveřejnil práci člena katedry informatiky Petra Jančara Equivalence of pushdown automata via first-order grammars.

V práci je uveden alternativní důkaz rozhodnutelnosti bisimulační ekvivalence pro gramatiky prvního řádu (tj. určitého protějšku zásobníkových automatů); první důkaz publikoval G. Sénizergues (1998, 2005), který tak rozšířil rozhodnutelnost ekvivalence deterministických zásobníkových automatů, za jejíž prokázání dostal v r. 2002 Gödelovu cenu. Zde prezentovaný důkaz je koncepčně jednodušší a pro čtenáře přístupnější a je podán ve formě, která umožňuje analýzu složitosti tohoto obtížného problému. Problém byl později na základě takové analýzy kvalifikován jako ,,Ackermann-complete''.