Battery transition systems Conference Paper


Author(s): Boker, Udi; Henzinger, Thomas A; Radhakrishna, Arjun
Title: Battery transition systems
Affiliation IST Austria
Abstract: 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.
Keywords: model checking; transition systems; Battery; Energy
Conference Title: POPL: Principles of Programming Languages
Volume: 49
Issue 1
Conference Dates: January 22-24, 2014
Conference Location: San Diego, CA, USA
Publisher: ACM  
Location: New York, NY, USA
Date Published: 2014-01-13
Start Page: 595
End Page: 606
Sponsor: This work was supported in part by the Austrian Science Fund NFN RiSE (Rigorous Systems Engineering), and by the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).
DOI: 10.1145/2578855.2535875
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Udi Boker
    12 Boker
Related IST Austria Work