An Algebraic Approach to Refinement with Fair Choice. Sekerinski, E. In Boiten, E., Derrick, J., & Schellhorn, G., editors, Proceedings of the 13th BAC-FACS Refinement Workshop (REFINE 2008), volume 214, of Electronic Notes in Theoretical Computer Science, pages 51–79, June, 2008. Elsevier. doi abstract bibtex 1 download In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.
@inproceedings{Sekerinski08AlgebraicFairChoice,
series = {Electronic {Notes} in {Theoretical} {Computer} {Science}},
title = {An {Algebraic} {Approach} to {Refinement} with {Fair} {Choice}},
volume = {214},
doi = {http://dx.doi.org/10.1016/j.entcs.2008.06.004},
abstract = {In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.},
booktitle = {Proceedings of the 13th {BAC}-{FACS} {Refinement} {Workshop} ({REFINE} 2008)},
publisher = {Elsevier},
author = {Sekerinski, Emil},
editor = {Boiten, E. and Derrick, J. and Schellhorn, G.},
month = jun,
year = {2008},
keywords = {action systems, alternating bit protocol, fairness, refinement},
pages = {51--79},
}
Downloads: 1
{"_id":"itQateiCR4SAi9hLh","bibbaseid":"sekerinski-analgebraicapproachtorefinementwithfairchoice-2008","downloads":1,"creationDate":"2019-02-02T15:48:53.589Z","title":"An Algebraic Approach to Refinement with Fair Choice","author_short":["Sekerinski, E."],"year":2008,"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Electronic Notes in Theoretical Computer Science","title":"An Algebraic Approach to Refinement with Fair Choice","volume":"214","doi":"http://dx.doi.org/10.1016/j.entcs.2008.06.004","abstract":"In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.","booktitle":"Proceedings of the 13th BAC-FACS Refinement Workshop (REFINE 2008)","publisher":"Elsevier","author":[{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Boiten"],"firstnames":["E."],"suffixes":[]},{"propositions":[],"lastnames":["Derrick"],"firstnames":["J."],"suffixes":[]},{"propositions":[],"lastnames":["Schellhorn"],"firstnames":["G."],"suffixes":[]}],"month":"June","year":"2008","keywords":"action systems, alternating bit protocol, fairness, refinement","pages":"51–79","bibtex":"@inproceedings{Sekerinski08AlgebraicFairChoice,\n\tseries = {Electronic {Notes} in {Theoretical} {Computer} {Science}},\n\ttitle = {An {Algebraic} {Approach} to {Refinement} with {Fair} {Choice}},\n\tvolume = {214},\n\tdoi = {http://dx.doi.org/10.1016/j.entcs.2008.06.004},\n\tabstract = {In the analysis and design of concurrent systems, it can be useful to assume fairness among processes. Action systems model a process by a set of atomic actions. Typically, actions are combined by nondeterministic choice, which models minimal progress among processes rather than fairness. Here we define an operator for the fair choice among a set of actions. A refinement rule for action systems with fair choice is derived and applied to the development of the alternating bit protocol. The novelty is the algebraic style in which the fair choice operator is defined and in which formal reasoning is carried out; it avoids an appeal to the operational understanding of fairness.},\n\tbooktitle = {Proceedings of the 13th {BAC}-{FACS} {Refinement} {Workshop} ({REFINE} 2008)},\n\tpublisher = {Elsevier},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Boiten, E. and Derrick, J. and Schellhorn, G.},\n\tmonth = jun,\n\tyear = {2008},\n\tkeywords = {action systems, alternating bit protocol, fairness, refinement},\n\tpages = {51--79},\n}\n\n","author_short":["Sekerinski, E."],"editor_short":["Boiten, E.","Derrick, J.","Schellhorn, G."],"key":"Sekerinski08AlgebraicFairChoice","id":"Sekerinski08AlgebraicFairChoice","bibbaseid":"sekerinski-analgebraicapproachtorefinementwithfairchoice-2008","role":"author","urls":{},"keyword":["action systems","alternating bit protocol","fairness","refinement"],"metadata":{"authorlinks":{}},"downloads":1},"search_terms":["algebraic","approach","refinement","fair","choice","sekerinski"],"keywords":["action systems","alternating bit protocol","fairness","refinement"],"authorIDs":[],"dataSources":["fDYYrPxpzcyDvQK6b","HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","RfxodDQazHHccThPz","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"]}