{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:09:11Z","timestamp":1748750951141,"version":"3.41.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251400"},{"type":"electronic","value":"9783319251417"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25141-7_7","type":"book-chapter","created":{"date-parts":[[2015,10,31]],"date-time":"2015-10-31T08:51:25Z","timestamp":1446281485000},"page":"83-98","source":"Crossref","is-referenced-by-count":8,"title":["Recharging Probably Keeps Batteries Alive"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[]},{"given":"Gilles","family":"Nies","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,1]]},"reference":[{"issue":"11","key":"7_CR1","doi-asserted-by":"publisher","first-page":"2724","DOI":"10.1016\/j.automatica.2008.03.027","volume":"44","author":"A Abate","year":"2008","unstructured":"Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724\u20132734 (2008)","journal-title":"Automatica"},{"issue":"6","key":"7_CR2","doi-asserted-by":"publisher","first-page":"2070","DOI":"10.1137\/S0363012995279985","volume":"35","author":"E Altman","year":"1997","unstructured":"Altman, E., Gaitsgory, V.: Asymptotic optimization of a nonlinear hybrid system governed by a markov decision process. SIAM J. Control Optim. 35(6), 2070\u20132085 (1997)","journal-title":"SIAM J. Control Optim."},{"key":"7_CR3","first-page":"95","volume":"2001","author":"H Aydin","year":"2001","unstructured":"Aydin, H., Mej\u00eda-Alvarez, P., Moss\u00e9, D., Melhem, R.G.: Dynamic and aggressive scheduling techniques for power-aware real-time systems. IEEE RTSS 2001, 95\u2013105 (2001)","journal-title":"IEEE RTSS"},{"key":"7_CR4","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","DOI":"10.1007\/11587392","volume-title":"Stochastic Hybrid Systems: Theory and Safety Critical Applications","author":"HA Blom","year":"2006","unstructured":"Blom, H.A., Lygeros, J., Everdij, M., Loizou, S., Kyriakopoulos, K.: Stochastic Hybrid Systems: Theory and Safety Critical Applications. LNCS, vol. 337. Springer, Heidelberg (2006)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Boker, U., Henzinger, T.A., Radhakrishna, A.: Battery transition systems. In: POPL, pp. 595\u2013606. ACM (2014)","DOI":"10.1145\/2535838.2535875"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-540-31954-2_13","volume-title":"Hybrid Systems: Computation and Control","author":"ML Bujorianu","year":"2005","unstructured":"Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for general stochastic hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198\u2013214. Springer, Heidelberg (2005)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Cao, J., Schofield, N., Emadi, A.: Battery balancing methods: a comprehensive review. In: Vehicle Power and Propulsion Conference, VPPC 2008, pp. 1\u20136. IEEE, September 2008","DOI":"10.1109\/VPPC.2008.4677669"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Cloth, L., Jongerden, M.R., Haverkort, B.R.: Computing battery lifetime distributions. In: DSN, pp. 780\u2013789. IEEE Computer Society (2007)","DOI":"10.1109\/DSN.2007.26"},{"issue":"1","key":"7_CR9","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BF02124750","volume":"5","author":"RM Corless","year":"1996","unstructured":"Corless, R.M., Gonnet, G.H., Hare, D.E.G., Jeffrey, D.J., Knuth, D.E.: On the lambertW function. Adv. Comput. Math. 5(1), 329\u2013359 (1996)","journal-title":"Adv. Comput. Math."},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1111\/j.2517-6161.1984.tb01308.x","volume":"46","author":"MH Davis","year":"1984","unstructured":"Davis, M.H.: Piecewise-deterministic markov processes: a general class of non-diffusion stochastic models. J. Roy. Stat. Soc. Ser. B (Methodol.) 46, 353\u2013388 (1984)","journal-title":"J. Roy. Stat. Soc. Ser. B (Methodol.)"},{"key":"7_CR11","unstructured":"Esa: Esa cubesat program, October 2014. http:\/\/www.esa.int\/Education\/CubeSats"},{"key":"7_CR12","series-title":"LNCS","first-page":"272","volume-title":"TACAS 2015","author":"SEZ Soudjani","year":"2015","unstructured":"Soudjani, S.E.Z., Gevaerts, C., Abate, A.: Faust2: formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272\u2013286. Springer, Heidelberg (2015)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Fox, M., Long, D., Magazzeni, D.: Automatic construction of efficient multiple battery usage policies. In: Walsh, T. (ed.) IJCAI, pp. 2620\u20132625. IJCAI\/AAAI (2011)","DOI":"10.1609\/icaps.v21i1.13453"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43\u201352. ACM Press, New York, NY, USA (2011)","DOI":"10.1145\/1967701.1967710"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-78929-1_13","volume-title":"Hybrid Systems: Computation and Control","author":"M Fr\u00e4nzle","year":"2008","unstructured":"Fr\u00e4nzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172\u2013186. Springer, Heidelberg (2008)"},{"key":"7_CR16","unstructured":"Gilles, P.: Private communication (2014)"},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/0021-9991(76)90041-3","volume":"22","author":"DT Gillespie","year":"1976","unstructured":"Gillespie, D.T.: A general method for numerically simulating the stochastic time evolution of coupled chemical reactions. J. Comput. Phys. 22(4), 403\u2013434 (1976)","journal-title":"J. Comput. Phys."},{"key":"7_CR18","unstructured":"GomSpace: Gomspace gomx-1, October 2014. http:\/\/gomspace.com\/?p=gomx1"},{"key":"7_CR19","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Kemal Inan, M., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11813040_1","volume-title":"FM 2006: Formal Methods","author":"TA Henzinger","year":"2006","unstructured":"Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 1\u201315. Springer, Heidelberg (2006)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Krc\u00e1l, J., Nies, G.: Recharging probably keeps batteries alive. CoRR abs\/1502.07120 (2015)","DOI":"10.1007\/978-3-319-25141-7_7"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Jongerden, M., Haverkort, B., Bohnenkamp, H., Katoen, J.: Maximizing system lifetime by battery scheduling. In: DSN, pp. 63\u201372. IEEE (2009)","DOI":"10.1109\/DSN.2009.5270351"},{"issue":"6","key":"7_CR23","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1049\/iet-sen.2009.0001","volume":"3","author":"MR Jongerden","year":"2009","unstructured":"Jongerden, M.R., Haverkort, B.R.: Which battery model to use? IET Softw. 3(6), 445\u2013457 (2009)","journal-title":"IET Softw."},{"key":"7_CR24","unstructured":"Jongerden, M.R.: Model-based energy analysis of battery powered systems. Ph.d. thesis, Enschede, December 2010"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"874","DOI":"10.1016\/S0378-7753(03)00196-4","volume":"119","author":"BY Liaw","year":"2003","unstructured":"Liaw, B.Y., Roth, E.P., Jungst, R.G., Nagasubramanian, G., Case, H.L., Doughty, D.H.: Correlation of arrhenius behaviors in power and capacity fades with cell impedance and heat generation in cylindrical lithium-ion cells. J. Power Sources 119, 874\u2013886 (2003)","journal-title":"J. Power Sources"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Liu, J., Chou, P.H., Bagherzadeh, N., Kurdahi, F.: Power-aware scheduling under timing constraints for mission-critical embedded systems. In: DAC, pp. 840\u2013845. ACM, New York, NY, USA (2001)","DOI":"10.1145\/378239.379076"},{"issue":"5","key":"7_CR27","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/0038-092X(93)90060-2","volume":"50","author":"JF Manwell","year":"1993","unstructured":"Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Sol. Energy 50(5), 399\u2013405 (1993)","journal-title":"Sol. Energy"},{"key":"7_CR28","unstructured":"Rao, V., Singhal, G., Kumar, A., Navet, N.: Battery model for embedded systems. In: VLSI Design\/ES Design, pp. 105\u2013110. IEEE (2005)"},{"key":"7_CR29","unstructured":"SENSATION: Sensation, March 2015. http:\/\/www.sensation-project.eu\/"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 31. Springer, Heidelberg (2000)"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Vill\u00e9n-Altamirano, M., Vill\u00e9n-Altamirano, J.: Restart: a straightforward method for fast simulation of rare events. In: WSC, pp. 282\u2013289. IEEE (1994)","DOI":"10.1109\/WSC.1994.717150"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-662-45231-8_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"ER Wognsen","year":"2014","unstructured":"Wognsen, E.R., Hansen, R.R., Larsen, K.G.: Battery-aware scheduling of mixed criticality systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part II. LNCS, vol. 8803, pp. 208\u2013222. Springer, Heidelberg (2014)"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-14295-6_21","volume-title":"Computer Aided Verification","author":"L Zhang","year":"2010","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 196\u2013211. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Cyber Physical Systems. Design, Modeling, and Evaluation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25141-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T07:45:53Z","timestamp":1748677553000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25141-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251400","9783319251417"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25141-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}