@inproceedings{conf/sss/JubranMT15,
Author = {Oday Jubran and Eike Möhlmann and Oliver E. Theel},
Title = {Verifying Recurrence Properties in Self-Stabilization by Checking the Absence of Finite Counterexamples},

Year = {2015},
Pages = {124-138},
Editor = {Andrzej Pelc and Alexander A. Schwarzmann},
Publisher = {Springer-Verlag},
Series = {Lecture Notes in Computer Science (LNCS)},
Edition = {9212},
Booktitle = {Stabilization, Safety, and Security of Distributed Systems - 17th International Symposium, {SSS} 2015},
Doi = {10.1007/978-3-319-21741-3_9},
Url = {http://dx.doi.org/10.1007/978-3-319-21741-3_9},
type = {inproceedings},
note = {A performance-related property of a system can be defined as the ratio of states satisfying some condition in each execution of the system, which we signify as the recurrence of the condition in the execution. In this work, we concern self-stabilization w},
Abstract = {A performance-related property of a system can be defined as the ratio of states satisfying some condition in each execution of the system, which we signify as the recurrence of the condition in the execution. In this work, we concern self-stabilization with respect to this property: the convergence to an execution that guarantees a minimum recurrence of a condition. For a system exhibiting infinite executions, it may not be straightforward to verify that the system satisfies the property, while considering the convergence as well. Towards simplifying such a verification, we show that for each system violating the property, there exists a finite execution prefix that is a counterexample with a reasonably short length. Furthermore, we exploit model checking to verify the absence of such counterexamples, to conclude that a system satisfies its property. We apply this approach by using the nuXmv model checker to analyze the service time of a self-stabilizing mutual exclusion algorithm having a finite state space, and running over many topologies.}
}
@COMMENT{Bibtex file generated on }