Реактивный синтез - Reactive synthesis
Реактивный синтез (или темпоральный синтез) - поле Информатика который изучает автоматическую генерацию конечных автоматов (например, Машины Мура ) из спецификаций высокого уровня (например, формул в линейная темпоральная логика ). «Реактивность» подчеркивает тот факт, что синтезированная машина взаимодействует с пользователем, считывая ввод и создавая вывод, и никогда не останавливает свою работу.
Проблема синтеза была введена Церковь Алонсо в 1962 г. [1], где спецификации являются формулами в монадическая логика второго порядка и конечные автоматы в виде цифровых схем.
Смотрите также
использованная литература
- ^ Церковь, Алонсо (1962). «Логика, арифметика и автоматы». Международный конгресс математиков. С. 23–35.