On Verification and Parameter Design in Hybrid Automaton Using Invariant
Lili Wang, Tadanao Zanma, Muneaki Ishida · IEEJ Transactions on Electrical and Electronic Engineering · 2009
Abstract 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.