Premium
On Verification and Parameter Design in Hybrid Automaton Using Invariant
Author(s) -
Wang LiLi,
Zanma Tadanao,
Ishida Muneaki
Publication year - 2009
Publication title -
ieej transactions on electrical and electronic engineering
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.254
H-Index - 30
eISSN - 1931-4981
pISSN - 1931-4973
DOI - 10.1002/tee.20480
Subject(s) - automaton , hybrid automaton , invariant (physics) , hybrid system , computer science , finite state machine , state (computer science) , theoretical computer science , model checking , constant (computer programming) , algorithm , programming language , mathematics , machine learning , mathematical physics
Invariants for hybrid automata are determined from predicates that are constant for every reachable state in the automata. These invariants can be used to verify a given specification by exploiting their characteristics. In this paper, a switched system driven by discrete inputs is used as an example of a hybrid dynamical system. For the system, we propose a verification method for a given specification based on the concept of invariants and a design policy of parameters with which the given specification is satisfied. Some numerical and experimental results are provided to show the validity of the proposed method. Copyright © 2009 Institute of Electrical Engineers of Japan. Published by John Wiley & Sons, Inc.