Decidability and Decomposition in Process Algebras

This thesis is concerned with the question of obtaining decidable theories for behavioural equivalences on various models of (parallel) computation encompassing systems with infinitely many states. The models on which we concentrate are based on the process calculi BPA and BPP but we also consider labelled Petri nets. The equivalences which we are interested in are language equivalence, bisimulation equivalence and distributed bisimulation equivalence. BPA (Basic Process Algebra) is provided by a standard calculus which admits of a general sequencing operator, along with atomic actions, choice and recursion. In contrast, BPP (Basic Parallel Processes) is provided by a standard calculus which admits of a simple parallel operator (full merge), along with atomic actions, choice and recursion. From the point of view of language equivalence we show that BPA and BPP are incomparable. This result is in part obtained through a pumping lemma for BPP. We furthermore show that the class of languages generated by BPP is included in a class of languages generated by labelled Petri nets as well as contained in the class of context-sensitive languages. Next we investigate into decidability of language equivalence on language classes related to BPP and Petri nets. We then move on to bisimulation equivalence. We show that this equivalence is decidable on all of BPA, answering a question left open by Baeten, Bergstra and Klop. We also show that bisimulation equivalence is decidable on BPP and BPPr, (where BPPr is similar to BPP except for its parallel operator which allows for synchronisation). By these results we have obtained a delicate line between decidable and undecidable theories for bisimilarity; by extending BPPr, with the operator of restriction we know that bisimilarity is undecidable. By relying on Jancar's recent result on the undecidability of bisimilarity on labelled Petri nets we further narrow the gap between decidable and undecidable theories; when extending BPP with a notion of forced synchronisation we know that bisimilarity is undecidable. The decidability proofs of bisimulation equivalence on BPP and BPPr (obtained via the tableau technique) permit us further to present sound and complete equational theories for these process classes. As BPP and BPPr contain the regular processes their results may be seen as proper extensions of Milner's equational theory for regular processes. In this thesis we shall also consider the problem of decomposing a process into the parallel composition of simpler processes. A particular aspect of decomposition involves decomposing uniquely into prime processes, i.e. those processes which cannot themselves be expressed as a parallel composition of other non-trivial processes. We shall present several unique decomposition results for bisimilarity and distributed bisimilarity on BPP and BPPr as well as subclasses thereof. Finally, for distributed bisimulation equivaalence we show decidability on the process classes BPP and BPPr. Again our proofs of decidability permit us to present sound and complete equational theories. These results may be seen as extensions of Castellani's equational theories for distributed bisimilarity on the recursion-free fragments of BPP and BPPr. Also for a fragment of BPPr where general summation is replaced by guarded summation shall we present an equational theory for distributed bisimilarity. The proof of completeness relies on the unique decomposition property admitted by this equivalence on BPP