Regularity of BPA-Systems is Decidable

摘要

It is decidable whether a system in Basic Process Algebra (BPA) is regular withrespect to bisimulation semantics. Basic operators in BPA are alternative composition, sequential composition and guarded recursion. A system is regular if the interpretations of all process variables defined in the system have finitely many states. We present an effective method to transform a BPA specification into a linear specification whenever possible.