Temporal Logics for Learning and Detection of Anomalous Behavior

被引:88
作者
Kong, Zhaodan [1 ]
Jones, Austin [2 ]
Belta, Calin [3 ,4 ]
机构
[1] Univ Calif Davis, Dept Mech & Aerosp Engn, Davis, CA 95616 USA
[2] Georgia Inst Technol, Mech Engn & Elect & Comp Engn, Atlanta, GA 30332 USA
[3] Boston Univ, Dept Mech Engn, Boston, MA 02215 USA
[4] Boston Univ, Div Syst Engn, Boston, MA 02215 USA
关键词
Anomaly detection; formal methods; learning; networked systems; signal temporal logic (STL); FALSIFICATION; ROBUSTNESS;
D O I
10.1109/TAC.2016.2585083
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
The increased complexity of modern systems necessitates automated anomaly detection methods to detect possible anomalous behavior determined by malfunctions or external attacks. We present formal methods for inferring (via supervised learning) and detecting (via unsupervised learning) anomalous behavior. Our procedures use data to construct a signal temporal logic (STL) formula that describes normal system behavior. This logic can be used to formulate properties such as "If the train brakes within 500 m of the platform at a speed of 50 km/hr, then it will stop in at least 30 s and at most 50 s."Our procedure infers not only the physical parameters involved in the formula (e.g., 500 m in the example above) but also its logical structure. STL gives a more human-readable representation of behavior than classifiers represented as surfaces in high-dimensional feature spaces. The learned formula enables us to perform early detection by using monitoring techniques and anomaly mitigation by using formal synthesis techniques. We demonstrate the power of ourmethodswith examples of naval surveillance and a train braking system.
引用
收藏
页码:1210 / 1222
页数:13
相关论文
共 33 条
[1]  
Abbas H, 2012, ANN ALLERTON CONF, P1594, DOI 10.1109/Allerton.2012.6483411
[2]  
[Anonymous], 2015, P 18 INT C HYBRID SY, DOI DOI 10.1145/2728606.2728628
[3]  
Asarin E., 2012, Lecture Notes in Computer Science, P147, DOI [DOI 10.1007/978-3-642, 10.1007/978-3-642-29860-812, 10.1007/978-3-642-29860-8_12, DOI 10.1007/978-3-642-29860-8_12]
[4]   On the Robustness of Temporal Properties for Stochastic Models [J].
Bartocci, Ezio ;
Bortolussi, Luca ;
Nenzi, Laura ;
Sanguinetti, Guido .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (125) :3-19
[5]  
Bishop C., 2006, Pattern recognition and machine learning, P423
[6]  
Davey B. A., 2002, INTRO LATTICES ORDER, DOI DOI 10.1017/CBO9780511809088
[7]   Stochastic Local Search for Falsification of Hybrid Systems [J].
Deshmukh, Jyotirmoy ;
Jin, Xiaoqing ;
Kapinski, James ;
Maler, Oded .
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 :500-517
[8]   On-line monitoring for temporal logic robustness [J].
Dokhanchi, Adel ;
Hoxha, Bardh ;
Fainekos, Georgios .
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8734 :231-246
[9]  
Donzé A, 2010, LECT NOTES COMPUT SC, V6246, P92, DOI 10.1007/978-3-642-15297-9_9
[10]  
Fainekos Georgios E., 2011, IEEE International Conference on Robotics and Automation, P40