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

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

Примеры

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

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

. Гибридный автомат Алура – Хенцингера $H$ включает в себя следующие компоненты: ^[1]

Конечное множество $X=\{x_{1},...,x_{n}\}$ вещественных переменных. Число $n$ называется размерностью $H$ . Позволять ${\dot {X}}$ быть набором $\{{\dot {x}}_{1},...,{\dot {x}}_{n}\}$ переменных, отмеченных точками, которые представляют первые производные во время непрерывных изменений, и пусть $X'$ быть набором $\{x'_{1},...,x'_{n}\}$ штриховых переменных, которые представляют значения в конце дискретного изменения.
Конечный мультиорграф $(V,E)$ . Вершины в $V$ называются режимами управления . Края в $E$ называются переключателями управления .
Три функции маркировки вершин init , inv и flow , которые назначаются каждому режиму управления. $v\in V$ три предиката. Каждое начальное условие init $(v)$ является предикатом, свободные переменные которого взяты из $X$ . Каждое инвариантное условие inv $(v)$ является предикатом, свободные переменные которого взяты из $X$ . Каждое условие потока $(v)$ является предикатом, свободные переменные которого взяты из $X\cup {\dot {X}}$ .

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

Функция маркировки кромок , которая назначается каждому переключателю управления. $e\in E$ предикат. Каждое условие прыжка $(e)$ является предикатом, свободные переменные которого взяты из $X\cup X'$ .
Конечное множество $\Sigma$ событий и функция маркировки ребер event : $E\rightarrow \Sigma$ который назначает каждому переключателю управления событие.

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

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

См. также

Автомат с таймером и автомат с сигналом , два вида гибридных автоматов.

Ссылки

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

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

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

[1] Хензингер, Т.А. «Теория гибридных автоматов». Труды одиннадцатого ежегодного симпозиума IEEE по логике в информатике (LICS), страницы 278–292, 1996.

[2] Алур, Р. и Дилл, Д.Л. «Теория временных автоматов». Теоретическая информатика (TCS), 126 (2), страницы 183–235, 1995.

[3] Хензингер, Томас А.; Копке, Питер В.; Пури, Анудж; Варайя, Правин (1 августа 1998 г.). «Что можно решить в отношении гибридных автоматов?». Журнал компьютерных и системных наук . 57 (1): 94–124. дои : 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] Берманн, Герд; Ларсен, Ким Г.; Расмуссен, Джейкоб И. (2005), «Оценочные автоматы с таймером: алгоритмы и приложения», Формальные методы для компонентов и объектов , Springer Berlin Heidelberg, стр. 162–182, CiteSeerX 10.1.1.106.7115 , doi : 10.1007/11561163_8 , ISBN 9783540291312

[6] Алур, Раджив; Триведи, Ашутош; Войчак, Доминик (17 апреля 2012 г.). Оптимальное планирование для многорежимных систем с постоянной скоростью . АКМ. стр. 75–84. CiteSeerX 10.1.1.299.946 . дои : 10.1145/2185632.2185647 . ISBN 9781450312202 . S2CID 14587340 .

[1]

[2]

[3]

[4]

[5]

[6]