---
_id: '2239'
abstract:
- lang: eng
  text: 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.
author:
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Arjun
  full_name: Radhakrishna, Arjun
  id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
  last_name: Radhakrishna
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: '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.'
  ista: 'Boker U, Henzinger TA, Radhakrishna A. 2014. Battery transition systems.
    POPL: Principles of Programming Languages vol. 49, 595–606.'
  mla: 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>.
  short: U. Boker, T.A. Henzinger, A. Radhakrishna, in:, ACM, 2014, pp. 595–606.
conference:
  end_date: 2014-01-24
  location: San Diego, USA
  name: 'POPL: Principles of Programming Languages'
  start_date: 2014-01-22
date_created: 2018-12-11T11:56:30Z
date_published: 2014-01-13T00:00:00Z
date_updated: 2021-01-12T06:56:13Z
day: '13'
department:
- _id: ToHe
doi: 10.1145/2535838.2535875
ec_funded: 1
intvolume: '        49'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 595 - 606
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_identifier:
  isbn:
  - 978-145032544-8
publication_status: published
publisher: ACM
publist_id: '4722'
quality_controlled: '1'
scopus_import: 1
status: public
title: Battery transition systems
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 49
year: '2014'
...