• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • An Afficient 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
October 14, 2026
At HSE University–St Petersburg, Experts Discuss How AI Changes Tourist Routes and Cultural Heritage
Neural networks are no longer simple travel assistants; now they decide what to include on the route and what to skip. Artificial intelligence changes how people perceive a place and shapes the image of tourist centres. At the II International Scientific and Practical Conference ’Information Technologies in the Preservation and Promotion of Cultural Heritage,’ researchers discussed who controls algorithmic solutions and in what ways, and whether authentic traditions get lost in them.
October 12, 2026
Road Injuries Leading Cause of Death Among Men Aged 10 to 39
Worldwide, road injuries are the leading cause of death among males aged 10–39. An international team of researchers reached this conclusion as part of the Global Burden of Disease Study 2023, analysing data from 204 countries between 1990 and 2023. Their findings have been published in The Lancet Public Health, with HSE University Professor Vasily Vlassov listed among the collaborators.
October 8, 2026
HSE Experts Take Part in 23rd Annual Meeting of Valdai Discussion Club
The 23rd Annual Meeting of the Valdai Discussion Club was held from September 28 to October 1, 2026 under the theme ‘Responsibility for the Future: Limits of the Possible, or Limitless Possibilities?’ The forum brought together 120 experts from 40 countries, including representatives of China, the United States, India, Brazil, the United Kingdom, Germany, Egypt, Iran, and Japan.

 

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 Afficient 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: abstractionsemigroupequivalence checkingprogram analysis

In book

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.
Similar publications
Methodology of Classical Political Economy:Interpretation from 19th Century Russia
Galeev A., / NRU Higher School of Economics. Series WP BRP "Economics/EC". 2024. No. 270/EC/2024.
The paper discusses Yuli Zhukovsky’s 1864 article “Smithian Direction and Positivism in Economics”, one of the first research in methodology of political economy in Russia. Zhukovsky contrasts the abstract theorising of classical economists like Adam Smith and David Ricardo with the empiricism of his contemporaries like Henry Macleod. Zhukovsky advocates for a deductive, universal approach ...
Added: November 2, 2024
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
Transformation of Functional Dataflow Parallel Programs into Imperative Programs
Vasilev V. S., A. I. Legalov, Zykov S. V., Automatic Control and Computer Sciences, Latvia 2022 Vol. 56 No. 7 P. 815–827
The functional dataflow paradigm of parallel programming is focused on the development of parallel portable programs. The source code of functional dataflow programs is translated into a set of graphs reflecting information and control dependences. The main method of their execution is interpretation, which makes it impossible to perform calculations efficiently on real parallel computing systems ...
Added: February 20, 2023
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
«У нас не автоматическая станция»: фильтры технического воображения в поэзии Генриха Сапгира и Игоря Холина
Анна Родионова, Новое литературное обозрение 2022 № 176 С. 254–269
The article analyzes 1950s--1960s poetry of “Lianozovo school” (especially Igor Kholin and Genrikh Sapgir) in connection with the ideology of scientific and technological progress (STP) and its influence on the aesthetic system of XX century Russian literature. This paper examines how the hallmarks of early 20th century literature (which later influenced the Soviet official aesthetics) ...
Added: June 6, 2022
Property-Preserving Transformations of Elementary Net Systems Based on Morphisms
Bernardinello L., Irina Lomazova, Nesterov R. et al., , in: Transactions on Petri Nets and Other Models of Concurrency XVIVol. 13220: Lecture Notes in Computer Science.: Springer, 2022. P. 1–23.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: March 23, 2022
Оптимизация графов потока управления в промежуточных представлениях языка функционально-потокового параллельного программирования
Васильев В. С., Легалов А. И., Научный вестник Новосибирского государственного технического университета 2020 № 4 С. 37–46
Functional dataflow programming languages are intended for the development of architecture-independent parallel programs and support the control of computations based on data availability. Due to the fact that at present parallel computing systems are very widespread, and their programming in imperative languages is associated with portability problems, the development of architecturally independent parallel programming tools ...
Added: August 26, 2021
Трансформация функционально-потоковых параллельных программ в императивные
Васильев В. С., Легалов А. И., Zykov S. V., Моделирование и анализ информационных систем 2021 Т. 28 № 2 С. 198–214
Functional dataflow programming languages are designed to create parallel portable programs. The source code of such programs is translated into a set of graphs that reflect information and control dependencies. The main way of their execution is interpretation, which does not allow to perform calculations efficiently on real parallel computing systems and leads to poor ...
Added: June 12, 2021
Abstraction and Generalization in the Logic of Science: Cases from Nineteenth-Century Scientific Practice
Pietarinen A., Cristalli C., HOPOS 2021 Vol. 11 No. 1 P. 93–121
Abstraction and generalization are two processes of reasoning that have a special role in the construction of scientific theories and models. They have been important parts of the scientific method ever since the nineteenth century. A philosophical and historical analysis of scientific practices shows how abstraction and generalization found their way into the theory of ...
Added: May 29, 2021
Tools and Methods of Program Analysis. 5th International Conference, TMPA 2019, Tbilisi, Georgia, November 7–9, 2019, Revised Selected Papers
Springer, 2021.
Added: April 14, 2021
Алгоритмы синтеза схем-заплаток для решения ресурсо-ориентированной функциональной коррекции схем из функциональных элементов
Высоцкий Л. И., Жуков В. В., Шуплецов М. С., В кн.: Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС-2018)Вып. 1.: М.: ИППМ РАН, 2018. С. 30–37.
При обнаружении ошибок или изменении спецификации проектируемой сверхбольшой интегральной схемы (СБИС) на поздних этапах маршрута проектирования откат на более ранние этапы проектирования и их повторное выполнение очень часто становится непрактичным в силу существенных временных затрат. Для целей сокращения времени проектирования в современные маршруты проектирования интегрируют специальные этапы функциональной коррекции схемы (англ. Engineering Change Order, ECO). В основе указанного подхода лежит анализ уже спроектированной схемы и построение небольшой подсхемы-заплатки, внедрение которой в уже синтезированную ...
Added: November 10, 2020
Property-Preserving Transformations of Elementary Net Systems Based on Morphisms
Bernardinello L., Lomazova I. A., Nesterov R. et al., , in: Proceedings of the International Workshop on Petri Nets and Software Engineering co-located with 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2020)Vol. 2651: CEUR Workshop Proceedings.: CEUR-WS.org, 2020. P. 49–67.
Structural transformations that preserve properties of formal models of concurrent systems make their verification easier. We define structural transformations that allow to abstract and refine elementary net systems. Relations between abstract models and their refinements are formalized using morphisms. Transformations proposed in this paper induce morphisms between elementary net systems as well as preserve their ...
Added: August 12, 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
Communications in Computer and Information Science
Springer, 2018.
This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017. The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as ...
Added: November 12, 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
О минимизации схем программ относительно логико-термальной эквивалентности
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
  • 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