Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in \(\mathsf{NP}\cap \mathsf{coNP}\) and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.

The dynamic gas flow model with static electric-driven compressor (EDC) model has been widely studied in coordinated analysis of integrated electricity-gas system (IEGS). However, as a crucial coupling unit, the boost characteristics of the EDC change dynamically with gas state, which may lead to unstable operation mode and then affect safe operating of IEGS. Meanwhile, its nonlinear model greatly increases the difficulty of analysis. This paper proposes a reduced-order transfer function model that considers EDCs for an accurate and efficient dynamic analysis of the IEGS. Firstly, a general two-port model in the Laplace-domain is derived to jointly analyze the pipeline and EDCs dynamic characteristics. The model based on transfer function, explicitly gives the relation between the pressures and flows state at ports. On this basis, to concisely analyze state variations of crucial nodes, the multiple cascaded pipelines and compressors are aggregated and to form an equivalent model. Meanwhile, to reduce the computational burden of the high-order Laplacian “s” in the aggregated process, a reduced-order method is developed based on Jordan continued-fraction expansion by preserving the main gas dynamic feature. Then the analytical expression of state fluctuation can be conveniently derived to analyze the underlying impact and interaction between power system and gas system. Finally, case studies are conducted to prove the effectiveness of proposed model and reduction method.

Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.