Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection

Kenichi Betsuno, Shota Matsumoto, Kazunori Ueda

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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’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.

    Original languageEnglish
    Title of host publicationCyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers
    PublisherSpringer Verlag
    Pages17-30
    Number of pages14
    Volume10107 LNCS
    ISBN (Print)9783319517377
    DOIs
    Publication statusPublished - 2017
    Event6th International Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, CyPhy 2016 - Pittsburgh, United States
    Duration: 2016 Oct 62016 Oct 6

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume10107 LNCS
    ISSN (Print)03029743
    ISSN (Electronic)16113349

    Other

    Other6th International Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, CyPhy 2016
    CountryUnited States
    CityPittsburgh
    Period16/10/616/10/6

    Fingerprint

    Symbolic Analysis
    Hybrid systems
    Hybrid Systems
    Sliding Mode
    Switching functions
    Phase Space
    Dynamical systems
    Simulator
    Proportion
    Inclusion
    Simulators
    Dynamical system
    Model
    Numerical Simulation
    Invariant
    Computer simulation
    Simulation

    Keywords

    • Hybrid systems
    • Loop invariants
    • Sliding mode
    • Symbolic analysis
    • Verification

    ASJC Scopus subject areas

    • Theoretical Computer Science
    • Computer Science(all)

    Cite this

    Betsuno, K., Matsumoto, S., & Ueda, K. (2017). Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. In Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers (Vol. 10107 LNCS, pp. 17-30). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10107 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-51738-4_2

    Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. / Betsuno, Kenichi; Matsumoto, Shota; Ueda, Kazunori.

    Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers. Vol. 10107 LNCS Springer Verlag, 2017. p. 17-30 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10107 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Betsuno, K, Matsumoto, S & Ueda, K 2017, Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. in Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers. vol. 10107 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10107 LNCS, Springer Verlag, pp. 17-30, 6th International Workshop on Design, Modeling and Evaluation of Cyber Physical Systems, CyPhy 2016, Pittsburgh, United States, 16/10/6. https://doi.org/10.1007/978-3-319-51738-4_2
    Betsuno K, Matsumoto S, Ueda K. Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. In Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers. Vol. 10107 LNCS. Springer Verlag. 2017. p. 17-30. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-51738-4_2
    Betsuno, Kenichi ; Matsumoto, Shota ; Ueda, Kazunori. / Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection. Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers. Vol. 10107 LNCS Springer Verlag, 2017. pp. 17-30 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @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’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",
    year = "2017",
    doi = "10.1007/978-3-319-51738-4_2",
    language = "English",
    isbn = "9783319517377",
    volume = "10107 LNCS",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    publisher = "Springer Verlag",
    pages = "17--30",
    booktitle = "Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers",
    address = "Germany",

    }

    TY - GEN

    T1 - Symbolic analysis of hybrid systems involving numerous discrete changes using loop detection

    AU - Betsuno, Kenichi

    AU - Matsumoto, Shota

    AU - Ueda, Kazunori

    PY - 2017

    Y1 - 2017

    N2 - 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’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.

    AB - 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’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.

    KW - Hybrid systems

    KW - Loop invariants

    KW - Sliding mode

    KW - Symbolic analysis

    KW - Verification

    UR - http://www.scopus.com/inward/record.url?scp=85010953539&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=85010953539&partnerID=8YFLogxK

    U2 - 10.1007/978-3-319-51738-4_2

    DO - 10.1007/978-3-319-51738-4_2

    M3 - Conference contribution

    SN - 9783319517377

    VL - 10107 LNCS

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 17

    EP - 30

    BT - Cyber Physical Systems: Design, Modeling, and Evaluation - 6th International Workshop, CyPhy 2016, Revised Selected Papers

    PB - Springer Verlag

    ER -