Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/410

This item has been viewed 21 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-93-278.ps1.35 MBPostscriptView/Open
Title: Decidability and Decomposition in Process Algebras
Authors: Christensen, Søren
Issue Date: Sep-1993
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: 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.
URI: http://hdl.handle.net/1842/410
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy