ИСТИНА

Мы предприняли попытку распространить ранее известный результат о разрешимости проблемы выполнимости темпоральной логики линейного времени на множествах вычислений конечных автоматов-преобразователей над свободной полугруппой на класс автоматов-преобразователей, работающих над коммутативными полугруппами. В таком автомате выполняемые действия могут мыслиться как движения робота в многомерном пространстве. Нам удалось установить, что алгоритмически неразрешимая задача проверки достижимости конфигураций в сетях Петри с ингибиторными дугами сводима к задаче проверки выполнимости FL-LTL на конечных автоматах преобразователях, работающих над вполне коммутативными полугруппами и абелевыми группами. Показано также, что даже задача верификации простейших свойств происшествия, которые выражаются формулами с одним темпоральным оператором, столь же сложна, как и задача проверки выполнимости формул арифметики Пресбургера.