This paper offers a formal framework for the rare collision risk estimation of autonomous vehicles (AVs) with multi-agent situation awareness, affected by different sources of noise in a complex dynamic environment. The estimation framework consists of two complementary parts: modeling formalism and a rare event estimation method using sequential Monte Carlo (MC) simulation instead of importance sampling. By defining incremental levels of severity that must be passed before a collision, a sequence of MC simulations can be applied from one level to the next. This particular sequential MC method consists of the simulation of an Interacting Particle System (IPS) in combination with Fixed Assignment Splitting (FAS) of particles that reach the next level. We model AVs equipped with the situation awareness as general stochastic hybrid systems (GSHS), including the IPS-FAS relevant severity levels, and assess the probability of collision in a lane-change scenario where two self-driving vehicles simultaneously intend to switch lanes into a shared one while utilizing the time-tocollision measure for decision-making as required. The IPS-FAS method is subsequently used to estimate collision risk for this GSHS model of the lane-changing scenario. The results show that in contrast to straightforward MC simulation, IPS-FAS is able to quantify the very low collision risk for the scenario of interest. @en

We present shrinking horizon model predictive control for discrete-time linear systems under stochastic disturbances with constraints encoded as signal temporal logic (STL) specification. The control objective is to satisfy a given STL specification with high probability against stochastic uncertainties while maximizing the robust satisfaction of an STL specification with minimum control effort. We formulate a general solution, which does not require precise knowledge of probability distributions of (possibly dependent) stochastic disturbances; only the bounded support of the density functions and moment intervals are used. For the specific case of disturbances that are normally distributed, we optimize the controllers by utilizing knowledge of the probability distribution of the disturbance. We show that in both cases, the control law can be obtained by solving optimization problems with linear constraints at each step. We experimentally demonstrate effectiveness of this approach by synthesizing a controller for a heating, ventilation, and air conditioning system.

@en

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this first edition, we present five benchmarks with different levels of complexities and stochastic favours. We make use of six different tools and frameworks (in alphabetical order): Barrier Certificates, FAUST2, FIRM-GDTL, Modest, SDCPN modelling & MC simulation and SReachTools; and attempt to solve instances of the five different benchmark problems. Through these benchmarks, we capture a snapshot on the current state-of the art tools and frameworks within the stochastic modelling domain. We also present the challenges encountered within this domain and highlight future plans which will push forward the development of more tools and methodologies for performing formal verification and optimal policy synthesis of stochastic processes. @en