Гибридный автомат - Hybrid automaton

В теории автоматов , A гибридный автомат ( во множественном числе: гибридные автоматы или гибридные автоматон ) представляет собой математическая модель для точного описания систем , в которых цифровые вычислительных процессах взаимодействуют с аналоговыми физическими процессами. Гибридный автомат - это конечный автомат с конечным набором непрерывных переменных, значения которых описываются набором обыкновенных дифференциальных уравнений . Эта комбинированная спецификация дискретного и непрерывного поведения позволяет моделировать и анализировать динамические системы, содержащие как цифровые, так и аналоговые компоненты.

Примеры

Простым примером является система комнатный термостат- обогреватель, в которой температура в комнате изменяется в соответствии с законами термодинамики и состоянием обогревателя ( вкл. / Выкл.); термостат определяет температуру, выполняет определенные вычисления и включает и выключает нагреватель. В целом гибридные автоматы использовались для моделирования и анализа множества встроенных систем, включая системы управления транспортными средствами, системы управления воздушным движением , мобильных роботов и процессы из системной биологии .

Формальное определение

Алуры-Henzinger гибридный автомат включает в себя следующие компоненты:

  • Конечный набор переменных с действительными номерами. Число называется размерность в . Позвольте быть набором переменных, отмеченных пунктиром, которые представляют первые производные во время непрерывного изменения, и пусть будет набором переменных со штрихом, которые представляют значения в конце дискретного изменения.
  • Конечный мультииграф . Вершины в называются режимами управления . Края в называются контрольными переключателями .
  • Три функции маркировки вершин: init , inv и flow, которые назначают каждому режиму управления по три предиката. Каждое начальное условие init - это предикат, из которого взяты свободные переменные . Каждое инвариантное условие inv - это предикат, из которого берутся свободные переменные . Каждый поток условий потока является предикатом, свободные переменные которого берутся из .

Итак, это помеченный мультидиграф .

  • Функция пограничной маркировки скачок , который назначает каждому контроля переключения предиката. Каждое условие перехода jump - это предикат, из которого взяты свободные переменные .
  • Конечный набор событий и событие функции маркировки краев : которое назначает каждому управляющему переключателю событие.

Связанные модели

Гибридные автоматы бывают нескольких видов: гибридный автомат Алура-Хенцингера - популярная модель; он был разработан в первую очередь для алгоритмического анализа проверки моделей гибридных систем . HyTech инструмент проверки модели на основе этой модели. Модель гибридного автомата ввода / вывода была разработана совсем недавно. Эта модель позволяет композиционное моделирование и анализ гибридных систем. Другой формализм, который полезен для моделирования реализаций гибридного автомата, - это ленивый линейный гибридный автомат .

Разрешаемый подкласс гибридных автоматов

Учитывая выразительность гибридных автоматов, неудивительно, что простые вопросы о достижимости неразрешимы для общих гибридных автоматов. Фактически, прямое сокращение от машины счетчика до гибридных автоматов с тремя переменными (две переменные для хранения значений счетчиков и одна для ограничения расхода единицы времени на местоположение) доказывает неразрешимость проблемы достижимости для гибридных автоматов. Подкласс гибридных автоматов - это временные автоматы, в которых все переменные растут с равномерной скоростью (т. Е. Все непрерывные переменные имеют производную 1). Такие ограниченные переменные могут действовать как переменные таймера, называемые часами, и позволяют моделировать системы реального времени. Другие известные разрешимые подклассы включают инициализированные прямоугольные гибридные автоматы, системы одномерных кусочно-постоянных производных (PCD), оцениваемые временные автоматы и многорежимные системы с постоянной скоростью.

Смотрите также

Рекомендации

  1. ^ Хенцингер, Т.А. "Теория гибридных автоматов". Материалы одиннадцатого ежегодного симпозиума IEEE по логике в компьютерных науках (LICS), страницы 278-292, 1996.
  2. ^ Алур, Р. и Дилл, DL "Теория временных автоматов". Теоретическая информатика (TCS), 126 (2), страницы 183-235, 1995.
  3. ^ Henzinger, Thomas A .; Копке, Питер В .; Пури, Анудж; Варайя, Правин (1998-08-01). «Что можно решить о гибридных автоматах?». Журнал компьютерных и системных наук . 57 (1): 94–124. DOI : 10.1006 / jcss.1998.1581 . hdl : 1813/7198 . ISSN  0022-0000 .
  4. ^ Асарин, Евгений; Шнайдер, Херардо; Йовин, Серджио (2001), «О разрешимости проблемы достижимости для плоских дифференциальных включений», Гибридные системы: вычисления и управление , Springer Berlin Heidelberg, стр. 89–104, CiteSeerX  10.1.1.23.8172 , doi : 10.1007 / 3 -540-45351-2_11 , ISBN 9783540418665
  5. ^ Берманн, Герд; Ларсен, Ким Дж .; Расмуссен, Яков I. (2005), "Цене Timed Automata: Алгоритмы и приложения", формальные методы для компонентов и объектов , Springer Berlin Heidelberg, стр 162-182,. CiteSeerX  10.1.1.106.7115 , DOI : 10.1007 / 11561163_8 , ISBN 9783540291312
  6. ^ Алур, Раджив; Триведи, Ашутош; Войтчак, Доминик (17 апреля 2012 г.). Оптимальное планирование для многомодовых систем с постоянной скоростью . ACM. С. 75–84. CiteSeerX  10.1.1.299.946 . DOI : 10.1145 / 2185632.2185647 . ISBN 9781450312202.

дальнейшее чтение

  • Раджив Алур , Костас Куркубетис, Николас Хальбвакс, Томас А. Хензингер, Пей-Син Хо, Ксавье Николлин, Альфредо Оливеро, Джозеф Сифакис и Серджио Йовин Алгоритмический анализ гибридных систем . Теоретическая информатика, том 138 (1), страницы 3–34, 1995.
  • Нэнси Линч , Роберто Сегала, Фриц Ваандрагер, Hybrid I / O Automata . Информация и вычисления, том 185 (1), страницы 103–157, 2003 г.