Анотація. Визначено клас 1-вимірних гібридних автоматів, у яких у кожному дискретному стані для різних множин початкових значень неперервного стану динаміка може бути представлена різними диференціальними рівняннями, та задано скінченну тривалість цієї динаміки, яка може бути різною для різних множин початкових значень неперервного стану. Запропоновано алгоритми розв’язання задач вилучення суперечностей в об’єктах, які визначають гібридний автомат, узгодження цих об’єктів один з одним, знаходження мінімального числа перемикань та оцінки мінімального часу, за який дискретні стани досяжні з множини початкових дискретних станів .

Ключові слова: гібридні автомати, верифікація.