Deciding Regularity in Process Algebras
DOI:
https://doi.org/10.7146/brics.v2i52.19953Abstract
We consider the problem of deciding regularity of normed BPPand normed BPA processes. A process is regular if it is bisimilar to a
process with finitely many states. We show, that regularity of normed
BPP processes is decidable and we provide a constructive regularity
test. We also show, that the same result can be obtained for the class
of normed BPA processes.
Regularity can be defined also w.r.t. other behavioural equivalences.
We define notions of strong regularity and finite characterisation
and we examine their relationship with notions of regularity
and finite representation. The introduced notion of the finite characterisation
is especially interesting from the point of view of possible
verification of concurrent systems.
In the last section we present some negative results. If we extend
the BPP algebra with the operator of restriction, regularity becomes
undecidable and similar results can be obtained also for other process
algebras.
Downloads
Published
1995-06-22
How to Cite
Kucera, A. (1995). Deciding Regularity in Process Algebras. BRICS Report Series, 2(52). https://doi.org/10.7146/brics.v2i52.19953
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.