2020/05/01 by Gal Amram, Shahar Maoz, Amram, Gal +5
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2005.00641
openalex publication_date 2020/05/01 · openalex created_date 2020/05/13 · openalex updated_date 2026/07/28
ω-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.