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

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

Примеры [ править ]

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

Формальное определение [ править ]

. Гибридный автомат Алура – Хенцингера $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$ который назначает каждому переключателю управления событие.

Сопутствующие модели [ править ]

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

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

Учитывая выразительность гибридных автоматов, неудивительно, что простые вопросы достижимости неразрешимы для общих гибридных автоматов. Фактически, прямое сокращение от счетных машин до гибридных автоматов с тремя переменными (две переменные для хранения значений счетчиков и одна для ограничения затрат в единицу времени на одно местоположение) доказывает неразрешимость проблемы достижимости для гибридных автоматов. Подкласс гибридных автоматов - это автоматы с таймером. ^[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]