arXiv subjects

Lisa Willemsen

Publications and source records attributed to Lisa Willemsen.

3 recordsLinked to original sources

arXiv2026

Stochastic Hybrid Automata for Power Profile Modeling in Energy Systems

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.

cs.FL↗

arXiv2025

Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata

Simulink is widely used in industrial design processes to model increasingly complex embedded control systems. Thus, their formal analysis is highly desirable. However, this comes with two major challenges: First, Simulink models often provide an idealized view of real-life systems and omit uncertainties such as, aging, sensor noise or failures. Second, the semantics of Simulink is only informally defined. In this paper, we present an approach to formally analyze safety and performance of embedded control systems modeled in Simulink in the presence of uncertainty. To achieve this, we 1) model different types of uncertainties as stochastic Simulink subsystems and 2) extend an existing formalization of the Simulink semantics based on stochastic hybrid automata (SHA) by providing transformation rules for the stochastic subsystems. Our approach gives us access to established quantitative analysis techniques, like statistical model checking and reachability analysis. We demonstrate the applicability of our approach by analyzing safety and performance in the presence of uncertainty for two smaller case studies.

eess.SY↗

arXiv2023

Comparing Two Approaches to Include Stochasticity in Hybrid Automata

Different stochastic extensions of hybrid automata have been proposed in the past, with unclear expressivity relations between them. To structure and relate these modeling languages, in this paper we formalize two alternative approaches to extend hybrid automata with stochastic choices of discrete events and their time points. The first approach, which we call decomposed scheduling, adds stochasticity via stochastic races, choosing random time points for the possible discrete events and executing a winner with an earliest time. In contrast, composed scheduling first samples the time point of the next event and then the event to be executed at the sampled time point. We relate the two approaches regarding their expressivity and categorize available stochastic extensions of hybrid automata from the literature.

cs.FL↗