@article{Gainer+Linker+Dixon+Hustadt+Fisher@arXiv2017,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption
               in Networks of Pulse-Coupled Oscillators},
  journal   = {arXiv},
  volume    = {abs/1709.04385},
  year      = {2017},
  url       = {http://arxiv.org/abs/1709.04385},
  abstract  = {We assess the power consumption of network synchronisation protocols,
  particularly the energy required to synchronise all nodes across a
  network. We use the widely adopted approach of bio-inspired,
  pulse-coupled oscillators to achieve network-wide synchronisation and
  provide an extended formal model of just such a protocol, enhanced
  with structures for recording energy usage. Exhaustive analysis is
  then carried out through formal verification, utilising the PRISM
  model checker to calculate the resources consumed on each possible
  system execution. This allows us to assess a range of parameter
  instantiations and to explore trade-offs between power consumption and
  time to synchronise. This provides a principled basis for the formal
  analysis of a much broader range of large-scale network protocols.}
}

{"_id":"2WZSSA986TLNh7Xj7","bibbaseid":"gainer-linker-dixon-hustadt-fisher-thepowerofsynchronisationformalanalysisofpowerconsumptioninnetworksofpulsecoupledoscillators-2017","downloads":0,"creationDate":"2018-04-02T20:55:30.121Z","title":"The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators","author_short":["Gainer, P.","Linker, S.","Dixon, C.","Hustadt, U.","Fisher, M."],"year":2017,"bibtype":"article","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Paul"],"propositions":[],"lastnames":["Gainer"],"suffixes":[]},{"firstnames":["Sven"],"propositions":[],"lastnames":["Linker"],"suffixes":[]},{"firstnames":["Clare"],"propositions":[],"lastnames":["Dixon"],"suffixes":[]},{"firstnames":["Ullrich"],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["Michael"],"propositions":[],"lastnames":["Fisher"],"suffixes":[]}],"title":"The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators","journal":"arXiv","volume":"abs/1709.04385","year":"2017","url":"http://arxiv.org/abs/1709.04385","abstract":"We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis is then carried out through formal verification, utilising the PRISM model checker to calculate the resources consumed on each possible system execution. This allows us to assess a range of parameter instantiations and to explore trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a much broader range of large-scale network protocols.","bibtex":"@article{Gainer+Linker+Dixon+Hustadt+Fisher@arXiv2017,\n author = {Paul Gainer and\n Sven Linker and\n Clare Dixon and\n Ullrich Hustadt and\n Michael Fisher},\n title = {The Power of Synchronisation: Formal Analysis of Power Consumption\n in Networks of Pulse-Coupled Oscillators},\n journal = {arXiv},\n volume = {abs/1709.04385},\n year = {2017},\n url = {http://arxiv.org/abs/1709.04385},\n abstract = {We assess the power consumption of network synchronisation protocols,\n particularly the energy required to synchronise all nodes across a\n network. We use the widely adopted approach of bio-inspired,\n pulse-coupled oscillators to achieve network-wide synchronisation and\n provide an extended formal model of just such a protocol, enhanced\n with structures for recording energy usage. Exhaustive analysis is\n then carried out through formal verification, utilising the PRISM\n model checker to calculate the resources consumed on each possible\n system execution. This allows us to assess a range of parameter\n instantiations and to explore trade-offs between power consumption and\n time to synchronise. This provides a principled basis for the formal\n analysis of a much broader range of large-scale network protocols.}\n}\n\n","author_short":["Gainer, P.","Linker, S.","Dixon, C.","Hustadt, U.","Fisher, M."],"key":"Gainer+Linker+Dixon+Hustadt+Fisher@arXiv2017","id":"Gainer+Linker+Dixon+Hustadt+Fisher@arXiv2017","bibbaseid":"gainer-linker-dixon-hustadt-fisher-thepowerofsynchronisationformalanalysisofpowerconsumptioninnetworksofpulsecoupledoscillators-2017","role":"author","urls":{"Paper":"http://arxiv.org/abs/1709.04385"},"metadata":{"authorlinks":{"linker, s":"https://cgi.csc.liv.ac.uk/~slk/index.php","hustadt, u":"https://cgi.csc.liv.ac.uk/~ullrich/publications/"}},"downloads":0},"search_terms":["power","synchronisation","formal","analysis","power","consumption","networks","pulse","coupled","oscillators","gainer","linker","dixon","hustadt","fisher"],"keywords":[],"authorIDs":["DJofX33ALvdrbndrr","aQLR39RKeqjQcByRb"],"dataSources":["sf65xF3tXwz6TBuoQ","77JvGFZQteoFsRiyX","WhiGijHmCtTSdLaAj","iqRbmbCgpDeaBjend","FgmYE34DdKWThg2dR","viaGT23rwj7vKvjeq"]}