Details
Title
Efficient choice of parameters on delta-reachability bounded hybrid systemsJournal title
Archives of Control SciencesYearbook
2021Volume
vol. 31Issue
No 4Authors
Affiliation
Rocha, Eugénio Miguel Alexandre : Center for Research and Development in Mathematics and Applications, and Department of Mathematics, University of Aveiro, 3810-193 Aveiro, Portugal ; Murillo, Kelly Patricia : Center for Research and Development in Mathematics and Applications, and Department of Mathematics, University of Aveiro, 3810-193 Aveiro, PortugalKeywords
bounded hybrid system ; safety property ; delta-reachability ; multidirectional efficiency analysisDivisions of PAS
Nauki TechniczneCoverage
781-794Publisher
Committee of Automatic Control and Robotics PASBibliography
[1] M. Althoff and J.M. Dolan: Online verification of automated road vehicles using reachability analysis. IEEE Trans. on Robotics, 30(4), (2014), 903– 918, DOI: 10.1109/TRO.2014.2312453.[2] P. Bogetoft and J.L. Hougaard: Efficiency evaluations based on potential (non-proportional) improvements. Journal of Productivity Analysis, 12(3), (1999), 233–247, DOI: 10.1023/A:1007848222681.
[3] X. Chen, E. Abraham and S. Sankaranarayanan: Flow*: An analyzer for non-linear hybrid systems. In: Proc. of CAV’13. LNCS, 8044, 258–263, Springer, 2013.
[4] E.M. Clarke and S. Gao: Model checking hybrid systems. In: Margaria T., Steffen B. (eds): Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014. Lecture Notes in Computer Science, 8803, 385–386, Springer, Berlin, Heidelberg, 2014.
[5] M. Franzle, C. Herde, S. Ratschan, T. Schubert and T. Teige: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation, 1 (2007), 209–236, DOI: 10.3233/SAT190012.
[6] G. Frehse, C.L. Guernic, A. Donze, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang and O. Maler: SpaceEx: Scalable verification of hybrid systems. In: Proc. of CAV’11. LNCS, 6806, 379–395, Springer, 2011.
[7] S. Gao: Computable analysis, decision procedures, and hybrid automata: A new framework for the formal verification of cyber-physical systems. Ph.D. thesis, Carnegie Mellon University, 2012.
[8] S. Gao, S. Kong and E.M. Clarke: dReal: An SMT solver for nonlinear theories over the reals. In: M.P. Bonacina (ed.) CADE 2013. LNCS (LNAI), 7898, 208–214, Springer, Heidelberg (2013). DOI: 10.1007/978-3-642-38574-2.
[9] HyCreate: A tool for overapproximating reachability of hybrid automata, http://stanleybak.com/projects/hycreate/hycreate.html.
[10] S. Kong, S. Gao, W. Chen and E. Clarke: dReach: δ-reachability analysis for hybrid systems. In Proc. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2015. Available: http://link.springer.com/10.1007/978-3-662-46681-0.
[11] J. Lygeros, C. Tomlin and S. Sastry: Hybrid systems: modeling analysis and control. Electronic Research Laboratory, University of California, Berkeley, CA, Tech. Rep. UCB/ERL M, 2008.
[12] A. Platzer and J. Quesel: Keymaera: A hybrid theorem prover for hybrid systems (system description). In: Proc. of IJCAR’08.LNCS, 5195, 171–178, Springer, 2008.
[13] S. Ratschan and Z. She: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Proc. of HSCC’05. LNCS, 3414, 573–589, Springer, 2005.
[14] E.M. Rocha: Oscillatory behaviour on a non-autonomous hybrid SIRmodel. In: M. Chaves and M. Martins (eds.), Molecular Logic and Computational Synthetic Biology. MLCSB 2018. Lecture Notes in Computer Science, 11415, Springer, Cham, 2019.
[15] L. Zhang, Z. She, S. Ratschan, H. Hermanns and E. Hahn: Safety verification for probabilistic hybrid systems. In: Proc. International Conference on Computer Aided Verification, (2010), 196–211.