@inproceedings{ad007eec9a2a458581e1bd83c9fedcf1,
title = "Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection",
abstract = "Hybrid systems are dynamical systems that include both continuous and discrete changes. Some hybrid systems involve a large or infinite number of discrete changes within an infinitesimal-width region of phase space. Systems with sliding mode are typical examples of such hybrid systems. It is difficult to analyze such hybrid systems through ordinary numerical simulation, since the time required for simulation increases in proportion to the number of discrete changes. In this paper, we propose a method to symbolically analyze such models involving numerous discrete changes by detecting loops and checking loop invariants of the model{\textquoteright}s behavior. The method handles parameterized hybrid systems and checks inclusion of parameterized states focusing on the values of a switching function that dominate the dynamics of sliding mode. We implemented the main part of the method in our symbolic hybrid system simulator HyLaGI, and conducted analysis of example models.",
keywords = "Hybrid systems, Loop invariants, Sliding mode, Symbolic analysis, Verification",
author = "Kenichi Betsuno and Shota Matsumoto and Kazunori Ueda",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 6th International Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, CyPhy 2016 ; Conference date: 06-10-2016 Through 06-10-2016",
year = "2017",
doi = "10.1007/978-3-319-51738-4_2",
language = "English",
isbn = "9783319517377",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "17--30",
editor = "Rafael Wisniewski and Mousavi, {Mohammad Reza} and Christian Berger",
booktitle = "Cyber Physical Systems",
}