TY - CHAP
T1 - Efficient Algorithms for Omega-Regular Energy Games
AU - Amram, Gal
AU - Maoz, Shahar
AU - Pistiner, Or
AU - Ringert, Jan Oliver
N1 - Funding Information:
Acknowledgments. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - ω -regular energy games are two-player ω -regular games augmented with a requirement to avoid the exhaustion of a finite resource, e.g., battery or disk space. ω -regular energy games can be reduced to ω -regular games by encoding the energy level into the state space. As this approach blows up the state space, it performs poorly. Moreover, it is highly affected by the chosen energy bound denoting the resource’s capacity. In this work, we present an alternative approach for solving ω -regular energy games, with two main advantages. First, our approach is efficient: it avoids the encoding of the energy level within the state space, and its performance is independent of the engineer’s choice of the energy bound. Second, our approach is defined at the logic level, not at the algorithmic level, and thus allows solving ω -regular energy games by seamless reuse of existing symbolic fixed-point algorithms for ordinary ω -regular games. We base our work on the introduction of energy μ -calculus, a multi-valued extension of game μ -calculus. We have implemented our ideas and evaluated them. The empirical evaluation provides evidence for the efficiency of our work.
AB - ω -regular energy games are two-player ω -regular games augmented with a requirement to avoid the exhaustion of a finite resource, e.g., battery or disk space. ω -regular energy games can be reduced to ω -regular games by encoding the energy level into the state space. As this approach blows up the state space, it performs poorly. Moreover, it is highly affected by the chosen energy bound denoting the resource’s capacity. In this work, we present an alternative approach for solving ω -regular energy games, with two main advantages. First, our approach is efficient: it avoids the encoding of the energy level within the state space, and its performance is independent of the engineer’s choice of the energy bound. Second, our approach is defined at the logic level, not at the algorithmic level, and thus allows solving ω -regular energy games by seamless reuse of existing symbolic fixed-point algorithms for ordinary ω -regular games. We base our work on the introduction of energy μ -calculus, a multi-valued extension of game μ -calculus. We have implemented our ideas and evaluated them. The empirical evaluation provides evidence for the efficiency of our work.
UR - http://www.scopus.com/inward/record.url?scp=85119831100&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-90870-6_9
DO - 10.1007/978-3-030-90870-6_9
M3 - Conference paper
AN - SCOPUS:85119831100
SN - 9783030908690
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 163
EP - 181
BT - Formal Methods - 24th International Symposium, FM 2021, Proceedings
A2 - Huisman, Marieke
A2 - Păsăreanu, Corina
A2 - Zhan, Naijun
PB - Springer Science and Business Media Deutschland GmbH
T2 - 24th International Symposium on Formal Methods, FM 2021
Y2 - 20 November 2021 through 26 November 2021
ER -