Реактивный синтез

Реактивный синтез (или временной синтез ) — это область информатики , которая изучает автоматическую генерацию конечных автоматов (например, машин Мура ) на основе спецификаций высокого уровня (например, формул в линейной темпоральной логике ). «Реактивность» подчеркивает тот факт, что синтезированная машина взаимодействует с пользователем, считывая входные данные и производя выходные данные, и никогда не прекращает свою работу.

Проблема синтеза была предложена Алонсо Чёрчем в 1962 году. со спецификациями, представляющими собой формулы в монадической логике второго порядка , и конечные автоматы в виде цифровых схем.

См. также

• Синтез программы
• Проверка модели