Neural State Classification for Hybrid Systems

Abstract

Model checking of hybrid systems is usually expressed in terms of the following reachability problem for hybrid automata (HA) [6]: Given an HAM, a set of initial states I , and a set of unsafe statesU , determine whether there exists a trajectory ofMstarting in an initial state and ending in an unsafe state. The time-bounded version of this problem considers trajectories that are within a given time boundT . We introduce the State Classification Problem (SCP), a generalization of the model checking problem for hybrid systems. Let B={0,1} be the set of Boolean values. Given an HAMwith state space S(M), time boundT , and set of unsafe states U s(M), the SCP problem is to find a function F →:S(M).iæBsuch that for all s s(M), F .(s)=1 if M|=Reach(U,s,T ), i.e., if it is possible forM, starting in s, to reach a state inU within time T ; F .(s)=0 otherwise. A state s iô S(M) is called positive if F .(s) = 1. Otherwise, s is negative.We call such a function a state classifier.