9 papers
Stochastic Hybrid Automata for Power Profile Modeling in Energy Systems
Lisa Willemsen, Anne Remke, Johann L. Hurink
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.…
Minimum Reachability Probabilities in Rectangular Automata with Random Clocks
Joanna Delicaris, Erika Ábrahám, Anne Remke
Control applications for cyber-physical systems must make reliably safe control decisions in the presence of continuous dynamics as well as stochastic uncertainty. Providing safety…
Scaling Up Reachability Analysis for Rectangular Automata with Random Clocks
Jonas Stübbe, Anne Remke, Erika Ábrahám
This paper presents optimizations to improve the scalability of reachability analysis on a subclass of hybrid automata extended with stochasticity. The optimizations target differe…
ARCH-COMP25 Category Report: Stochastic Models
Alessandro Abate, Omid Akbarzadeh, Henk A. P. Blom +14
This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks a…
Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata
Pauline Blohm, Felix Schulz, Lisa Willemsen +2
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…
Comparing Two Approaches to Include Stochasticity in Hybrid Automata
Lisa Willemsen, Anne Remke, Erika Ábrahám
Different stochastic extensions of hybrid automata have been proposed in the past, with unclear expressivity relations between them. To structure and relate these modeling language…
Maximizing Reachability Probabilities in Rectangular Automata with Random Clocks
Joanna Delicaris, Stefan Schupp, Erika Ábrahám +1
This paper proposes an algorithm to maximize reachability probabilities for rectangular automata with random clocks via a history-dependent prophetic scheduler. This model class in…
Proceedings The 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT
Anne Remke, Dung Hoang Tran
The proceedings of the 7th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2021) feature five peer-reviewed contributions and three invited…
State-space construction of Hybrid Petri nets with multiple stochastic firings
Jannik Hüls, Carina Pilch, Patricia Schinke +3
Hybrid Petri nets have been extended to include general transitions that fire after a randomly distributed amount of time. With a single general one-shot transition the state space…