Abstract. A class of 1-dimensional hybrid automata is defined, such that in each discrete state, the dynamics can be presented by different differential equations for different sets of initial values of continuous state, each dynamics duration is finite, and can be different for different sets of initial values of continuous state. Algorithms are proposed to solve problems of eliminating contradictions in objects that define the hybrid automata, of coordinating these objects with each other, calculating the minimum number of switchings, and estimating the minimum time for reachability of discrete states from the set of initial discrete states.

Keywords: hybrid automata, verification.