发表机构
University of Twente; University of Münster（特文特大学; 明斯特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出用随机混合自动机对能源系统功率曲线建模，形式化两种方法并给出构造规则，分析设计选择对复杂度的影响，并用工具验证可行性。
AI 中文摘要
功率曲线被广泛用于描述能源系统中的电力需求和发电。然而，实际使用中往往涉及不确定性，这使得确定例如电池能否可靠地满足给定曲线变得具有挑战性。形式化建模能够计算电池满足此类需求的概率。鉴于离散和连续动态的结合，以及不确定的使用模式，随机混合自动机（SHA）为这种建模和分析提供了合适的框架。在本文中，我们形式化了两种正交的方法来指定特定电池能够服务的（不确定的）功率曲线以及存储模型。对于两种类型的功率曲线，我们提供了反映存储模型在给定特定功率曲线下行为的SHA的正式构造规则。我们分析了设计选择（如功率曲线、存储模型和不确定性表示）如何影响所得SHA的复杂性。最后，我们演示了这些模型如何使用工具Modest和realyst量化可行性，并评估分析如何随曲线大小和随机组件数量扩展。
英文摘要
Power profiles are widely used to describe power demand and production in energy systems. Yet, real-world usage often involves uncertainty, making it challenging to determine, e.g., whether a battery can reliably meet a given profile. Formal modeling enables the computation of probabilities that a battery will satisfy such demands. Given the combination of discrete and continuous dynamics, along with uncertain usage patterns, stochastic hybrid automata (SHA) offer a suitable framework for such modeling and analysis. In this paper, we formalize two orthogonal approaches to specify the (uncertain) power profiles that a specific battery can serve as well as a storage model. For both types of power profiles, we provide formal construction rules for SHA reflecting the behavior of the storage model given a specific power profile. We analyze how design choices, such as the power profile, storage model, and representation of uncertainty, affect the complexity of the resulting SHA. Finally, we demonstrate how these models quantify feasibility using the tools Modest and realyst, and assess how the analysis scales with profile size and the number of stochastic components.
CommentsThis paper is accepted for publication (without appendix) in the Proceedings of the 2026 International Colloquium on Theoretical Aspects of Computing (ICTAC). The appendix was part of the submission and provides additional material which is not included in the ICTAC publication
