Stability Analysis of Switched Fuzzy Systems Via Model Checking

Switched fuzzy systems can be used to describe the hybrid systems with fuzziness. Their stability issue is the most important one and has received significant attention. Most of the existing methods to study it are based on Lyapunov functions. However, the existence of such functions is difficult to establish. This paper presents a new method to analyze the stability. A switched fuzzy system with a Takagi-Sugeno (T-S) fuzzy model is first transformed to a hybrid automaton (HA) that is linearized. The reachability of this linearized one is then checked by the model checker PHAVer. Finally, the stability is obtained by analyzing the reachability. It is shown that a switched fuzzy system and its corresponding HA have the same behavior and that the linearization does not affect the stability analysis. We demonstrate the effectiveness of our method through a case study on a differential-drive two-wheeled mobile robot.