Temporal Logic Inference for Hybrid System Observation with Spatial and Temporal Uncertainties.
作者： Agung Julius , Yi Deng , Zhe Xu
DOI:
关键词:
摘要: In this paper, we present a mechanism for building hybrid system observers to differentiate between specific positions of the system. The is designed through inferring metric temporal logic (MTL) formulae from simulated trajectories We first approximate behavior by simulating finitely many with timerobust tube segments around them. These time-robust account both spatial and uncertainties that exist in initial state variations. inferred MTL classify different thus can be used classifying behaviors provably correct fashion. implement our approach on model smart testbed distinguish two cases room occupancy.
arxiv.org
harvard.edu参考文章(45)
Ebenezer Hailemariam, Azam Khan, Rhys Goldstein, Ramtin Attar, Real-time occupancy detection using decision trees with multiple sensor types annual simulation symposium. pp. 141- 148 ,(2011) , 10.5555/2048536.2048555
Antoine Girard, Approximately bisimilar finite abstractions of stable linear systems international conference on hybrid systems computation and control. ,vol. 4416, pp. 231- 244 ,(2007) , 10.1007/978-3-540-71493-4_20
Yi Deng, Akshay Rajhans, A. Agung Julius, STRONG: A Trajectory-Based Verification Toolbox for Hybrid Systems Quantitative Evaluation of Systems. pp. 165- 168 ,(2013) , 10.1007/978-3-642-40196-1_13
Andrea Balluchi, Luca Benvenuti, Maria D. Di Benedetto, Alberto L. Sangiovanni-Vincentelli, Design of Observers for Hybrid Systems acm international conference hybrid systems computation and control. pp. 76- 89 ,(2002) , 10.1007/3-540-45873-5_9
A. Agung Julius, Georgios E. Fainekos, Madhukar Anand, Insup Lee, George J. Pappas, Robust test generation and coverage for hybrid systems international conference on hybrid systems computation and control. pp. 329- 342 ,(2007) , 10.1007/978-3-540-71493-4_27
A. Alessandri, P. Coletta, Design of Luenberger Observers for a Class of Hybrid Linear Systems acm international conference hybrid systems computation and control. pp. 7- 18 ,(2001) , 10.1007/3-540-45351-2_5
Alexandre Donzé, Oded Maler, Robust satisfaction of temporal logic over real-valued signals formal modeling and analysis of timed systems. ,vol. 6246, pp. 92- 106 ,(2010) , 10.1007/978-3-642-15297-9_9
Orna Kupferman, Moshe Y. Vardi, Model Checking of Safety Properties formal methods. ,vol. 19, pp. 291- 314 ,(2001) , 10.1023/A:1011254632723
Eugene Asarin, Alexandre Donzé, Oded Maler, Dejan Nickovic, Parametric identification of temporal properties runtime verification. pp. 147- 160 ,(2011) , 10.1007/978-3-642-29860-8_12
R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, The algorithmic analysis of hybrid systems Theoretical Computer Science. ,vol. 138, pp. 3- 34 ,(1995) , 10.1016/0304-3975(94)00202-T