• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • An efficient equivalence-checking algorithm for a model of programs with commutative and absorptive statements
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
August 13, 2026
‘Working with AI Solves a Wide Range of Engineering Problems
Artificial intelligence is a working tool based on a balanced combination of algorithms and engineering. Experts and doctoral students from the HSE Moscow Institute of Electronics and Mathematics explain how AI technologies can improve an application, device, or system, and what engineering tasks are solved in the process.
August 12, 2026
‘I Would Like My Research to Help Make the World a Calmer and Better Place
Whatever task Saraa Ali, Junior Research Fellow at the Laboratory of Methods for Big Data Analysis (LAMBDA) of the AI and Digital Science Institute (HSE Faculty of Computer Science), is working on, she thinks about how it can benefit people. She told the Young Scientists of HSE University project about her large family, diagnosing three-phase motors, and her dream of building a children’s home in her native country.
August 11, 2026
‘The Peak of Stupidity and ‘The Valley of Despair: HSE Economists Propose an Explanation for the Dunning–Kruger Effect
The Dunning–Kruger effect, which describes a sharp surge in self-confidence among beginners followed by an equally rapid decline as they gain experience, can be explained by the nature of the learning process and the acquisition of new knowledge. This conclusion was reached by Andrey Vorchik of the HSE Faculty of Economic Sciences together with independent researcher Murat Mamyshev. They developed a mathematical model of learning and demonstrated how subjective confidence is formed and changes as knowledge accumulates, as well as how teachers can reduce the ‘valley of despair’ experienced by learners.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

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
Keywords: semigroupprogramequivalence checking
Publication based on the results of:
­­­Information system processes modeling, analysis and enhancement (2015)

In book

Concurrency, Specification & Programming. 24th International Workshop, CS&P 2015. Rzeszow, Poland, September 28-30, 2015. Proceedings
Vol. 2. , University of Rzeszow, 2015.
Similar publications
Sensitivity and Chaoticity of Some Classes of Semigroup Actions
Zhukova N., Regular and Chaotic Dynamics 2024 Vol. 29 No. 1 P. 174–189
The focus of the work is the investigation of chaos and closely related dynamic properties of continuous actions of almost open semigroups and $C$-semigroups. The class of dynamical systems $(S, X)$ defined such semigroups $S$ is denoted by $\frak A.$ These semigroups contain, in particular, cascades, semiflows and groups of homeomorphisms. We extend the Devaney ...
Added: February 11, 2024
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
Invariant measures of torus piecewise isometries
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
THE PHENOMENON OF CLASSICAL MUSIC RADIO IN THE CONTEXT OF GLOBAL RADIO INDUSTRY ISSUES
Герасимова И. А., Цветковская Т. А., 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
Алгоритмы синтеза схем-заплаток для решения ресурсо-ориентированной функциональной коррекции схем из функциональных элементов
Высоцкий Л. И., Жуков В. В., Шуплецов М. С., В кн.: Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС-2018)Вып. 1.: М.: ИППМ РАН, 2018. С. 30–37.
При обнаружении ошибок или изменении спецификации проектируемой сверхбольшой интегральной схемы (СБИС) на поздних этапах маршрута проектирования откат на более ранние этапы проектирования и их повторное выполнение очень часто становится непрактичным в силу существенных временных затрат. Для целей сокращения времени проектирования в современные маршруты проектирования интегрируют специальные этапы функциональной коррекции схемы (англ. Engineering Change Order, ECO). В основе указанного подхода лежит анализ уже спроектированной схемы и построение небольшой подсхемы-заплатки, внедрение которой в уже синтезированную ...
Added: November 10, 2020
Технологии разработки объектно-ориентированных программ на языке С++. Часть 1. Основы структурного программирования на алгоритмическом языке С++
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., Жайлауова Ш. Р., В кн.: Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019).: М.: Изд-во механико-математического факультета МГУ, 2019. С. 272–274.
В данной статье мы продолжаем поиск и исследование новых классов недетерминированных автоматов-преобразователей с разрешимой проблемой эквивалентности. Цель исследования~--- провести как можно более точную и подробную демаркацию границы между разрешимыми и неразрешимыми случаями проблемы эквивалентности для рассматриваемой модели вычислений. Мы рассматриваем один класс недетерминированных автоматов, работающих над выходным алфавитом из одной буквы. Характерная особенность рассматриваемых автоматов-преобразователей ...
Added: October 17, 2019
Recurrence for free semigroups of maps
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
Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018
Yaroslavl: Ярославский государственный университет им. П.Г. Демидова, 2018.
Workshop on Program Semantics, Specification and Verification: Theory and Applications is the leading event in Russia in the field of applying of the formal methods to software analysis. Proceedings of the ninth workshop dedicated to formalisms for program semantics, formal models and verification, programming and specification languages, algebraic and logical aspects of programming. ...
Added: October 26, 2018
Полиномиальный алгоритм проверки эквивалентности детерминированных двухленточных автоматов
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
Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science
Cham: Springer, 2017.
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 ...
Added: January 24, 2018
On the Minimization Problem for Sequential Programs
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
Анализ программных продуктов оценки эффективности государственных закупок
Кравцова М. В., Наука и бизнес: пути развития 2016 № 12(66) С. 138–141
The article considers the basic program products designed for the customer in work with state procurement. There is conducted a comparative analysis of the program and revealed its advantages and disadvantages. The author develops and proposes his own program for state procurement efficiency assessment. ...
Added: November 27, 2017
О минимизации схем программ относительно логико-термальной эквивалентности
Zakharov V., Жайлауова Ш. Р., В кн.: Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.).: М.: МГУ, МАКС Пресс, 2017. С. 84–87.
Эффективная разрешимость проблемы л-т эквивалентности дает возможность приступить к решению задачи минимизации - построения схемы программ наименьшего размера, л-т эквивалентной заданной схеме. Чтобы отыскать ее решение, заметим, что модель вычислений стандартных схем программ сходна модели вычислений автоматов-преобразователей, работающих над полугруппами. Ранее был предложен метод минимизации автоматов-преобра\-зо\-вателей, работающих над упорядоченными левосократимыми полугруппами. В данной заметке мы ...
Added: October 22, 2017
Rational Dyck Paths in the Non Relatively Prime Case
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
О задаче минимизации последовательных программ
Zakharov V., Жайлауова Ш. Р., Моделирование и анализ информационных систем 2017 Т. 24 № 4 С. 415–433
rst-order program schemata is one of the simplest models of sequential imperative programs intended for solving veri cation 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
Выявление и преодоление педагогических рисков в процессе модернизации системы образования Московской области
Шевелёва Н. Н., Ножичкина Л. В., АСОУ, 2017.
The collection presents anti-risk programs of general education organizations of the Moscow region. The risks and ways to minimize them are presented in the context of modernization of education. ...
Added: August 27, 2017
A counterexample on outer inverses in semigroups
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
On the Minimization of Finite State Transducers over Semigroups
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
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit