Abstract: The model checking problem for initialized multirate hybrid systems is investigated, which is to check whether or not an initialized multirate automaton satisfies a property described by a hybrid interval temporal logic (HITL) formula. Firstly, some rules are defined to translate an HITL formula to an interval temporal logic (ITL) formula. Then, an equivalence relation over state spaces of multirate automata is defined to construct region automata from multirate automata. By constructing a labeled finite state automaton from a region automaton, the model checking issue for initialized multirate automata is translated to the same issue for ITL. Thus, by using the model checking algorithms for ITL and the translating rules defined in this paper, the model checking problem for initialized multirate hybrid systems can be solved.

Key words: model checking, hybrid systems, multirate automata, interval temporal logic