E.Asarin, O. Maler and A.Pnueli, Symbolic Controller Synthesis for Discrete and Timed Systems. (Символический синтез контроллера для дискретных и темпоризованных систем)

В работе предложены алгоритмы для символического синтеза управляющих автоматов в дискретном и непрерывном времени. На семантическом уровне синтез такого контроллера основан на построении выигрышной стратегии для игры, представленной обычным или темпоризованным (timed) автоматом. Алгоритм построения такой стратегии требуют поиска в пространстве состояний системы, размер которого растут экспоненциально при увеличении числа компонент. Символические методы позволяют при проведении такого поиска избежать прямого перебора состояний. Вместо этого множества состояний представляются логическими формулами. Хотя в наихудшем случае символические методы столь же трудоемки сколь и перечислительные, однако многие практические задачи успешно решаются символически. В данной статье символические методы распространяются с анализа на синтез и с чисто дискретных систем на системы реального времени. Надеемся, что эти результаты найдут применение для синтеза цифровых контроллеров реального времени, разработки асинхронных схем и других задач. [Postscript]