Basic process algebra with deadlocking states (Q5958771)

Bisimilarity and regularity are decidable properties for the class of BPA (or context-free) processes [\textit{S. Christensen, H. Hütel} and \textit{C. Stirling}, Inf. Comput. 121, 143-148 (1995; Zbl 0833.68074); \textit{O. Burkart, D. Caucal} and \textit{B. Steffen}, Lect. Notes Comput. Sci. 119, 247-262 (1996)]. We extend BPA with a deadlocking state obtaining \(\text{BPA}_{\delta}\) systems. We show that the \(\text{BPA}_{\delta}\) class is more expressive w.r.t. bisimilarity, but it remains language equivalent to BPA. We prove that bisimilarity and regularity remain decidable for \(\text{BPA}_{\delta}\). Finally, we give a characterisation of those \(\text{BPA}_{\delta}\) processes that can be equivalently (up to bisimilarity) described within the ``pure'' BPA syntax.