Techniques for decidability and undecidability of bisimilarity

In this tutorial we describe general approaches to deciding bisimilarity between vertices of (infinite) directed edge-labelled graphs. The approaches are based on a systematic search following the definition of bisimilarity. We outline (in decreasing levels of detail) how the search is modified to solve the problem for finite graphs, BPP graphs, BPA graphs, normed PA graphs, and normed PDA graphs. We complete this by showing the technique used in the case of graphs generated Ly one-counter machines. Finally, we demonstrate a general reduction strategy for proving undecidability, which we apply in the case of graphs generated by state-extended BPP (a restricted form of labelled Petri nets).