No Cover Image

E-Thesis 141 views 49 downloads

Towards weak bisimilarity on a class of parallel processes. / W. J. T Harwood

Swansea University Author: W. J. T Harwood

Abstract

A directed labelled graph may be used, at a certain abstraction, to represent a system's behaviour. Its nodes, the possible states the system can be in; its arrows labelled by the actions required to move from one state to another. Processes are, for our purposes, synonymous with these labelled...

Full description

Published: 2006
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
URI: https://cronfa.swan.ac.uk/Record/cronfa42496
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-08-02T18:54:51Z
last_indexed 2018-08-03T10:10:18Z
id cronfa42496
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-08-02T16:24:29.4625964</datestamp><bib-version>v2</bib-version><id>42496</id><entry>2018-08-02</entry><title>Towards weak bisimilarity on a class of parallel processes.</title><swanseaauthors><author><sid>1a60068903d11c5a551b2ab5bc82def3</sid><ORCID>NULL</ORCID><firstname>W. J. T</firstname><surname>Harwood</surname><name>W. J. T Harwood</name><active>true</active><ethesisStudent>true</ethesisStudent></author></swanseaauthors><date>2018-08-02</date><abstract>A directed labelled graph may be used, at a certain abstraction, to represent a system's behaviour. Its nodes, the possible states the system can be in; its arrows labelled by the actions required to move from one state to another. Processes are, for our purposes, synonymous with these labelled transition systems. With this view a well-studied notion of behavioural equivalence is bisimilarity, where processes are bisimilar when whatever one can do, the other can match, while maintaining bisimilarity. Weak bisimilarity accommodates a notion of silent or internal action. A natural class of labelled transition systems is given by considering the derivations of commutative context-free grammars in Greibach Normal Form: the Basic Parallel Processes (BPP), introduced by Christensen in his PhD thesis. They represent a simple model of communication-free parallel computation, and for them bisimilarity is PSPACE-complete. Weak bisimilarity is believed to be decidable, but only partial results exist. Non-bisimilarity is trivially semidecidable on BPP (each process has finitely many next states, so the state space can be explored until a mis-match is found); the research effort in proving it fully decidable centred on semideciding the positive case. Conversely, weak bisimilarity has been known to be semidecidable for a decade, but no method for semideciding inequivalence has yet been found - the presence of silent actions allows a process to have infinitely many possible successor states, so simple exploration is no longer possible. Weak bisimilarity is defined coinductively, but may be approached, and even reached, by its inductively defined approximants. Game theoretically, these change the Defender's winning condition from survival for infinitely many turns to survival for K turns, for an ordinal k, creating a hierarchy of relations successively closer to full weak bisimilarity. It can be seen that on any set of processes this approximant hierarchy collapses: there will always exist some K such that the kth approximant coincides with weak bisimilarity. One avenue towards the semidecidability of non- weak bisimilarity is the decidability of its approximants. It is a long-standing conjecture that on BPP the weak approximant hierarchy collapses at o x 2. If true, in order to semidecide inequivalence it would suffice to be able to decide the o + n approximants. Again, there exist only limited results: the finite approximants are known to be decidable, but no progress has been made on the wth approximant, and thus far the best proven lower-bound of collapse is w1CK (the least non-recursive ordinal number). We significantly improve this bound to okx2(for a k-variable BPP); a key part of the proof being a novel constructive version of Dickson's Lemma. The distances-to-disablings or DD functions were invented by Jancar in order to prove the PSPACE-completeness of bisimilarity on BPP. At the end of his paper is a conjecture that weak bisimilarity might be amenable to the theory; a suggestion we have taken up. We generalise and extend the DD functions, widening the subset of BPP on which weak bisimilarity is known to be computable, and creating a new means for testing inequivalence. The thesis ends with two conjectures. The first, that our extended DD functions in fact capture weak bisimilarity on full BPP (a corollary of which would be to take the lower bound of approximant collapse to and second, that they are computable, which would enable us to semidecide inequivalence, and hence give us the decidability of weak bisimilarity.</abstract><type>E-Thesis</type><journal/><journalNumber></journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><issnPrint/><issnElectronic/><keywords>Computer science.</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2006</publishedYear><publishedDate>2006-12-31</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2018-08-02T16:24:29.4625964</lastEdited><Created>2018-08-02T16:24:29.4625964</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>W. J. T</firstname><surname>Harwood</surname><orcid>NULL</orcid><order>1</order></author></authors><documents><document><filename>0042496-02082018162459.pdf</filename><originalFilename>10801726.pdf</originalFilename><uploaded>2018-08-02T16:24:59.0870000</uploaded><type>Output</type><contentLength>4643347</contentLength><contentType>application/pdf</contentType><version>E-Thesis</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-02T16:24:59.0870000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2018-08-02T16:24:29.4625964 v2 42496 2018-08-02 Towards weak bisimilarity on a class of parallel processes. 1a60068903d11c5a551b2ab5bc82def3 NULL W. J. T Harwood W. J. T Harwood true true 2018-08-02 A directed labelled graph may be used, at a certain abstraction, to represent a system's behaviour. Its nodes, the possible states the system can be in; its arrows labelled by the actions required to move from one state to another. Processes are, for our purposes, synonymous with these labelled transition systems. With this view a well-studied notion of behavioural equivalence is bisimilarity, where processes are bisimilar when whatever one can do, the other can match, while maintaining bisimilarity. Weak bisimilarity accommodates a notion of silent or internal action. A natural class of labelled transition systems is given by considering the derivations of commutative context-free grammars in Greibach Normal Form: the Basic Parallel Processes (BPP), introduced by Christensen in his PhD thesis. They represent a simple model of communication-free parallel computation, and for them bisimilarity is PSPACE-complete. Weak bisimilarity is believed to be decidable, but only partial results exist. Non-bisimilarity is trivially semidecidable on BPP (each process has finitely many next states, so the state space can be explored until a mis-match is found); the research effort in proving it fully decidable centred on semideciding the positive case. Conversely, weak bisimilarity has been known to be semidecidable for a decade, but no method for semideciding inequivalence has yet been found - the presence of silent actions allows a process to have infinitely many possible successor states, so simple exploration is no longer possible. Weak bisimilarity is defined coinductively, but may be approached, and even reached, by its inductively defined approximants. Game theoretically, these change the Defender's winning condition from survival for infinitely many turns to survival for K turns, for an ordinal k, creating a hierarchy of relations successively closer to full weak bisimilarity. It can be seen that on any set of processes this approximant hierarchy collapses: there will always exist some K such that the kth approximant coincides with weak bisimilarity. One avenue towards the semidecidability of non- weak bisimilarity is the decidability of its approximants. It is a long-standing conjecture that on BPP the weak approximant hierarchy collapses at o x 2. If true, in order to semidecide inequivalence it would suffice to be able to decide the o + n approximants. Again, there exist only limited results: the finite approximants are known to be decidable, but no progress has been made on the wth approximant, and thus far the best proven lower-bound of collapse is w1CK (the least non-recursive ordinal number). We significantly improve this bound to okx2(for a k-variable BPP); a key part of the proof being a novel constructive version of Dickson's Lemma. The distances-to-disablings or DD functions were invented by Jancar in order to prove the PSPACE-completeness of bisimilarity on BPP. At the end of his paper is a conjecture that weak bisimilarity might be amenable to the theory; a suggestion we have taken up. We generalise and extend the DD functions, widening the subset of BPP on which weak bisimilarity is known to be computable, and creating a new means for testing inequivalence. The thesis ends with two conjectures. The first, that our extended DD functions in fact capture weak bisimilarity on full BPP (a corollary of which would be to take the lower bound of approximant collapse to and second, that they are computable, which would enable us to semidecide inequivalence, and hence give us the decidability of weak bisimilarity. E-Thesis Computer science. 31 12 2006 2006-12-31 COLLEGE NANME Computer Science COLLEGE CODE Swansea University Doctoral Ph.D 2018-08-02T16:24:29.4625964 2018-08-02T16:24:29.4625964 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science W. J. T Harwood NULL 1 0042496-02082018162459.pdf 10801726.pdf 2018-08-02T16:24:59.0870000 Output 4643347 application/pdf E-Thesis true 2018-08-02T16:24:59.0870000 false
title Towards weak bisimilarity on a class of parallel processes.
spellingShingle Towards weak bisimilarity on a class of parallel processes.
W. J. T Harwood
title_short Towards weak bisimilarity on a class of parallel processes.
title_full Towards weak bisimilarity on a class of parallel processes.
title_fullStr Towards weak bisimilarity on a class of parallel processes.
title_full_unstemmed Towards weak bisimilarity on a class of parallel processes.
title_sort Towards weak bisimilarity on a class of parallel processes.
author_id_str_mv 1a60068903d11c5a551b2ab5bc82def3
author_id_fullname_str_mv 1a60068903d11c5a551b2ab5bc82def3_***_W. J. T Harwood
author W. J. T Harwood
author2 W. J. T Harwood
format E-Thesis
publishDate 2006
institution Swansea University
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description A directed labelled graph may be used, at a certain abstraction, to represent a system's behaviour. Its nodes, the possible states the system can be in; its arrows labelled by the actions required to move from one state to another. Processes are, for our purposes, synonymous with these labelled transition systems. With this view a well-studied notion of behavioural equivalence is bisimilarity, where processes are bisimilar when whatever one can do, the other can match, while maintaining bisimilarity. Weak bisimilarity accommodates a notion of silent or internal action. A natural class of labelled transition systems is given by considering the derivations of commutative context-free grammars in Greibach Normal Form: the Basic Parallel Processes (BPP), introduced by Christensen in his PhD thesis. They represent a simple model of communication-free parallel computation, and for them bisimilarity is PSPACE-complete. Weak bisimilarity is believed to be decidable, but only partial results exist. Non-bisimilarity is trivially semidecidable on BPP (each process has finitely many next states, so the state space can be explored until a mis-match is found); the research effort in proving it fully decidable centred on semideciding the positive case. Conversely, weak bisimilarity has been known to be semidecidable for a decade, but no method for semideciding inequivalence has yet been found - the presence of silent actions allows a process to have infinitely many possible successor states, so simple exploration is no longer possible. Weak bisimilarity is defined coinductively, but may be approached, and even reached, by its inductively defined approximants. Game theoretically, these change the Defender's winning condition from survival for infinitely many turns to survival for K turns, for an ordinal k, creating a hierarchy of relations successively closer to full weak bisimilarity. It can be seen that on any set of processes this approximant hierarchy collapses: there will always exist some K such that the kth approximant coincides with weak bisimilarity. One avenue towards the semidecidability of non- weak bisimilarity is the decidability of its approximants. It is a long-standing conjecture that on BPP the weak approximant hierarchy collapses at o x 2. If true, in order to semidecide inequivalence it would suffice to be able to decide the o + n approximants. Again, there exist only limited results: the finite approximants are known to be decidable, but no progress has been made on the wth approximant, and thus far the best proven lower-bound of collapse is w1CK (the least non-recursive ordinal number). We significantly improve this bound to okx2(for a k-variable BPP); a key part of the proof being a novel constructive version of Dickson's Lemma. The distances-to-disablings or DD functions were invented by Jancar in order to prove the PSPACE-completeness of bisimilarity on BPP. At the end of his paper is a conjecture that weak bisimilarity might be amenable to the theory; a suggestion we have taken up. We generalise and extend the DD functions, widening the subset of BPP on which weak bisimilarity is known to be computable, and creating a new means for testing inequivalence. The thesis ends with two conjectures. The first, that our extended DD functions in fact capture weak bisimilarity on full BPP (a corollary of which would be to take the lower bound of approximant collapse to and second, that they are computable, which would enable us to semidecide inequivalence, and hence give us the decidability of weak bisimilarity.
published_date 2006-12-31T03:53:05Z
_version_ 1763752631415603200
score 11.0241995

Similar Items