Skip to main content
SpringerLink
Log in

Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption

  • Conference paper
Analytical and Stochastic Modeling Techniques and Applications (ASMTA 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6148))

Abstract

Leader election has been studied intensively in recent years. In this paper, we present an analysis of a randomized leader election using probabilistic model checking with PRISM. We first investigate the quantitative properties of the original protocol such as the expected number of election rounds. Then we modify the protocol so that it consumes less energy and processes with larger energy have higher chance to be elected. The modified protocol is modeled as Markov Decision Process, which allow us to compute minimum and maximum values, interpreting the best- and worst-case performance of the protocol under any scenario.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Bordim, J.L., Ito, Y., Nakano, K.: Randomized leader election protocols in noisy radio networks with a single transceiver. In: Guo, M., Yang, L.T., Di Martino, B., Zima, H.P., Dongarra, J., Tang, F. (eds.) ISPA 2006. LNCS, vol. 4330, pp. 246–256. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Brunekreef, J., Katoen, J.-P., Koymans, R., Mauw, S.: Design and analysis of dynamic leader election protocols in broadcast networks. Distributed Computing 9(4), 157–171 (1996)

    Article  Google Scholar 

  4. Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)

    Article  Google Scholar 

  5. Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: International Workshop on Logic Synthesis (IWLS), pp. 1–15 (1993)

    Google Scholar 

  6. de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic processes using MTBDDs and the kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Fokkink, W., Pang, J.: Simplifying Itai-Rodeh leader election for anonymous rings. In: Automated Verification of Critical Systems (AVoCS), vol. 128, pp. 53–68 (2004)

    Google Scholar 

  8. Fokkink, W., Pang, J.: Variations on Itai-Rodeh leader election for anonymous rings and their analysis in PRISM. Journal of Universal Computer Science 12, 981–1006 (2006)

    Google Scholar 

  9. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. In: Formal Aspect of Computing, pp. 512–535 (1994)

    Google Scholar 

  10. Jongerden, M.R., Haverkort, B.R., Bohnenkamp, H., Katoen, J.-P.: Maximizing system lifetime by battery scheduling. In: International Conference on Dependable Systems and Networks, pp. 63–77 (2009)

    Google Scholar 

  11. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Int. Conf. on the Quantitative Evaluation of Systems (QEST), pp. 167–176 (2009)

    Google Scholar 

  12. Le Lann, G.: Distributed systems: Towards a formal approach. In: Information Processing 77, Proc. of the IFIP Congress, pp. 155–160 (1977)

    Google Scholar 

  13. Herault, T., Lassaigne, R., Magniette, F., Messika, S., Peyronnet, S., Duflot, M., Fribourg, L., Picaronny, C.: Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC. In: Automated Verification of Critical Systems (AVoCS), ENTCS, vol. 128, pp. 195–214 (2004)

    Google Scholar 

  14. Norman, G., Kwiatkowska, M., Parker, D.: Analysis of a gossip protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review 36, 17–22 (2008)

    Article  Google Scholar 

  15. Malpani, N., Welch, J.L., Vaidya, N.: Leader election algorithms for mobile ad hoc networks. In: Discrete Algorithms and Methods for Mobile Computing and Communications, pp. 96–103. ACM, New York (2000)

    Google Scholar 

  16. Miller, M.J., Vaidya, N.H.: Minimizing energy consumption in sensor networks using a wakeup radio. In: Wireless Communications and Networking Conference (WCNC), vol. 4, pp. 2335–2340 (2004)

    Google Scholar 

  17. Romijn, J.: A timed verification of the IEEE 1394 leader election protocol. Formal Methods in System Design 19(2), 165–194 (2001)

    Article  MATH  Google Scholar 

  18. Romijn, J.M.T.: Model checking the HAVi leader election protocol (1999)

    Google Scholar 

  19. Nordic Semiconductors. nRF2401 Single-chip 2.4GHz Transceiver Data Sheet (2002)

    Google Scholar 

  20. Shnayder, V., Hempstead, M., Chen, B., Allen, G.W., Welsh, M.: Simulating the power consumption of large-scale sensor network applications. In: Int. Conf. on Embedded Networked Sensor Systems, pp. 188–200. ACM, New York (2004)

    Chapter  Google Scholar 

  21. Tel, G.: Introduction to Distributed Algorithms. Cambridge University Press, Cambridge (2000)

    MATH  Google Scholar 

  22. Tiliute, D.E.: Battery management in wireless sensor networks. Electronics and Electrical Engineering 4(76), 9–12 (2007)

    Google Scholar 

  23. Vasudevan, S., Kurose, J., Towsley, D.: Design and analysis of a leader election algorithm for mobile ad hoc networks. In: Int. Conf. on Network Protocols (ICNP), pp. 350–360 (2004)

    Google Scholar 

  24. MRMC website. http://www.mrmc-tool.org/trac/

  25. PRISM website, http://www.prismmodelchecker.org

  26. VESTA website, http://osl.cs.uiuc.edu/~ksen/vesta2/

Download references

Author information

Authors and Affiliations

  1. Software Modeling & Verification Group, RWTH Aachen University, D-52056, Aachen, Germany

    Haidi Yue & Joost-Pieter Katoen

Authors
  1. Haidi Yue
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Advanced Technology, University of Glamorgan, CF37 1DL, Pontypridd, UK

    Khalid Al-Begain

  2. Department TELIN, Ghent University, Sint-Pietersnieuwstraat 41, 9000, Gent, Belgium

    Dieter Fiems

  3. Department of Computing,, Imperial College London, South Kensington Campus, SW7 2AZ, London, United Kingdom

    William J. Knottenbelt

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yue, H., Katoen, JP. (2010). Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. In: Al-Begain, K., Fiems, D., Knottenbelt, W.J. (eds) Analytical and Stochastic Modeling Techniques and Applications. ASMTA 2010. Lecture Notes in Computer Science, vol 6148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13568-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-13568-2_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-13567-5

  • Online ISBN: 978-3-642-13568-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation