dc.contributor.advisor Jerrum, Mark en dc.contributor.author Stríbrná, Jitka en dc.date.accessioned 2004-03-02T16:13:36Z dc.date.available 2004-03-02T16:13:36Z dc.date.issued 1999-07 dc.identifier.uri http://hdl.handle.net/1842/383 dc.description.abstract In this thesis I study decidability, complexity and structural properties of strong and weak bisimilarity with respect to two process algebras, Basic Process Algebras and Basic Parallel Process Algebras. en The decidability of strong bisimilarity for both algebras is an established result. For the subclasses of normed BPA-processes and BPP there even exist polynomial decision procedures. The complexity of deciding strong bisimilarity for the whole class of BPP is unsatisfactory since it is not bounded by any primitive recursive function. Here we present a new approach that encodes BPP as special polynomials and expresses strong bisimulation in terms of polynomial ideals and then uses a theorem about polynomial ideals (Hilbert's Basis Theorem) and an algorithm from computer algebra (Gröbner bases) to construct a new decision procedure. For weak bisimilarity, Hirshfeld found a decision procedure for the subclasses of totally normed BPA-processes and BPP, and Esparza demonstrated a semidecision procedure for general BPP. The remaining questions are still unsolved. Here we provide some lower bounds on the computational complexity of a decision procedure that might exist. For BPP we show that the decidability problem is NP-hard (even for the class of totally normed BPP), for BPA-processes we show that the decidability problem is PSPACE-hard. Finally we study the notion of weak bisimilarity in terms of its inductive definition. We start from the relation containing all pairs of processes and then form a non-increasing chain of relations by eliminating pairs that do not satisfy a certain expansion condition. These relations are labelled by ordinal numbers and are called approximants. We know that this chain eventually converges for some a' such that =a' = =b' = = for all a' < b'. We study the upper and lower bounds on such ordinals a'. We prove that for BPA, a' => w^w, and for BPPA, a' => w.2. For some restricted classes of BPA and BPPA we show that = = =w.2. dc.contributor.sponsor Wolfson Foundation Scholarship en dc.format.extent 560572 bytes en dc.format.extent 1100788 bytes en dc.format.extent 964221 bytes en dc.format.mimetype application/x-dvi en dc.format.mimetype application/pdf en dc.format.mimetype application/postscript en dc.language.iso en dc.publisher University of Edinburgh. College of Science and Engineering. School of Informatics. en dc.title Decidability and complexity of equivalences for simple process algebras en dc.type Thesis or Dissertation en dc.type.qualificationlevel Doctoral en dc.type.qualificationname PhD Doctor of Philosophy en
﻿