This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year’s edition of the competition. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Spring 2019.@en

For diffusions, a well-developed approach in rare event estimation is to introduce a suitable factorization of the reach probability and then to estimate these factors through simulation of an Interacting Particle System (IPS). This paper studies IPS based reach probability estimation for General Stochastic Hybrid Systems (GSHS). The continuous-time executions of a GSHS evolve in a hybrid state space under influence of combinations of diffusions, spontaneous jumps and forced jumps. In applying IPS to a GSHS, simulation of the GSHS execution plays a central role. From literature, two basic approaches in simulating GSHS execution are known. One approach is direct simulation of a GSHS execution. An alternative is to first transform the spontaneous jumps of a GSHS to forced transitions, and then to simulate executions of this transformed version. This paper will show that the latter transformation yields an extra Markov state component that should be treated as being unobservable for the IPS process. To formally make this state component unobservable for IPS, this paper also develops an enriched GSHS transformation prior to transforming spontaneous jumps to forced jumps. The expected improvements in IPS reach probability estimation are also illustrated through simulation results for a simple GSHS example.@en

This paper focuses on estimating reach probability of a closed unsafe set by a stochastic process. A well-developed approach is to make use of multi-level MC simulation, which consists of encapsulating the unsafe set by a sequence of increasing closed sets and conducting a sequence of MC simulations to estimate the reach probability of each inner set from the previous set. An essential step is to copy (split) particles that have reached the next level (inner set) prior to conducting a MC simulation to the next level. The aim of this paper is to prove that the variance of the multi-level MC estimated reach probability under fixed assignment splitting is smaller or equal than under random assignment splitting methods. The approaches are illustrated for a geometric Brownian motion example.@en

This paper studies estimation of reach probability for a generalized stochastic hybrid system (GSHS). For diffusion processes a well-developed approach in reach probability estimation is to introduce a suitable factorization of the reach probability and then to estimate these factors through simulation of an Interacting Particle System (IPS). The theory of this IPS approach has been extended to arbitrary strong Markov processes, which includes GSHS executions. Because Monte Carlo simulation of GSHS particles involves sampling of Brownian motion as well as sampling of random discontinuities, the practical elaboration of the IPS approach for GSHS is not straightforward. The aim of this paper is to elaborate the IPS approach for GSHS by using complementary Monte Carlo sampling techniques. For a simple GSHS example, it is shown that and why the specific technique selected for sampling discontinuities can have a major influence on the effectiveness of IPS in reach probability estimation.@en

This thesis conducts a series of interrelated research studies on reach probability estimation of rare events for stochastic hybrid systems. Chapter 1 explains that the motivation for these studies stems from the need to assess safety and capacity of a design for a future Air Traffic Management (ATM) concept of operations (ConOps). The safety/capacity of an ATM ConOps can be expressed in terms of the amount of traffic that can be handled in such a way that the probability of rare events remains sufficiently low. Chapter 1 also explains that the dynamic and stochastic behaviours in an ATM ConOps design can be captured by a General Stochastic Hybrid System (GSHS) model, and that the rare events to be studied can be defined as events that the state of a GSHS model reaches an unsafe set. In ATM safety studies, an unsafe set often considered is the closed subset in the GSHS state space where the physical shapes of two aircraft overlap. The state of a GSHS model consists of two components: i) a Euclidean valued component, and ii) a discrete valued component. The evolution of these two components influence each other; therefore a GSHS model can capture various types of dynamic and stochastic behaviours, including Brownian motion and spontaneous jumps. In contrast to forced jumps, that happen when the GSHS state reaches a boundary in the hybrid state space, spontaneous jumps occur according to a Poisson point process. A mathematically important property of GSHS, is that a GSHS execution satisfies the strong Markov property...@en

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks within this category, and recommends next steps for this category towards next year's edition of the competition. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Spring/Summer 2021.@en

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.@en