Characterization and Analysis of Flexible Energy Prosumers using Resource Timed Automata
Translated title
Karakterisering og Analyse af Fleksible Energi Prosumers ved brug af Resurse Automater
Author
Hansen, Jonas
Term
4. term
Education
Publication year
2022
Submitted on
2022-08-10
Pages
21
Abstract
Modern energy systems must match supply and demand. We study how to model and analyze the flexible behavior of prosumer systems—participants who both consume and produce energy—to help balance an energy grid. We introduce Resource Timed Automata (RTA), a formal model of states and timed transitions that also tracks resources such as energy, and show how individual prosumers can be represented within this framework. We then show that aggregating many prosumers in a smart grid can be captured as a special kind of parallel composition, where multiple RTAs evolve side by side. The balancing task is formalized as a reachability question on an observer automaton that monitors the combined system: are the desired balanced states reachable? Finally, we illustrate how to solve these reachability problems using established model checking methods, and discuss why we expect these techniques to scale well in practice for this class of problems.
Moderne energisystemer skal matche udbud og efterspørgsel. Vi undersøger, hvordan man kan modellere og analysere den fleksible adfærd i systemer med prosumenter—aktører, der både forbruger og producerer energi—for at balancere et elnet. Vi introducerer Resource Timed Automata (RTA), en formel model af tilstande og tidsbestemte overgange, som også holder styr på ressourcer som energi, og viser, hvordan individuelle prosumenter kan beskrives i denne ramme. Dernæst viser vi, at aggregering af mange prosumenter i et smart elnet kan modelleres som en særlig form for parallel komposition, hvor flere RTA'er udvikler sig side om side. Balanceringsopgaven formaliseres som et nåbarhedsspørgsmål på en observer-automat, der overvåger det samlede system: kan de ønskede, balancerede tilstande nås? Endelig illustrerer vi, hvordan disse nåbarhedsproblemer kan løses med etablerede metoder fra model checking, og diskuterer, hvorfor vi forventer, at metoderne vil skalere godt i praksis for denne type problem.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords