@inproceedings{bdebf718ae834625b6e506d9af4f7638,
title = "On automatic verification of self-stabilizing population protocols",
abstract = "The population protocol model [2] has emerged as an elegant computation paradigm for describing mobile ad hoc networks, consisting of a number of mobile nodes that interact with each other to carry out a computation. The interactions of nodes are subject to a fairness constraint. One essential property of population protocols is that all nodes must eventually converge to the correct output value (or configuration). In this paper, we aim to automatically verify self-stabilizing population protocols for leader election and token circulation in the Spin model checker [8]. We report our verification results and discuss the issue of modeling strong fairness constraints in Spin.",
author = "Jun Pang and Zhengqin Luo and Yuxin Deng",
year = "2008",
doi = "10.1109/TASE.2008.8",
language = "英语",
isbn = "9780769532493",
series = "Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008",
pages = "185--192",
booktitle = "Proceedings - 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008",
note = "2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2008 ; Conference date: 17-06-2008 Through 19-06-2008",
}