conference paper published yes Udi Boker author 31E297B6-F248-11E8-B48F-1D18A9856A87 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Arjun Radhakrishna author 3B51CAC4-F248-11E8-B48F-1D18A9856A87 ToHe department POPL: Principles of Programming Languages Rigorous Systems Engineering project Quantitative Reactive Modeling project The analysis of the energy consumption of software is an important goal for quantitative formal methods. Current methods, using weighted transition systems or energy games, model the energy source as an ideal resource whose status is characterized by one number, namely the amount of remaining energy. Real batteries, however, exhibit behaviors that can deviate substantially from an ideal energy resource. Based on a discretization of a standard continuous battery model, we introduce battery transition systems. In this model, a battery is viewed as consisting of two parts-the available-charge tank and the bound-charge tank. Any charge or discharge is applied to the available-charge tank. Over time, the energy from each tank diffuses to the other tank. Battery transition systems are infinite state systems that, being not well-structured, fall into no decidable class that is known to us. Nonetheless, we are able to prove that the !-regular modelchecking problem is decidable for battery transition systems. We also present a case study on the verification of control programs for energy-constrained semi-autonomous robots. ACM2014San Diego, USA eng 978-145032544-810.1145/2535838.2535875 491595 - 606 Boker, Udi, et al. <i>Battery Transition Systems</i>. Vol. 49, no. 1, ACM, 2014, pp. 595–606, doi:<a href="https://doi.org/10.1145/2535838.2535875">10.1145/2535838.2535875</a>. U. Boker, T. A. Henzinger, and A. Radhakrishna, “Battery transition systems,” presented at the POPL: Principles of Programming Languages, San Diego, USA, 2014, vol. 49, no. 1, pp. 595–606. Boker, U., Henzinger, T. A., &#38; Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM. <a href="https://doi.org/10.1145/2535838.2535875">https://doi.org/10.1145/2535838.2535875</a> Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol 49. ACM; 2014:595-606. doi:<a href="https://doi.org/10.1145/2535838.2535875">10.1145/2535838.2535875</a> U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606. Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems. POPL: Principles of Programming Languages vol. 49, 595–606. Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition Systems,” 49:595–606. ACM, 2014. <a href="https://doi.org/10.1145/2535838.2535875">https://doi.org/10.1145/2535838.2535875</a>. 22392018-12-11T11:56:30Z2021-01-12T06:56:13Z