Deciding Bisimilarity between BPA and BPP Processes

We identify a necessary condition for when a given BPP process can be expressed as a BPA process. We provide an effective procedure for testing if this condition holds of a given BPP, and in the positive case we provide an effective construction for a particular form of one-counter automaton which is bisimilar to the given BPP. This in turn provides the mechanism to decide bisimilarity between a given BPP process and a given BPA process.

• Type: Conference
• Year: 2003
• Where: CONCUR
• Authors: Petr Jancar, Antonín Kucera, Faron Moller
• Keywords: BPA Process, BPP Process, CONCUR 2003, Necessary Condition