Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
Authors:
Gal Amram,
Shahar Maoz,
Or Pistiner,
Jan Oliver Ringert
Abstract:
$ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω…
▽ More
$ω$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $μ$-calculus, when applied over game graphs with $ω$-regular winning conditions, allows defining symbolic algorithms in the form of fixed-point formulas for computing the sets of winning states.
In this paper, we introduce energy $μ$-calculus, a multi-valued extension of the $μ$-calculus that serves as a symbolic framework for solving $ω$-regular energy games. Energy $μ$-calculus enables the seamless reuse of existing, well-known symbolic $μ$-calculus algorithms for $ω$-regular games, to solve their corresponding energy augmented variants. We define the syntax and semantics of energy $μ$-calculus over symbolic representations of the game graphs, and show how to use it to solve the decision and the minimum credit problems for $ω$-regular energy games, for both bounded and unbounded energy level accumulations.
△ Less
Submitted 18 October, 2020; v1 submitted 1 May, 2020;
originally announced May 2020.
Symbolic BDD and ADD Algorithms for Energy Games
Authors:
Shahar Maoz,
Or Pistiner,
Jan Oliver Ringert
Abstract:
Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative co…
▽ More
Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative constraints expressed in the energy game. A symbolic algorithm for energy games, recently presented by Chatterjee et al., is symbolic in its representation of quantitative values but concrete in the representation of game states and transitions. In this paper we present an algorithm that is symbolic both in the quantitative values and in the underlying game representation. We have implemented our algorithm using two different symbolic representations for reactive games, Binary Decision Diagrams (BDD) and Algebraic Decision Diagrams (ADD). We investigate the commonalities and differences of the two implementations and compare their running times on specifications of energy games.
△ Less
Submitted 22 November, 2016;
originally announced November 2016.
