Résumé: We present an exact characterization of those transition systems which can be equivalently (up to bisimilarity) defined by the syntax of normed BPA(T) and normed BPP(T) processes. We give such a characterization for the subclasses of normed BPA and normed BPP processes as well. Next we demonstrate the decidability of the problem whether for a given normed BPA(T) process 'Delta' there is some unspecified normed BPP(T) process 'Delta' ' such that 'Delta' and 'Delta' ' are bisimilar. The algorithm is polynomial. Furthermore, we show that if the answer to the previous question is positive, then (an example of) the process 'Delta' ' is effectively constructible. Analogous algorithms are provided for normed BPP(T) processes. Simplified versions of the mentioned algorithms which work for normed BPA and normed BPP are given too. As a simple consequence we obtain the decidability of bisimilarity in the union of normed BPA(T) and normed BPP(T) processes.

Langue: Anglais