It is decidable whether a system in Basic Process Algebra (BPA) is regular with respect 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.
|Title of host publication||CONCUR'94 (Proceedings 5th International Conference on Concurrency Theory, Uppsala, Sweden, August 22-25, 1994)|
|Editors||B. Jonsson, J. Parrow|
|Publication status||Published - 1994|
|Name||Lecture Notes in Computer Science|