### ?

## An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements

Fundamenta Informaticae. 2016. Vol. 147. No. 2-3. P. 315-336.

Vladislav Podymov

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 real one, in which only some simple properties are captured, and to provide an efficient equivalence-checking algorithm for the model. We focus on two kinds of properties of data-modifying statements of imperative programs. Statements a and b are commutative, if the execution of sequences ab and ba lead to the same result. A statement b is (left-)absorptive for a statement a, if the execution of sequences ab and b lead to the same result. We consider propositional program models in which commutativity and absorption properties are caprtured (CA-models). Formally, data states for a CA-model are elements of a monoid over the set of statement symbols, defined by an arbitrary set of relations of the form ab = ba (for commutativity) and ab = b (for absorption). We propose an equivalence-checking algorithm for CA-models based on (what we call) progressive monoids. The algorithm terminates in time polynomial in size of programs. As a consequence, we prove a polynomial-time decidability for the equivalence problem in such CA-models.

Priority areas:
mathematics

Language:
English

Publication based on the results of:

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

Shitov Y., A semigroup identity for tropical 3x3 matrices / 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

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

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

Р.С. Авдеев, Горфинкель Н. Е., Функциональный анализ и его приложения 2012 Т. 46 № 3 С. 1-15

For all spherical homogeneous spaces G/H, where G is a simply connected semisimple algebraic group and H a connected solvable subgroup of G, we compute the spectra of representations of G on spaces of regular sections of homogeneous line bundles over G/H. ...

Added: February 25, 2014

Vladislav Podymov, , in : Concurrency, Specification & Programming. 24th International Workshop, CS&P 2015. Rzeszow, Poland, September 28-30, 2015. Proceedings. Vol. 2.: University of Rzeszow, 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 11, 2015

Zakharov V., Джусупекова З., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.

Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, ...

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

Р.С. Авдеев, Известия РАН. Серия математическая 2010 Т. 74 № 6 С. 3-26

The extended weight semigroup of a homogeneous space G/H of a connected semisimple algebraic group G characterizes the spectra of the representations of G on spaces of regular sections of homogeneous line bundles over G/H, including the space of regular functions on G/H. We compute the extended weight semigroups for all strictly irreducible affine spherical ...

Added: February 25, 2014

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., 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

Gorsky E., Mazin M., Vazirani M., Electronic Journal of Combinatorics 2017 Vol. 24 No. 3 P. 1-29

We study the relationship between rational slope Dyck paths and invariant subsets of Z; extending the work of the rst two authors in the relatively prime case. We also find a bijection between (dn;dm)-Dyck paths and d-tuples of (n;m)-Dyck paths endowed with certain gluing data. These are the rst steps towards understanding the relationship between rational slope Catalan combinatorics ...

Added: October 13, 2017

Р.С. Авдеев, Математический сборник 2012 Т. 203 № 11 С. 3-22

For an affine spherical homogeneous space G/H of a connected semisimple algebraic group G, we consider the factorization morphism by the action on G/H of a maximal unipotent subgroup of G. We prove that this morphism is equidimensional if and only if the weight semigroup of G/H satisfies a simple condition. ...

Added: February 25, 2014

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

Springer, 2021

Added: April 14, 2021

Shitov Y., Linear Algebra and its Applications 2017 Vol. 513 P. 120-121

We construct a counterexample to the following conjecture, which was proposed recently by Bapat et al. ‘If a is a regular element in a semigroup S, and x is an outer inverse of a, then a has a reflexive generalized inverse y which dominates x with respect to the minus order on S.’ ...

Added: October 21, 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

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

191574970, Functional Analysis and Its Applications 2006 Vol. 40 No. 2 P. 81-90

It is well known that every module M over the algebra ℒ(X) of operators on a finite-dimensional space X can be represented as the tensor product of X by some vector space E, M ≅ = E ⊗ X. We generalize this assertion to the case of topological modules by proving that if X is a stereotype space with the stereotype approximation property, then for each stereotype module M over the ...

Added: September 23, 2016

Losev A. S., Slizovskiy S., JETP Letters 2010 Vol. 91 P. 620-624

Added: February 27, 2013

Ilyashenko Y., Яковенко С. Ю., М. : МЦНМО, 2013

Предлагаемая книга—первый том двухтомной монографии, посвящённой аналитической теории дифференциальных уравнений.
В первой части этого тома излагается формальная и аналитическая теория нормальных форм и теорема о разрешении особенностей для векторных полей на плоскости.
Вторая часть посвящена алгебраически разрешимым локальным задачам теории аналитических дифференциальных уравнений , квадратичным векторным полям и проблеме локальной классификации ростков векторных полей в комплексной области ...

Added: February 5, 2014

Kalyagin V.A., Koldanov A.P., Koldanov P.A. et al., Physica A: Statistical Mechanics and its Applications 2014 Vol. 413 No. 1 P. 59-70

A general approach to measure statistical uncertainty of different filtration techniques for market network analysis is proposed. Two measures of statistical uncertainty are introduced and discussed. One is based on conditional risk for multiple decision statistical procedures and another one is based on average fraction of errors. It is shown that for some important cases ...

Added: July 19, 2014

Min Namkung, Younghun K., Scientific Reports 2018 Vol. 8 No. 1 P. 16915-1-16915-18

Sequential state discrimination is a strategy for quantum state discrimination of a sender’s quantum
states when N receivers are separately located. In this report, we propose optical designs that can
perform sequential state discrimination of two coherent states. For this purpose, we consider not
only binary phase-shifting-key (BPSK) signals but also general coherent states, with arbitrary prior
probabilities. Since ...

Added: November 16, 2020

Maslov V., Теоретическая и математическая физика 2019 Т. 201 № 1 С. 65-83

We study the process of a nucleon separating from an atomic nucleus from the mathematical standpoint
using experimental values of the binding energy for the nucleus of the given substance. A nucleon becomes
a boson at the instant of separating from a fermionic nucleus. We study the further transformations of
boson and fermion states of separation in a ...

Added: November 1, 2019