Search results

Filters

  • Journals
  • Authors
  • Keywords
  • Date
  • Type

Search results

Number of results: 1
items per page: 25 50 75
Sort by:
Download PDF Download RIS Download Bibtex

Abstract

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.
Go to article

Bibliography

[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.
Go to article

Authors and Affiliations

Eugénio Miguel Alexandre Rocha
1
Kelly Patricia Murillo
1

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

This page uses 'cookies'. Learn more