2:00 PM - 2:20 PM
[2E3-OS-13b-03] Benchmarking hybrid systems modeling tools based on the reachability analysis of parameterized models
Keywords:Hybrid systems, Reachability analysis, Parameterized models
Hybrid systems are dynamical systems which include both continuous and discrete changes. HydLa is a modeling language for hybrid systems, and HyLaGI is an implementation of HydLa being developed in our research group.
HyLaGI is based on symbolic computation and can handle parameterized models rigorously. Other tools that can handle parameterized hybrid systems include SpaceEx and dReach. SpaceEx computes convex-set inclusion of orbits of variables using numerical computation, while dReach solves reachability problems rigorously after extending both target regions and the model. Although they can all handle parameterized models, they are based on quite different approaches and have not been compared in depth.
In this paper, we evaluate and study the characteristics of these modeling tools based on some parameterized models for benchmarking.
HyLaGI is based on symbolic computation and can handle parameterized models rigorously. Other tools that can handle parameterized hybrid systems include SpaceEx and dReach. SpaceEx computes convex-set inclusion of orbits of variables using numerical computation, while dReach solves reachability problems rigorously after extending both target regions and the model. Although they can all handle parameterized models, they are based on quite different approaches and have not been compared in depth.
In this paper, we evaluate and study the characteristics of these modeling tools based on some parameterized models for benchmarking.
Authentication for paper PDF access
A password is required to view paper PDFs. If you are a registered participant, please log on the site from Participant Log In.
You could view the PDF with entering the PDF viewing password bellow.