Efficient Algorithms for Omega-Regular Energy Games

Gal Amram, Shahar Maoz*, Or Pistiner, Jan Oliver Ringert

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

3 Citations (Scopus)

Abstract

ω -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.

Original languageEnglish
Title of host publicationFormal Methods - 24th International Symposium, FM 2021, Proceedings
EditorsMarieke Huisman, Corina Păsăreanu, Naijun Zhan
PublisherSpringer Science and Business Media Deutschland GmbH
Pages163-181
Number of pages19
ISBN (Print)9783030908690
DOIs
Publication statusPublished - 2021
Event24th International Symposium on Formal Methods, FM 2021 - Virtual, Online
Duration: 20 Nov 202126 Nov 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13047 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Symposium on Formal Methods, FM 2021
CityVirtual, Online
Period20/11/202126/11/2021

Fingerprint

Dive into the research topics of 'Efficient Algorithms for Omega-Regular Energy Games'. Together they form a unique fingerprint.

Cite this