TY - GEN
T1 - Neural State Classification for Hybrid Systems
AU - Phan, Dung
AU - Paoletti, Nicola
AU - Zhang, Timothy
AU - Grosu, Radu
AU - Smolka, Scott A.
AU - Stoller, Scott D.
N1 - Publisher Copyright:
© 2019 Association for Computing Machinery.
PY - 2019/4/15
Y1 - 2019/4/15
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/85066150584
U2 - 10.1145/3313149.3313372
DO - 10.1145/3313149.3313372
M3 - Conference contribution
AN - SCOPUS:85066150584
T3 - SNR 2019 - Proceedings of the 5th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT
BT - SNR 2019 - Proceedings of the 5th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT
A2 - Ramachandran, Gowri Sankar
A2 - Ortiz, Jorge
PB - Association for Computing Machinery, Inc
T2 - 5th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT, SNR 2019, held as part of the 12th Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2019
Y2 - 15 April 2019
ER -