文章基本信息

标题：Deciding Regularity in Process Algebras
本地全文：下载
作者：Antonin Kucera
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1995
卷号：2
期号：52
出版社：Aarhus University
摘要：We consider the problem of deciding regularity of normed BPP and 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.