Convergence proofs for Simulated Annealing falsification of safety properties
作者： Houssam Abbas , Georgios Fainekos
DOI: 10.1109/ALLERTON.2012.6483411
关键词:
摘要: The problem of falsifying temporal logic properties hybrid automata can be posed as a minimization by utilizing quantitative semantics for logics. Previous work has used variation Simulated Annealing (SA) to solve the problem. While SA is known converge global minimum continuous objective function over closed and bounded search space, or when space discrete, there do not exist convergence proofs cases addressed in that previous work. Namely, discontinuous, vector-valued function. In this paper, we derive conditions prove both scenarios. We also consider matters affecting practical performance SA.
elsevier.com
sci-hub.se 参考文章(29)
Stefan Ratschan, Jan-Georg Smaus, Finding Errors of Hybrid Systems by Optimising an Abstraction-Based Quality Estimate tests and proofs. pp. 153- 168 ,(2009) , 10.1007/978-3-642-02949-3_12
Houssam Abbas, Georgios Fainekos, Linear hybrid system falsification through local search automated technology for verification and analysis. pp. 503- 510 ,(2011) , 10.1007/978-3-642-24372-1_39
Paulo Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach ,(2009)
Alexandre Donzé, Oded Maler, Systematic simulation using sensitivity analysis international conference on hybrid systems computation and control. pp. 174- 189 ,(2007) , 10.1007/978-3-540-71493-4_16
Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi, Falsification of LTL Safety Properties in Hybrid Systems tools and algorithms for construction and analysis of systems. pp. 368- 382 ,(2009) , 10.1007/978-3-642-00768-2_31
Tarik Nahhal, Thao Dang, Test Coverage for Continuous and Hybrid Systems Computer Aided Verification. pp. 449- 462 ,(2007) , 10.1007/978-3-540-73368-3_47
Aurélien Rizk, Grégory Batt, François Fages, Sylvain Soliman, On a Continuous Degree of Satisfaction of Temporal Logic Formulae with Applications to Systems Biology computational methods in systems biology. ,vol. 5307, pp. 251- 268 ,(2008) , 10.1007/978-3-540-88562-7_19
Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi, Hybrid Systems: From Verification to Falsification Computer Aided Verification. pp. 463- 476 ,(2007) , 10.1007/978-3-540-73368-3_48
M.S. Branicky, S. Morgan, J. Levine, M.M. Curtiss, Sampling-based planning, control and verification of hybrid systems IEE Proceedings - Control Theory and Applications. ,vol. 153, pp. 575- 590 ,(2006) , 10.1049/IP-CTA:20050152
K.I. Smith, R.M. Everson, J.E. Fieldsend, C. Murphy, R. Misra, Dominance-Based Multiobjective Simulated Annealing IEEE Transactions on Evolutionary Computation. ,vol. 12, pp. 323- 342 ,(2008) , 10.1109/TEVC.2007.904345