Глава
An efficient equivalence-checking algorithm for a model of programs with commutative and absorptive statements
В книге
Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, которая вложима в некоторую конечно порожденную группу с разрешимой проблемой тождества. Ранее было установлено, что задача проверки $k$-значности конечных автоматов-преобразователей над свободными моноидами разрешима. Затем было показано, что эту задачу можно решить за время, полиномиальное относительно размера преобразователей и был предложен более общий метод анализа поведения автоматов преобразователей над полугруппами, вложимыми в разрешимые группы,. Однако применение этого метода было обосновано только для решения задачи проверки 2-значности автоматов-преобразователей. Цель данной работы - показать, что для любого $k, k\geq 1,$ за полиномиальное время проверять свойство $k$-значности конечных автоматов-преобразователей, работающих над полугруппой, вложимой в конечно порожденные разрешимые группы.
В статье освещаются социально-правовые аспекты организации общественных работ как наиболее действенной меры обеспечения временной занятости, поддержки социальной стабильности и полноценной социальной защиты безработных граждан
This book constitutes the refereed proceedings of the 13th International Haifa Verification Conference, HVC 2017, held in Haifa, Israel in November 2017. The 13 revised full papers presented together with 4 poster and 5 tool demo papers were carefully reviewed and selected from 45 submissions. They are dedicated to advance the state of the art and state of the practice in verification and testing and are discussing future directions of testing and verification for hardware, software, and complex hybrid systems.
Эффективная разрешимость проблемы л-т эквивалентности дает возможность приступить к решению задачи минимизации - построения схемы программ наименьшего размера, л-т эквивалентной заданной схеме. Чтобы отыскать ее решение, заметим, что модель вычислений стандартных схем программ сходна модели вычислений автоматов-преобразователей, работающих над полугруппами. Ранее был предложен метод минимизации автоматов-преобра\-зо\-вателей, работающих над упорядоченными левосократимыми полугруппами. В данной заметке мы покажем, что этим методом можно воспользоваться для минимизации стандартных схем программ относительно л-т эквивалентности в случае, когда эти схемы определены над ортогональными консервативными подстановками.
Проблема эквивалентности программ состоит в том, чтобы для произвольной заданной пары программ выяснить, имеют ли эти программы одинаковое поведение. С этой проблемой сталкиваются в системном программировании при проведении оптимизирующих преобразований программ, их верификации, реорганизации, маскировке (обфускации), обнаружении уязвимостей и вредоносных фрагментов кода, и др. В данной монографии представлены различные виды моделей императивных (последовательных) и функциональных (рекурсивных) программ и подробно описан и исследован общий метод решения проблемы эквивалентности программ – метод совместных вычислений. С его помощью можно конструировать алгоритмы проверки эквивалентности разных видов программ.
В сборнике представлены антирисковые программы общеобразовательных организаций Московской области. Представлены риски и пути их минимизации в условиях модернизации образования.