?
Об эквивалентности ограниченно недетерминированных автоматов-преобразователей над полугруппами
С. 100-102.
Захаров В. А.
Показано, что задача проверки k-значности конечного автомата-преобразователя, работающего над полугруппой, вложимой в разрешимую группу, может быть решена за время, полиномиальное относительно размера автомата.
Язык:
русский
В книге
Каз. : Отечество, 2014
Подымов В. В., Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика 2012 № 4 С. 37-43
В работе предложен метод решения проблемы эквивалентности линейных унарных рекурсивных программ. Основная его идея состоит в сведении проблемы эквивалентности к известным задачам на графах и задачам теории групп. Выделен класс программных семантик, для которых проблема эквивалентности рассматриваемых программ разрешима за полиномиальное время с использованием предложенной методики. ...
Добавлено: 29 сентября 2015 г.
Подымов В. В., Молчанов А. Э., В кн. : Материалы XVIII международной конференции "Проблемы теоретической кибернетики" (Пенза, 19-23 июня 2017 г.). : М. : МАКС Пресс, 2017. С. 174-176.
Проблема эквивалентности программ формулируется так: выяснить, имеют ли две программы схожие (эквивалентные) поведения. Известен алгоритм полиномиального сведения проблемы эквивалентности в перегородчатых моделях программ с процедурами к двум проблемам в моделях программ без процедур с той же семантикой программных операторов: эквивалентности и совместного останова. Проблема совместного останова формулируется так: выяснить, существует ли общий контекст работы программ, ...
Добавлено: 22 октября 2017 г.
Захаров В. А., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753
Автоматы-преобразователи над полугруппами можно использовать в качестве модели последовательных реагирующих программ, работающих в постоянном взаимодействии со своим окружением. Получив очередную порцию данных, реагирующая программа выполняет некоторую последовательность действий и предъявляет результат. Такие программы возникают при проектировании компьютерных драйверов, алгоритмов, работающих в оперативном режиме, сетевых коммутаторов. Во многих случаях проблема верификации программ такого рода может быть ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Козлова Д. Г., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 204-206.
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2014 Т. 26 № 2 С. 245-268
Задача унификации пары подстановок θ_1 и θ_2 состоит в вычислении такой пары подстановок η' и η'', чтобы композиции θ_1 η' и θ_2 η'' были равны. По существу, задача унификации подстановок равносильна задаче решения линейных уравнений вида θ_1 X=θ_2 Y в полугруппе подстановок. Но некоторые линейные уравнения над подстановками также можно рассматривать как новые варианты задачи ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Жайлауова Ш. Р., Моделирование и анализ информационных систем 2017 Т. 24 № 4 С. 415-433
Стандартные схемы программ - это одна из наиболее простых моделей последовательных императивных программ, предназначенная для решения задач оптимизации и верификации программ. Мы рассматриваем разрешимое отношение логико-термальной эквивалентности стандартных схем программ и задачу минимизации их размера при условии сохранением отношения логико-термальной эквивалентности. Нами доказано, что эта задача является алгоритмически разрешимой. Далее показано, что стандартные схемы программ ...
Добавлено: 12 октября 2017 г.
Захаров В. А., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 128-130.
Показано, каким образом задача проверки эквивалентности двухленточных детерминированных автоматов может быть сведена к задаче проверки эквивалентности слабо недетерминированных конечных автоматов-преобразователей, работающих над полугруппой префиксных регулярных языков с операцией конкатенации. ...
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303-324
Добавлено: 14 июня 2018 г.
Гнатенко А. Р., Захаров В. А., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776-785
Добавлено: 17 января 2022 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2011 Т. 21 С. 141-166
Для решения многих задач системного программирования, к числу которых относятся задачи реорганизации программ, деобфускации программ, выявления уязвимостей в программном коде и др., желательно иметь инструментальное средство, позволяющее обнаруживать фрагменты программ, имеющие сходное поведение. Современные средства обнаружения программных клонов позволяют выявлять лишь фрагменты программ, имеющие сходное синтаксическое устройство, поскольку более глубокий семантический анализ программ сталкивается с ...
Добавлено: 30 сентября 2015 г.
Подымов В. В., Захаров В. А., Труды Института системного программирования РАН 2014 Т. 26 № 3 С. 145-166
В статье исследована задача проверки эквивалентности последовательных программ, некоторые операторы которых обладают свойствами перестановочности и подавления. Два оператора считаются перестановочными, если результат их последовательного выполнения не зависит от порядка, в котором эти операторы выполняются. Считается, что оператор b подавляет оператор a, если последовательное выполнение операторов a и b дает такой же результат, что и выполнение ...
Добавлено: 29 сентября 2015 г.
Соснин А. В., Балакина Ю. В., Кащихин А. Н., Вестник Санкт-Петербургского университета. Язык и литература 2022 Т. 19 № 1 С. 125-148
Статья посвящена оценке качества перевода: рассматриваются прикладные и прагматические аспекты оценки качества перевода в условиях стремительного увеличения
числа текстов, которые требуется перевести для обеспечения межкультурной коммуникации; суммируется большое количество подходов, каждый из которых при оценке
качества перевода имеет свои преимущества и недостатки; анализируется соотношение категорий адекватности и эквивалентности перевода как основных параметров
оценки. Заключается, что эквивалентность ориентирована на ...
Добавлено: 31 мая 2022 г.
Захаров В. А., Темербекова Г. Г., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 232-234.
Потоковые алгоритмы возникают при решении многих прикладных задач. В статье предложена модель потоковых программ- автоматов-преобразователей над полугруппами- и для нее была исследована проблема эквивалентности. В настоящей работе описан метод оптимизации потоковых программ. Этот метод является обобщением ранее известного подхода, предложенного в статье для минимизации автоматов-преобразователей. Решение задачи минимизации потоковых программ над группами представлено в статье ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Kozlova D., , in : Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016. Vol. 1698.: Humboldt-Universität zu Berlin, 2016. P. 233-244.
Добавлено: 13 октября 2016 г.
Гнатенко А. Р., Захаров В. А., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 131-133.
Проведено сравнение выразительных возможностей темпоральной логики LP-CTL*. В этой логике были выделены два класса формул (фрагмента) LP-1-LTL и LP-n-LTL и показано, что фрагмент LP-1-LTL превосходит по выразительным возможностям известную темпоральную логику линейного времени LTL, а фрагмент LP-n-LTL имеет такие же выразительные возможности, что и монадическая логика второго порядка с одной функцией следования S1S. ...
Добавлено: 14 июня 2018 г.
Захаров В. А., Джусупекова З., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, ...
Добавлено: 13 октября 2016 г.
Захаров В. А., Подымов В. В., Труды Института системного программирования РАН 2015 Т. 27 № 4
На примере двух моделей программ показано, что задача оптимизации размера программ может быть эффективно решена при помощи процедур проверки эквивалентности программ в рассматриваемых моделях. Основной результат работы – полиномиальные по времени алгоритмы минимизации конечных детерминированных автоматов-преобразователей над конечно порожденными разрешимыми группами и схем последовательных программ, семантика которых определяется конечно порожденными разрешимыми упорядоченными левосократимыми полугруппами. Предложенные ...
Добавлено: 13 октября 2015 г.
Захаров В. А., Жайлауова Ш. Р., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 272-274.
В данной статье мы продолжаем поиск и исследование новых классов недетерминированных автоматов-преобразователей с разрешимой проблемой эквивалентности. Цель исследования~--- провести как можно более точную и подробную демаркацию границы между разрешимыми и неразрешимыми случаями проблемы эквивалентности для рассматриваемой модели вычислений. Мы рассматриваем один класс недетерминированных автоматов, работающих над выходным алфавитом из одной буквы. Характерная особенность рассматриваемых автоматов-преобразователей ...
Добавлено: 17 октября 2019 г.
Захаров В. А., Automatic Control and Computer Sciences (AC&CS), Switzerland 2021 Vol. 55 No. 7 P. 670-701
Добавлено: 17 января 2022 г.
Захаров В. А., Новикова Т. А., Труды Института системного программирования РАН 2012 Т. 22 С. 435-455
Логико-термальная эквивалентность программ – это одно из наиболее слабых отношений эквивалентности программ, аппроксимирующих отношение функциональной эквивалентности и обладающих разрешающим алгоритмом. В данной статье предложена новая модификация алгоритма проверки логико-термальной эквивалентности программ, основанная на операции вычисления точной нижней грани в решетке конечных подстановок. Показано, что трудоемкость предложенного алгоритма оценивается величиной O(n6) , где n - размер ...
Добавлено: 30 сентября 2015 г.
Захаров В. А., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44
Добавлено: 13 октября 2016 г.
Гнатенко А. Р., Захаров В. А., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356-371
К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, ...
Добавлено: 17 января 2022 г.
Захаров В. А., Новикова Т. А., В кн. : Дискретные модели в теории управляющих систем : IX Международная конференция, Москва и Подмосковье, 20-22 мая 2015 г.: Труды. : М. : МАКС Пресс, 2015. С. 173-176.
В статье предложена новая модель последовательных императивных программ, использующих средства работы с динамической памятью (указателями, списками и пр.) ...
Добавлено: 12 октября 2015 г.
Подымов В. В., Вестник Московского университета. Серия 15: Вычислительная математика и кибернетика 2013 № 1 С. 21-27
В работе предложен метод решения проблемы сильной эквивалентности металинейных унарных рекурсивных программ, позволяющий описать полиномиальный по времени работы разрешающий алгоритм. Основная идея метода состоит в анализе ориентированного графа, описывающего всевозможные совместные вычисления программ, и сведении проблемы сильной эквивалентности к проблеме достижимости вершины в графе. ...
Добавлено: 29 сентября 2015 г.