{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,2]],"date-time":"2024-08-02T23:36:38Z","timestamp":1722641798392},"reference-count":37,"publisher":"Elsevier BV","issue":"20","license":[{"start":{"date-parts":[[2010,4,1]],"date-time":"2010-04-01T00:00:00Z","timestamp":1270080000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2014,4,28]],"date-time":"2014-04-28T00:00:00Z","timestamp":1398643200000},"content-version":"vor","delay-in-days":1488,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1016\/j.tcs.2009.12.019","type":"journal-article","created":{"date-parts":[[2010,1,7]],"date-time":"2010-01-07T04:16:40Z","timestamp":1262837800000},"page":"1999-2018","source":"Crossref","is-referenced-by-count":18,"title":["Detecting synchronisation of biological oscillators by model checking"],"prefix":"10.1016","volume":"411","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[]},{"given":"Flavio","family":"Corradini","sequence":"additional","affiliation":[]},{"given":"Emanuela","family":"Merelli","sequence":"additional","affiliation":[]},{"given":"Luca","family":"Tesei","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/j.tcs.2009.12.019_b1","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1086\/415929","article-title":"Synchronous rhythmic flashing of fireflies II","volume":"63","author":"Buck","year":"1988","journal-title":"The Quarterly Review of Biology"},{"key":"10.1016\/j.tcs.2009.12.019_b2","unstructured":"C.S. Peskin, Mathematical aspects of heart physiology, Courant Institute of Mathematical Sciences, New York University, New York, 1975"},{"issue":"5","key":"10.1016\/j.tcs.2009.12.019_b3","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BF00215074","article-title":"Ionic and synaptic mechanisms underlying a brainstem oscillator: An in vitro study of the pacemaker nucleus of apteronotus","volume":"168","author":"Dye","year":"1991","journal-title":"Journal of Comparative Physiology"},{"key":"10.1016\/j.tcs.2009.12.019_b4","series-title":"Sync, The Emerging Science of Spontaneous Order","author":"Strogatz","year":"2004"},{"key":"10.1016\/j.tcs.2009.12.019_b5","series-title":"Foundations of Systems Biology","author":"Kitano","year":"2002"},{"issue":"6","key":"10.1016\/j.tcs.2009.12.019_b6","doi-asserted-by":"crossref","first-page":"1182","DOI":"10.1143\/PTP.71.1182","article-title":"Phase dynamics of weakly unstable periodic structures: Condensed matter and statistical physics","volume":"71","author":"Kuramoto","year":"1984","journal-title":"Progress of Theoretical Physics"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b7","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0022-5193(67)90051-3","article-title":"Biological rhythms and the behavior of populations of coupled oscillators","volume":"16","author":"Winfree","year":"1967","journal-title":"Journal of Theoretical Biology"},{"issue":"14","key":"10.1016\/j.tcs.2009.12.019_b8","doi-asserted-by":"crossref","first-page":"1775","DOI":"10.1093\/bioinformatics\/btl182","article-title":"Synchronizing a multicellular system by external input: an artificial control strategy","volume":"22","author":"Wang","year":"2006","journal-title":"Bioinformatics"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b9","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1103\/RevModPhys.77.137","article-title":"The Kuramoto model: A simple paradigm for synchronization phenomena","volume":"77","author":"Acebron","year":"2005","journal-title":"Reviews of Modern Physics"},{"key":"10.1016\/j.tcs.2009.12.019_b10","unstructured":"C.S. Peskin, Mathematical Aspects of Heart Physiology, Courant Institute of Mathematical Sciences, 1975"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.entcs.2009.02.004","article-title":"Model checking biological oscillators","volume":"229","author":"Bartocci","year":"2009","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b12","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/0167-2789(91)90075-K","article-title":"Collective synchronization of pulse-coupled oscillators and excitable units","volume":"50","author":"Kuramoto","year":"1991","journal-title":"Physica D"},{"issue":"6","key":"10.1016\/j.tcs.2009.12.019_b13","doi-asserted-by":"crossref","first-page":"1645","DOI":"10.1137\/0150098","article-title":"Synchronization of pulse-coupled biological oscillators","volume":"50","author":"Mirollo","year":"1990","journal-title":"SIAM Journal of Applied Mathematics"},{"key":"10.1016\/j.tcs.2009.12.019_b14","series-title":"Chemical Oscillations, Waves, and Turbulence","author":"Kuramoto","year":"2003"},{"issue":"6","key":"10.1016\/j.tcs.2009.12.019_b15","doi-asserted-by":"crossref","first-page":"1645","DOI":"10.1137\/0150098","article-title":"Synchronization of pulse-coupled biological oscillators","volume":"50","author":"Mirollo","year":"1990","journal-title":"SIAM Journal of Applied Mathematics"},{"issue":"2","key":"10.1016\/j.tcs.2009.12.019_b16","doi-asserted-by":"crossref","first-page":"1483","DOI":"10.1103\/PhysRevE.48.1483","article-title":"Asynchronous states in networks of pulse-coupled oscillators","volume":"48","author":"Abbott","year":"1993","journal-title":"Physical Review E"},{"issue":"2","key":"10.1016\/j.tcs.2009.12.019_b17","doi-asserted-by":"crossref","first-page":"2160","DOI":"10.1103\/PhysRevE.60.2160","article-title":"Mean-field theory of globally coupled integrate-and-fire neural oscillators with dynamic synapses","volume":"60","author":"Bressloff","year":"1999","journal-title":"Physical Review E"},{"key":"10.1016\/j.tcs.2009.12.019_b18","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1162\/089976600300015529","article-title":"The number of synaptic inputs and the synchrony of large, sparse neuronal networks","volume":"12","author":"Golomb","year":"2000","journal-title":"Neural Computation"},{"key":"10.1016\/j.tcs.2009.12.019_b19","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2009.12.019_b20","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/j.tcs.2009.12.019_b21","series-title":"HART \u201997: Proceedings of the International Workshop on Hybrid and Real-Time Systems","first-page":"331","article-title":"Robust timed automata","author":"Gupta","year":"1997"},{"issue":"4","key":"10.1016\/j.tcs.2009.12.019_b22","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1093\/logcom\/12.4.607","article-title":"Extending CTL with actions and real time","volume":"12","author":"Jansen","year":"2002","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/j.tcs.2009.12.019_b23","series-title":"Proceedings of the DIMACS\/SYCON Workshop on Hybrid Systems III: Verification and control","first-page":"208","article-title":"The tool kronos","author":"Daws","year":"1996"},{"key":"10.1016\/j.tcs.2009.12.019_b24","series-title":"Proc. of Fundamentals of Computation Theory","first-page":"62","article-title":"Model-checking for real-time systems","volume":"vol. 965","author":"Larsen","year":"1995"},{"key":"10.1016\/j.tcs.2009.12.019_b25","series-title":"Formal Methods for the Design of Real-Time Systems, SFM-RT 2004","first-page":"200","article-title":"A tutorial on uppaal","volume":"vol. 3185","author":"Behrmann","year":"2004"},{"key":"10.1016\/j.tcs.2009.12.019_b26","series-title":"FMSB","first-page":"77","article-title":"Approximating continuous systems by timed automata","volume":"vol. 5054","author":"Maler","year":"2008"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b27","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1076\/1387-3954(200003)6:1;1-Q;FT051","article-title":"On the generation of timed discrete approximations for continuous systems","volume":"6","author":"Stursberg","year":"2000","journal-title":"Mathematical and Computer Modelling of Dynamical Systems"},{"key":"10.1016\/j.tcs.2009.12.019_b28","doi-asserted-by":"crossref","unstructured":"A. Olivero, J. Sifakis, S. Yovine, Using abstractions for the verification of linear hybrid systems, in: CAV, 1994, pp. 81\u201394","DOI":"10.1007\/3-540-58179-0_45"},{"key":"10.1016\/j.tcs.2009.12.019_b29","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, The theory of hybrid automata, in: LICS, 1996, pp. 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"10.1016\/j.tcs.2009.12.019_b30","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, in: FOCS, 1977, pp. 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"issue":"4","key":"10.1016\/j.tcs.2009.12.019_b31","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans","year":"1990","journal-title":"Real-Time Systems"},{"issue":"1","key":"10.1016\/j.tcs.2009.12.019_b32","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","article-title":"A really temporal logic","volume":"41","author":"Alur","year":"2004","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.tcs.2009.12.019_b33","unstructured":"E. Bartocci, F. Corradini, E. Merelli, L. Tesei, BOSL model checker prototype, URL http:\/\/cosy.cs.unicam.it\/bosl\/"},{"key":"10.1016\/j.tcs.2009.12.019_b34","series-title":"Numerical Methods for Ordinary Differential Equations","author":"Butcher","year":"2003"},{"key":"10.1016\/j.tcs.2009.12.019_b35","doi-asserted-by":"crossref","unstructured":"M. Bozga, S. Graf, L. Mounier, If-2.0: A validation environment for component-based real-time systems, CAV, 2002, pp. 343\u2013348","DOI":"10.1007\/3-540-45657-0_26"},{"key":"10.1016\/j.tcs.2009.12.019_b36","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1161\/01.RES.46.1.11","article-title":"Functional and morphological organization of the rabbit sinus node","volume":"46","author":"Bleeker","year":"1980","journal-title":"Circulation Research"},{"key":"10.1016\/j.tcs.2009.12.019_b37","series-title":"Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday","first-page":"493","article-title":"Stonycam: A formal framework for modeling, analyzing and regulating cardiac myocytes","volume":"vol. 5065","author":"Bartocci","year":"2008"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750900855X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750900855X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T20:13:46Z","timestamp":1558728826000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439750900855X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4]]},"references-count":37,"journal-issue":{"issue":"20","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["S030439750900855X"],"URL":"http:\/\/dx.doi.org\/10.1016\/j.tcs.2009.12.019","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2010,4]]}}}
