Show simple item record

dc.contributor.advisorJerrum, Mark
dc.contributor.authorStríbrná, Jitka
dc.date.accessioned2004-03-02T16:13:36Z
dc.date.available2004-03-02T16:13:36Z
dc.date.issued1999-07
dc.identifier.urihttp://hdl.handle.net/1842/383
dc.description.abstractIn 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. 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.en
dc.contributor.sponsorWolfson Foundation Scholarshipen
dc.format.extent560572 bytes
dc.format.extent1100788 bytes
dc.format.extent964221 bytes
dc.format.mimetypeapplication/x-dvi
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleDecidability and complexity of equivalences for simple process algebrasen
dc.typeThesis or Dissertation
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record