Techniques for Decidability and Undecidability of Bisimilarity
Petr Jančar5
and Faron Moller6 
| (5) |
Technical University of Ostrava, Czech Republic |
| (6) |
Uppsala University, Sweden |
Abstract
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 by onecounter 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).
The second author is supported by Swedish TFR grants No. 221-98-103 ’Verification of Infinite State Automata’ and 221-97-275
’Games for Processes’.
References secured to subscribers.