Verification of probabilistic bounded δ-reachability for cyber-physical systems

Abstract—Verification of cyber-physical systems is a difficult, yet extremely important, problem. Hybrid systems offer a theoret-ical framework in which to perform formal verification of cyber-physical systems. In this paper we study the problem of bounded δ-reachability in hybrid systems with random initial parameters. We devise a technique for computing reachability probabilities over a finite number of discrete steps for nonlinear hybrid systems featuring a bounded random initial parameter. Our approach is to define an appropriate δ-relaxation of the (undecidable) reachability problem, so that it can be solved by a δ-complete decision procedure. Specifically, we can compute an interval that is guaranteed to contain the probability of, say, a hybrid system behaving in a faulty way. Moreover, we discuss certain types of random variables with unbounded support and show that the bounded δ-reachability problem can still be solved by using an appropriate δ-complete decision procedure. Finally, we propose the development of a validated integration procedure over an arbitrary Borel set in order to cope with hybrid systems with dynamics given by solutions of ordinary differential equations. I