Аннотация. Игровые модели широко используются при решении задач реализуемости, синтеза и верификации реактивных систем. Для решения таких задач в статье рассматривается автоматный подход, основанный на понятии согласованности автоматов или их логических спецификаций. Соответствующие методы существенно отличаются от тех, которые используются в игровом контексте. Показано, как эти методы можно применять для синтеза выигрышной стратегии в игре двух лиц, не связанной с проектированием реактивных систем.

Ключевые слова: язык спецификации L, согласование автоматов, синтез автомата, модель игры, выигрышная стратегия.