?
An efficient equivalence-checking algorithm for a model of programs with commutative and absorptive statements
P. 85-96.
Vladislav Podymov
We present an efficient equivalence-checking algorithm for a propositional model of programs with semantics based on (what we call) progressive monoids on the finite set of statements generated by relations of a specific form. We consider arbitrary set of relations for commutativity (relations of the form ab=ba for statements a, b) and left absorption (relations of the form ab=b for statements a, b) properties. The main results are a polynomial-time decidability for the equivalence problem in the considered case, and an explicit description of an equivalence-checking algorithm which terminates in time polynomial in size of programs.
Language:
English
Publication based on the results of:
In book
Vol. 2. , University of Rzeszow, 2015
Zakharov V., Джусупекова З., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, ...
Added: October 13, 2016
Vladislav Podymov, , in : CEUR Workshop Proceedings. Vol. 1492: Proceedings of the 24th International Workshop on Concurrency, Specification and Programming. Rzeszow, Poland, September 28-30, 2015.: CEUR Workshop Proceedings, 2015. P. 85-96.
We present an efficient equivalence-checking algorithm for a propositional model of programs with semantics based on (what we call) progressive monoids on the finite set of statements generated by relations of a specific form. We consider arbitrary set of relations for commutativity (relations of the form ab=ba for statements a, b) and left absorption (relations ...
Added: October 10, 2016
Zakharov V., Temerbekova G., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 523-530
Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In ...
Added: October 13, 2016
Zakharov V., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44
Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In some cases verification of such programs can be reduced to minimization and equivalence checking problems for this model of computation. To solve efficiently these problems certain requirements are imposed on a semigroup these transducers operate on. Minimization of ...
Added: October 13, 2016
Zakharov V., Жайлауова Ш. Р., Моделирование и анализ информационных систем 2017 Т. 24 № 4 С. 415-433
rst-order program schemata is one of the simplest models of sequential imperative
programs intended for solving verication and optimization problems. We consider the decidable rela tion of logical-thermal equivalence of these schemata and the problem of their size minimization while
preserving logical-thermal equivalence. We prove that this problem is decidable. Further we show that
the rst-order program schemata supplied ...
Added: October 12, 2017
Zakharov V., Труды Института системного программирования РАН 2015 Т. 27 № 2 С. 221-250
Finite state transducers extend the finite state automata to model functions on strings or lists. They may be used also as simple models of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. ...
Added: September 30, 2015
Zakharov V., Jaylauova S., Automatic Control and Computer Sciences 2017 Vol. 51 No. 7 P. 689-700
First-order program schemata represent one of the most simple models of sequential
imperative programs intended for solving verification and optimization problems. We consider the
decidable relation of logical–thermal equivalence on these schemata and the problem of their size
minimization while preserving logical–thermal equivalence. We prove that this problem is decidable.
Further we show that the first-order program schemata supplied ...
Added: December 19, 2017
Zakharov V.A., Lecture Notes in Computer Science 2015 Vol. 9270 P. 208-221
Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In this paper we introduce a uniform tech- nique for checking eectively functionality, k-valuedness, equivalence and inclusion for this model of computation in the case when a semigroup these transducers op- erate over is embeddable in a decidable group. ...
Added: September 30, 2015
Vladislav Podymov, Fundamenta Informaticae 2016 Vol. 147 No. 2-3 P. 315-336
For many program analysis problems it is useful to have means to efficiently prove that given programs have similar (equivalent) behaviors. Unfortunately, in most cases to prove the behavioral equivalence is an undecidable problem. A common way to overcome such undecidability is to consider a model of programs with an abstract semantics based on the ...
Added: October 9, 2016
Zakharov V., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753
Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In ...
Added: October 13, 2016
Shitov Y., / Cornell University. Series math "arxiv.org". 2014. No. 1406.2601.
We construct a nontrivial identity which holds in the semigroup of tropical 3-by-3 matrices. ...
Added: March 14, 2015
The symmetric Post Correspondence Problem, and errata for the freeness problem for matrix semigroups
Birget J., Talambutsa A., International Journal of Algebra and Computation 2022 Vol. 32 No. 6 P. 1261-1274
In this paper, we define the symmetric Post Correspondence Problem (PCP) and prove that it is undecidable. As an application, we show that the original proof of undecidability of the freeness problem for 3×3 integer matrix semigroups works for the symmetric PCP, but not for the PCP in general. ...
Added: December 9, 2022
Vikentyeva O., Полякова О. А., Пермь : Издательство Пермского национального исследовательского политехнического университета, 2019
The tutorial deals with the application of the basic principles of structured programming in complex software systems in the high-level C ++ language, which are demonstrated with meaningful examples. ...
Added: September 16, 2020
Zakharov V., Темербекова Г. Г., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 232-234.
Потоковые алгоритмы возникают при решении многих прикладных задач. В статье предложена модель потоковых программ- автоматов-преобразователей над полугруппами- и для нее была исследована проблема эквивалентности. В настоящей работе описан метод оптимизации потоковых программ. Этот метод является обобщением ранее известного подхода, предложенного в статье для минимизации автоматов-преобразователей. Решение задачи минимизации потоковых программ над группами представлено в статье ...
Added: October 13, 2016
Blank M., Advances in Mathematics 2022 Vol. 406 Article 108529
We study measure-theoretical aspects of torus piecewise isometries.
Not much is known about this type of dynamical systems, except for
the special case of one-dimensional interval exchange mappings. The
last case is fundamentally different from the general situation
in the presence of an invariant measure (Lebesgue measure), which
helps a lot in the analysis. Due to the absence of good ...
Added: June 26, 2022
Zakharov V., Новикова Т. А., Труды Института системного программирования РАН 2014 Т. 26 № 2 С. 245-268
It is generally accepted that to unify a pair of substitutions θ_1 and θ_2 means to find out a pair of substitutions η' and η'' such that the compositions θ_1 η' and θ_2 η'' are the same. Actually, unification is the problem of solving linear equations of the form θ_1 X=θ_2 Y in the semigroup ...
Added: September 30, 2015
Zakharov V., АРГАМАК-МЕДИА, 2016
Проблема эквивалентности программ состоит в том, чтобы для произвольной заданной пары программ выяснить, имеют ли эти программы одинаковое поведение. С этой проблемой сталкиваются в системном программировании при проведении оптимизирующих преобразований программ, их верификации, реорганизации, маскировке (обфускации), обнаружении уязвимостей и вредоносных фрагментов кода, и др. В данной монографии представлены различные виды моделей императивных (последовательных) и функциональных ...
Added: October 13, 2016
Высоцкий Л. И., Жуков В. В., Шуплецов М. С., В кн. : Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС-2018). Вып. 1.: М. : ИППМ РАН, 2018. С. 30-37.
При обнаружении ошибок или изменении
спецификации
проектируемой
сверхбольшой
интегральной схемы (СБИС) на поздних этапах
маршрута проектирования откат на более ранние этапы
проектирования и их повторное выполнение очень часто
становится непрактичным в силу существенных
временных затрат. Для целей сокращения времени
проектирования
в
современные
маршруты
проектирования интегрируют специальные этапы
функциональной коррекции схемы (англ. Engineering
Change Order, ECO). В основе указанного подхода лежит
анализ уже спроектированной схемы и построение
небольшой подсхемы-заплатки, внедрение которой в уже
синтезированную ...
Added: November 10, 2020
Zakharov V., Жайлауова Ш. Р., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 272-274.
В данной статье мы продолжаем поиск и исследование новых классов недетерминированных автоматов-преобразователей с разрешимой проблемой эквивалентности. Цель исследования~--- провести как можно более точную и подробную демаркацию границы между разрешимыми и неразрешимыми случаями проблемы эквивалентности для рассматриваемой модели вычислений. Мы рассматриваем один класс недетерминированных автоматов, работающих над выходным алфавитом из одной буквы. Характерная особенность рассматриваемых автоматов-преобразователей ...
Added: October 17, 2019
Avdoshin S. M., Набебин А. А., М. : ДМК Пресс, 2017
The textbook contains necessary information about universal and classical algebras, systems of axioms for the basic algebraic structures (groupoid, monoid, semi-groups, groups, partial orders, rings, fields). The basic cryptographic algorithms are described. Error-correcting codes - linear, cyclic, BCH are considered. Algorithms for designing of such codes are given. Many examples are shown. It is put ...
Added: August 19, 2016
Gorsky Evgeny, Mazin M., Journal of Algebraic Combinatorics 2014 Vol. 39 No. 1 P. 153-186
We continue the study of the rational-slope generalized q,t-Catalan numbers c m,n (q,t). We describe generalizations of the bijective constructions of J. Haglund and N. Loehr and use them to prove a weak symmetry property c m,n (q,1)=c m,n (1,q) for m=kn±1. We give a bijective proof of the full symmetry c m,n (q,t)=c m,n (t,q) for ...
Added: December 9, 2014
Герасимова И. А., Цветковская Т. А., Konson G., , in : Art History in the Context of Other Sciences in Modern World: Parallels and Interaction. : M. : Information and Publishing House Filin, 2020. P. 888-897.
In this interview, Irina Gerasimova, the General Director and Artistic Director of the Russian State Music, Television and Radio Center, discusses her experience of running Orpheus radio, the only Russian radio station broadcasting classical music. The commercial success of any media outlet is measured by its ratings in the conditions of market competition. The place ...
Added: May 9, 2021
Zakharov V., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 128-130.
It is shown how the verification of the equivalence of two-tape deterministic automata can be reduced to the problem of checking the equivalence of weakly nondeterministic finite automata-transformers working on the semigroup of prefix regular languages with the concatenation operation. ...
Added: June 14, 2018
Blank M., Russian Mathematical Surveys 2019 Vol. 74 No. 4 P. 758-760
We discuss the recurrence property, based on the representation of trajectories of the semigroup as realizations of a certain Markov chain for which necessary and sufficient conditions for the recurrence were obtained recently in [Blank2019]. Remark that a direct generalization of the recurrence property does not work well in the case of the semigroup action and one needs to make ...
Added: October 8, 2019