BRÁZDIL, Tomáš, David KLAŠKA, Antonín KUČERA and Petr NOVOTNÝ. Minimizing Running Costs in Consumption Systems. In Armin Biere, Roderick Bloem. Computer Aided Verification. Neuveden: Springer International Publishing, 2014. p. 457-472. ISBN 978-3-319-08866-2. doi:10.1007/978-3-319-08867-9_30.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Minimizing Running Costs in Consumption Systems
Authors BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), David KLAŠKA (203 Czech Republic, belonging to the institution), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution) and Petr NOVOTNÝ (203 Czech Republic, belonging to the institution).
Edition Neuveden, Computer Aided Verification, p. 457-472, 16 pp. 2014.
Publisher Springer International Publishing
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/14:00074098
Organization unit Faculty of Informatics
ISBN 978-3-319-08866-2
ISSN 0302-9743
Keywords in English controller synthesis; consumption systems; mean payoff
Tags core_A, firank_1, formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Petr Novotný, Ph.D., učo 172743. Changed: 16/11/2014 13:12.
A standard approach to optimizing long-run running costs of discrete systems is based on minimizing the mean-payoff, i.e., the long-run average amount of resources ("energy") consumed per transition. However, this approach inherently assumes that the energy source has an unbounded capacity, which is not always realistic. For example, an autonomous robotic device has a battery of finite capacity that has to be recharged periodically, and the total amount of energy consumed between two successive charging cycles is bounded by the capacity. Hence, a controller minimizing the mean-payoff must obey this restriction. In this paper we study the controller synthesis problem for consumption systems with a finite battery capacity, where the task of the controller is to minimize the mean-payoff while preserving the functionality of the system encoded by a given linear-time property. We show that an optimal controller always exists, and it may either need only finite memory or require infinite memory (it is decidable in polynomial time which of the two cases holds). Further, we show how to compute an effective description of an optimal controller in polynomial time. Finally, we consider the limit values achievable by larger and larger battery capacity, show that these values are computable in polynomial time, and we also analyze the corresponding rate of convergence. To the best of our knowledge, these are the first results about optimizing the long-run running costs in systems with bounded energy stores.
GAP202/10/1469, research and development projectName: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Czech Science Foundation, Standard Projects
MUNI/A/0765/2013, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/0855/2013, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 5/3/2021 02:39