Finitary Fairness in Action Systems. Sekerinski, E. & Zhang, T. In Liu, Z., Woodcock, J., & Zhu, H., editors, Theoretical Aspects of Computing–ICTAC 2013, 10th International Colloquium, volume 8049, of Lecture Notes in Computer Science, pages 319–336, September, 2013. Springer. ![Finitary Fairness in Action Systems [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper doi abstract bibtex In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.
@inproceedings{SekerinskiZhang13FinitaryFairness,
series = {Lecture {Notes} in {Computer} {Science}},
title = {Finitary {Fairness} in {Action} {Systems}},
volume = {8049},
isbn = {978-3-642-39717-2},
url = {http://dx.doi.org/10.1007/978-3-642-39718-9_19},
doi = {10.1007/978-3-642-39718-9_19},
abstract = {In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.},
booktitle = {Theoretical {Aspects} of {Computing}–{ICTAC} 2013, 10th {International} {Colloquium}},
publisher = {Springer},
author = {Sekerinski, Emil and Zhang, Tian},
editor = {Liu, Zhiming and Woodcock, Jim and Zhu, Huibiao},
month = sep,
year = {2013},
keywords = {Event-B, Finitary Fairness, Modelling, Stepwise Refinement, Termination},
pages = {319--336},
}
Downloads: 0
{"_id":"re7QJoCDgatgyf9jq","bibbaseid":"sekerinski-zhang-finitaryfairnessinactionsystems-2013","author_short":["Sekerinski, E.","Zhang, T."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","series":"Lecture Notes in Computer Science","title":"Finitary Fairness in Action Systems","volume":"8049","isbn":"978-3-642-39717-2","url":"http://dx.doi.org/10.1007/978-3-642-39718-9_19","doi":"10.1007/978-3-642-39718-9_19","abstract":"In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.","booktitle":"Theoretical Aspects of Computing–ICTAC 2013, 10th International Colloquium","publisher":"Springer","author":[{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]},{"propositions":[],"lastnames":["Zhang"],"firstnames":["Tian"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Liu"],"firstnames":["Zhiming"],"suffixes":[]},{"propositions":[],"lastnames":["Woodcock"],"firstnames":["Jim"],"suffixes":[]},{"propositions":[],"lastnames":["Zhu"],"firstnames":["Huibiao"],"suffixes":[]}],"month":"September","year":"2013","keywords":"Event-B, Finitary Fairness, Modelling, Stepwise Refinement, Termination","pages":"319–336","bibtex":"@inproceedings{SekerinskiZhang13FinitaryFairness,\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {Finitary {Fairness} in {Action} {Systems}},\n\tvolume = {8049},\n\tisbn = {978-3-642-39717-2},\n\turl = {http://dx.doi.org/10.1007/978-3-642-39718-9_19},\n\tdoi = {10.1007/978-3-642-39718-9_19},\n\tabstract = {In basic action systems, the choice among actions is not restricted. Fairness can be imposed to restrict this nondeterminism. Finitary fairness has been proposed as a further restriction of fairness: it models implementations closer, and allows problems to be solved for which standard fairness is not sufficient. We propose a method for expressing finitary fairness in action systems. We give two general transformations from a system in which some actions are marked as fair, into an equivalent system without fair actions. A theoretical justification is given, and the transformations are illustrated with two examples: alternating bit protocol and distributed consensus. The examples are developed by stepwise refinement in Event-B and are mechanically checked.},\n\tbooktitle = {Theoretical {Aspects} of {Computing}–{ICTAC} 2013, 10th {International} {Colloquium}},\n\tpublisher = {Springer},\n\tauthor = {Sekerinski, Emil and Zhang, Tian},\n\teditor = {Liu, Zhiming and Woodcock, Jim and Zhu, Huibiao},\n\tmonth = sep,\n\tyear = {2013},\n\tkeywords = {Event-B, Finitary Fairness, Modelling, Stepwise Refinement, Termination},\n\tpages = {319--336},\n}\n\n","author_short":["Sekerinski, E.","Zhang, T."],"editor_short":["Liu, Z.","Woodcock, J.","Zhu, H."],"key":"SekerinskiZhang13FinitaryFairness","id":"SekerinskiZhang13FinitaryFairness","bibbaseid":"sekerinski-zhang-finitaryfairnessinactionsystems-2013","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/978-3-642-39718-9_19"},"keyword":["Event-B","Finitary Fairness","Modelling","Stepwise Refinement","Termination"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","ienufKdnmJs49AsjR","So4gmSWFmbQRNEuFs","ezsmw4w22u9JFLNYJ","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":["event-b","finitary fairness","modelling","stepwise refinement","termination"],"search_terms":["finitary","fairness","action","systems","sekerinski","zhang"],"title":"Finitary Fairness in Action Systems","year":2013}