Deciding Regularity in Process Algebras

Open Access
Publisher Website
Google Scholar
Abstract
We consider the problem of deciding regularity of normed BPPand normed BPA processes. A process is regular if it is bisimilar to aprocess with finitely many states. We show, that regularity of normedBPP processes is decidable and we provide a constructive regularitytest. We also show, that the same result can be obtained for the classof normed BPA processes.Regularity can be defined also w.r.t. other behavioural equivalences.We define notions of strong regularity and finite characterisationand we examine their relationship with notions of regularityand finite representation. The introduced notion of the finite characterisationis especially interesting from the point of view of possibleverification of concurrent systems.In the last section we present some negative results. If we extendthe BPP algebra with the operator of restriction, regularity becomesundecidable and similar results can be obtained also for other processalgebras.

This publication has 0 references indexed in Scilit: