Антоація. Розглянуто метод синтезу скінченного автомата, специфікованого логічною мовою L*. Цей метод базується на трансляції специфікації у менш виразну мову L і застосуванні існуючого методу синтезу автомата за специфікацією у цій мові. Автомат, що синтезується у такий спосіб, може мати зайві (фіктивні) стани, які мають бути вилученими. Запропоновано простий метод перевірки станів на фіктивність.
Ключові слова: мова специфікації L*, ∃-формула, зворотне надслово, елімінація кванторів, синтез автомата, фіктивний стан.
Чеботарев Анатолий Николаевич,
доктор техн. наук, ведущий научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины,
e-mail: ancheb@gmail.com.