We consider the problem of deciding regularity of normed BPP and normed BPA processes. A process is regular if it is bisimilar to a process with finitely many states. We show that regularity of normed BPP and normed BPA processes is decidable in polynomial time and we present constructive regularity tests. Combining these two results we obtain a rich subclass of normed PA processes (called sPA) where the regularity is also decidable. Moreover, constructiveness of this result implies decidability of bisimilarity for pairs of processes such that one process of this pair is sPA and the other has finitely many states.
展开▼
