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
-
PDF | E-Thesis
Download (4.49MB)
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...
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 |