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

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

Примеры

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

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

An Гибридный автомат Алур-Хенцингер ${ displaystyle H}$ состоит из следующих компонентов:^[1]

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

Так что это маркированный мультидиграф.

• Функция маркировки краев Прыгать который назначает каждому переключателю управления ${ displaystyle e in E}$ предикат. Каждое условие прыжка Прыгать${ Displaystyle (е)}$ это предикат, свободные переменные которого из ${ Displaystyle X чашка X '}$.
• Конечное множество ${ displaystyle Sigma}$ событий и функция маркировки краев мероприятие: ${ Displaystyle E rightarrow Sigma}$ который присваивает каждому переключателю управления событие.

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

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

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

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

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

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

• Автомат с синхронизацией и Сигнальный автомат, два вида гибридных автоматов

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

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