BRÁZDIL, Tomáš, David KLAŠKA, Antonín KUČERA a Petr NOVOTNÝ. Minimizing Running Costs in Consumption Systems. In Armin Biere, Roderick Bloem. Computer Aided Verification. Neuveden: Springer International Publishing, 2014. s. 457-472. ISBN 978-3-319-08866-2. doi:10.1007/978-3-319-08867-9_30.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Minimizing Running Costs in Consumption Systems
Autoři BRÁZDIL, Tomáš (203 Česká republika, domácí), David KLAŠKA (203 Česká republika, domácí), Antonín KUČERA (203 Česká republika, garant, domácí) a Petr NOVOTNÝ (203 Česká republika, domácí).
Vydání Neuveden, Computer Aided Verification, od s. 457-472, 16 s. 2014.
Nakladatel Springer International Publishing
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/14:00074098
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-08866-2
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-08867-9_30
Klíčová slova anglicky controller synthesis; consumption systems; mean payoff
Štítky core_A, firank_1, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Petr Novotný, Ph.D., učo 172743. Změněno: 16. 11. 2014 13:12.
Anotace
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.
Návaznosti
GAP202/10/1469, projekt VaVNázev: Formální metody pro analýzu a verifikaci komplexních systémů
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/0765/2013, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0855/2013, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)
Investor: Masarykova univerzita, Grantová agentura MU, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 17. 1. 2021 10:51