TY - JOUR AU - Kucera, Antonin PY - 1995/06/22 Y2 - 2024/03/28 TI - Deciding Regularity in Process Algebras JF - BRICS Report Series JA - BRICS VL - 2 IS - 52 SE - Articles DO - 10.7146/brics.v2i52.19953 UR - https://tidsskrift.dk/brics/article/view/19953 SP - AB - We consider the problem of deciding regularity of normed BPP<br />and normed BPA processes. A process is regular if it is bisimilar to a<br />process with finitely many states. We show, that regularity of normed<br />BPP processes is decidable and we provide a constructive regularity<br />test. We also show, that the same result can be obtained for the class<br />of normed BPA processes.<br />Regularity can be defined also w.r.t. other behavioural equivalences.<br />We define notions of strong regularity and finite characterisation<br />and we examine their relationship with notions of regularity<br />and finite representation. The introduced notion of the finite characterisation<br />is especially interesting from the point of view of possible<br />verification of concurrent systems.<br />In the last section we present some negative results. If we extend<br />the BPP algebra with the operator of restriction, regularity becomes<br />undecidable and similar results can be obtained also for other process<br />algebras. ER -