Эффективные алгоритмы проверки эквивалентности пропозициональных программ Мили на уравновешенных шкалах | Прикладная дискретная математика. 2025. № 70. DOI: 10.17223/20710410/70/5

Предлагается и рассматривается модель программ, называемая далее моделью пропозициональных программ Мили (ППМ) и представляющая собой небольшое синтаксическое обобщение модели дискретных преобразователей Глушкова - Летичевского с «осовремененной» семантикой, основанной на понятиях, использующихся в модели пропозициональных последовательных программ, введённой В. А. Захаровым (ПППЗ). Предлагается подход к построению эффективных алгоритмов проверки эквивалентности ППМ, являющийся адаптацией известного подхода к проверке эквивалентности ПППЗ, основанного на анализе графа совместных вычислений программ. Демонстрируется применение этого подхода для получения эффективных алгоритмов проверки эквивалентности ППМ для некоторых видов семантик прикладного характера.
  • Title Эффективные алгоритмы проверки эквивалентности пропозициональных программ Мили на уравновешенных шкалах
  • Headline Эффективные алгоритмы проверки эквивалентности пропозициональных программ Мили на уравновешенных шкалах
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 70
  • Date:
  • DOI 10.17223/20710410/70/5
Ключевые слова
проблема эквивалентности, проверка эквивалентности, модели программ, дискретные преобразователи, пропозициональные последовательные программы
Авторы
Ссылки
Rice Н. G. Classes of recursively enumerable sets and their decision problems // Trans. AMS. 1953. V. 74. P. 358-366.
Клини С. К. Введение в метаматематику. M.: ИЛ, 1957.
Глушков В. М., Летичевский А. А. Теория дискретных преобразователей // Избранные вопросы алгебры и логики. Новосибирск: Наука, Сибирское отделение, 1973. С. 5-39.
Захаров В. А. Быстрые алгоритмы разрешения эквивалентности операторнвіх программ на уравновешеннвіх шкалах // Ма гем. вопр. кибернетики. 1998. Вып.7. С. 303-324.
Летичевский А. А. Функционалвная эквивалентности дискретных преобразователей III // Кибернетика. 1972. №1. С. 1-4.
Летичевский А. А., Смикун Л. Б. Об одном классе групп с разрешимой проблемой эквивалентности // Докл. АН СССР. 1976. Т. 227. №1. С. 36-38.
Захаров В. А., Подымов В. В. Применение алгоритмов проверки эквивалентности для оптимизации программ // Трѵдві ИСП РАН. 2015. Т. 27. Вып.4. С. 145-174.
Zakharov V. А. An efficient and unified approach to the decidability of equivalence of propositional programs // LNCS. 1998. V. 1443. P.247-258.
Захаров В. А. Быстрые алгоритмы разрешения эквивалентности иропозиционалвных операторных программ на упорядоченных полугрупповых шкалах // Вести. Моек, ун-та. Сер. 15. Вычислителвная математика и кибернетика. 1999. №3. С. 29-35.
Захаров В. А. О проблеме эквивалентности операторных программ на уравновешенных однородных обратимых шкалах // Матем. вопр. кибернетики. 2001. Вып. 10. С. 155-166.
Zakharov V. A. The equivalence problem for computational models: Decidable and undecidable cases // LNCS. 2001. V.2055. P. 133-152.
Zakharyaschev I. M. and Zakharov V. A. On the equivalence-checking problem for polysemantic models of sequential programs // Труды ИСП РАН. 2004. T. 6. С. 179-198.
Podlovchenko R. I., Rusakov D. M., and Zakharov V. A. The equivalence problem for programs with mode switching is PSPACE-complete // Труды ИСП РАН. 2006. T. 11. С. 109-128.
Щербина В. Л., Захаров В. А. Эффективные алгоритмы проверки эквивалентности программ в моделях, связанных с обработкой прерываний // Вести. Моек, ун-та. Сер. 15. Вычислителвная математика и кибернетика. 2008. №2. С. 33-41.
Подловченко Р. И., Кузюрин Н. Н., Щербина В. Л., Захаров В. А. Исполвзование алгебраических моделей программ для обнаружения метаморфного вредоносного кода // Фундамент. и прикл. матем. 2009. Т. 15. №5. С. 181-198.
Zakharov V.A. Program equivalence checking by two-tape automata // Cybernetics and Systems Analysis. 2010. V. 46. No. 4. P. 554-562. '.
Подымов В. В., Захаров В. А. О двухленточных машинах, описывающих полугруппы с сокращением // Проблемы теоретической кибернетики. Материалы XVI Междунар. конф. (Нижний Новгород, 20-25 июня 2011 г.). Н. Новгород: Изд-во Нижегор. ун-та, 2011. С. 372-375.
Захаров В. А. Модели и алгоритмы в задаче проверки эквивалентности программ // Материалы XI Междунар. семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О. Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), М.: Изд-во механико-математического факулвтета МГУ, 2012. С. 53-62.
Подловченко Р. И., Захаров В. А. О двух методах распознавания эквивалентности в алгебраических моделях программ // Интеллектуальные системы. 2013. Т. 17. Vs 1-4. С.366-370.
Подымов В. В., Захаров В. А. Полиномиальный алгоритм проверки эквивалентности в модели программ с перестановочными и подавляемыми операторами // Труды ИСП РАН. 2014. Т. 26. Вып. 3. С. 145-166.
Подымов В. В. Улучшение алгоритмов проверки эквивалентности операторных программ при помощи анализа весов вершин // Ломоносовские чтения-2021. Секция Вычислительной математики и кибернетики. М.: Изд-во Моек, ун-та, 2021. С. 124-125.
Карпов Ю.Г. Теория автоматов. СПб.: Питер, 2003.
Zakharov V. A. and Zakharyaschev I. М. On the equivalence checking problem for a model of programs related with muti-tape automata // LNCS. 2005. V. 3317. P.293-305.
Пентус A. E., Пентус M. P. Теория формальных языков: учеб, пособие. М.: Изд-во ЦПИ при механико-математическом факультете МГУ, 2004.
Гаврилов Г. П., Сапоженко А. А. Задачи и упражнения по дискретной математике: учеб, пособие. 3-е изд., перераб. М.: Физматлит, 2005.
Зорич В. А. Математический анализ. Ч.І. 4-е изд., испр. М.: МЦНМО, 2002.
Кормен Т., Лейзерсон Ч., Pueecm Р., Штайн К. Алгоритмы: построение и анализ. 3-е изд. М.: ООО «И. Д. Вильямс», 2013.
Лаллеман Ж. Полугруппы и комбинаторные приложения. М.: Мир, 1985.
Клиффорд А., Престон Г. Алгебраическая теория полугрупп. Т. 1. М.: Мир, 1972.
Страуструп Б. Язык программирования C++. Краткий курс. 2-е изд. СПб.: ООО «Диалектика», 2019.
Захаров В. А. Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ // Матем. вопр. кибернетики. 1999. Т. 8. С. 255-273.
Захаров В. А. Об эквивалентности потоковых программ // Материалы XI Междунар. семинара «Дискретная математика и ее приложения», посвященного 80-летию со дня рождения академика О. Б. Лупанова (Москва, МГУ, 18-23 июня 2012 г.), М.: Изд-во механико-математического факультета МГУ, 2012. С. 119-122.
Подымов В. В. Алгоритм проверки эквивалентности линейных унарных рекурсивных программ на упорядоченных полугрупповых шкалах // Вести. Моек, ун-та. Сер. 15. Вычислительная математика и кибернетика. 2012. №4. С. 37-43.
Захаров В. А. Об эквивалентности ограниченно недетерминированных автоматов-преобразователей над полугруппами // Проблемы теоретической кибернетики. Материалы XVII Междунар. конф. (Казань, 16-20 июня 2014 г.). Казань: Отечество, 2014. С. 100-102.
Захаров В. А. Моделирование и анализ поведения последовательных реагирующих программ // Труды ПСП ГАН. 2015. Т. 27. №2. С. 221-250.
Подымов В. В. Алгоритмы проверки эквивалентности программ с процедурами в прогрессивных полугрупповых перегородчатых моделях // Вести. Моек, ун-та. Сер. 15. Вычислительная математика и кибернетика. 2019. №4. С. 37-44.
Подымов В. В. О сложности проверки эквивалентности линейных унарных рекурсивных программ над уравновешенными полугруппами // Ломоносовские чтения-2024. Секция Вычислительной математики и кибернетики. М.: МАКС Пресс, 2024. С. 53-55.
Котов В. Е., Сабелъфелъд В. К. Теория схем программ. М.: Наука, 1991.
 Эффективные алгоритмы проверки эквивалентности пропозициональных программ Мили на уравновешенных шкалах | Прикладная дискретная математика. 2025. № 70. DOI: 10.17223/20710410/70/5
Эффективные алгоритмы проверки эквивалентности пропозициональных программ Мили на уравновешенных шкалах | Прикладная дискретная математика. 2025. № 70. DOI: 10.17223/20710410/70/5