Battery transition systems

U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.

No fulltext has been uploaded. References only!

Conference Paper | Published | English

Scopus indexed
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.
Publishing Year
Date Published
595 - 606
POPL: Principles of Programming Languages
Conference Location
San Diego, USA
Conference Date
2014-01-22 – 2014-01-24

Cite this

Boker U, Henzinger TA, Radhakrishna A. Battery transition systems. In: Vol 49. ACM; 2014:595-606. doi:10.1145/2535838.2535875
Boker, U., Henzinger, T. A., & Radhakrishna, A. (2014). Battery transition systems (Vol. 49, pp. 595–606). Presented at the POPL: Principles of Programming Languages, San Diego, USA: ACM.
Boker, Udi, Thomas A Henzinger, and Arjun Radhakrishna. “Battery Transition Systems,” 49:595–606. ACM, 2014.
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 TA, Radhakrishna A. 2014. Battery transition systems. POPL: Principles of Programming Languages vol. 49, 595–606.
Boker, Udi, et al. Battery Transition Systems. Vol. 49, no. 1, ACM, 2014, pp. 595–606, doi:10.1145/2535838.2535875.


Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar
ISBN Search