Verification and Control of Probabilistic Rectangular Hybrid Automata

Hybrid systems are characterised by a combination of discrete and continuous components. In many application areas for hybrid systems, such as vehicular control and systems biology, stochastic behaviour is exhibited. This has led to the development of stochastic extensions of formalisms, such as hybrid automata, for the modelling of hybrid systems, together with their associated verification and controller synthesis algorithms, in order to allow reasoning about quantitative properties such as “the vehicle’s speed will reach 50kph within 10 seconds with probability at least 0.99”. We consider verification and control of probabilistic rectangular hybrid automata, which generalise the well-known class of rectangular hybrid automata with the possibility of representing random behaviour of the discrete components of the system, permitting the modelling of the likelihood of faults, choices in randomised algorithms and message losses. Furthermore, we will also consider how probabilistic rectangular hybrid automata can be used as abstract models for more general classes of stochastic hybrid systems.