Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Techniques for Decidability and Undecidability of Bisimilarity

Petr JančarContact Information and Faron MollerContact Information

(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’.

Contact Information Petr Jančar
Email: Petr.Jancar@vsb.cz

Contact Information Faron Moller
Email: fm@csd.uu.se
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.106 • Server: mpweb21
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)