Efficient choice of parameters on delta-reachability bounded hybrid systems

• Autorzy: Rocha Eugénio Miguel Alexandre , Murillo Kelly Patricia

Identyfikatory

DOI

10.24425/acs.2021.139730

• Języki publikacji: EN

Abstrakty

EN

Hybrid systems (HS) are roughly described as a set of discrete state transitions and continuous dynamics modeled by differential equations. Parametric HS may be constructed by having parameters on the differential equations, initial conditions, jump conditions, or a combination of the previous ones. In real applications, the best solution is obtained by a set of metrics functional over the set of solutions generated from a finite set of parameters. This paper examines the choice of parameters on delta-reachability bounded hybrid systems. We present an efficient model based on the tool pHL-MT to benchmark the HS solutions (based on dReach), and a non-parametric frontier analysis approach, relying on multidirectional efficiency analysis (MEA). Three numerical examples of epidemic models with variable growth infectivity are presented, namely: when the variable of infected individuals oscillates around some endemic (non-autonomous) equilibrium; when there is an asymptotically stable non-trivial attractor; and in the presence of bump functions.

Słowa kluczowe

EN

bounded hybrid system; safety property; delta-reachability; multidirectional efficiency analysis

• Wydawca: Polish Academy of Sciences, Committee of Automatic Control and Robotics
• Czasopismo: Archives of Control Sciences
• Rocznik: 2021
• Tom: Vol. 31, No. 4
• Strony: 781--794
• Opis fizyczny: Bibliogr. 15 poz., rys., tab., wykr., wzory

Twórcy

autor

Rocha Eugénio Miguel Alexandre

• Center for Research and Development in Mathematics and Applications, University of Aveiro, 3810-193 Aveiro, Portugal
• Department of Mathematics, University of Aveiro, 3810-193 Aveiro, Portugal

autor

Murillo Kelly Patricia

• Center for Research and Development in Mathematics and Applications, University of Aveiro, 3810-193 Aveiro, Portugal
• Department of Mathematics, University of Aveiro, 3810-193 Aveiro, Portugal

Bibliografia

• [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.

Uwagi

1. The authors were supported by the Center for Research and Development in Mathematics and Applications (CIDMA) through the Portuguese Foundation for Science and Technology (FCT - Fundação para a Ciência e a Tecnologia), references UIDB/04106/2020 and UIDP/04106/2020. Murillo was also supported by national funds (OE), through FCT, I.P., in the scope of the framework contract foreseen in the numbers 4, 5 and 6 of the article 23 of the Decree-Law 57/2016, of August 29, changed by Law 57/2017, of July 19.

2. Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).