Заметка об автоматическом решении квадратичных уравнений в словах
Автор: Непейвода Антонина Николаевна
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 2 (37) т.9, 2018 года.
Бесплатный доступ
При анализе программ, оперирующих строками, естественным образом возникает задача решения уравнений в словах. На практике часто встречаются такие уравнения, содержащие, самое большее, два вхождения каждой переменной, –- так называемые квадратичные уравнения. Для их решения Ю. И. Хмелевским в 1971 году предложен интуитивно ясный алгоритм, имеющий экспоненциальную сложность. В 1999 году В. Дьекертом показано, что задача решения квадратичного уравнения является NP-трудной. В данной заметке изложены и показаны на примерах способы упрощения классического алгоритма Хмелевского, позволяющие добиться лучшей его применимости в автоматическом анализе программ.
Суперкомпиляция, уравнения в словах, анализ программ
Короткий адрес: https://sciup.org/143164301
IDR: 143164301 | DOI: 10.25209/2079-3316-2017-9-2-3-21
Список литературы Заметка об автоматическом решении квадратичных уравнений в словах
- А. П. Немытых. Суперкомпилятор SCP4: Общая структура, УРСС, М., 2007.
- N. Bjorner, N. Tillmann, A. Voronkov. "Path feasibility analysis for string-manipulating programs", Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, Lecture Notes in Computer Science, vol. 5505, eds. Kowalewski S., Philippou A., Springer, Berlin. P. 307-321.
- M. T. Trinh, D. H. Chu, J. Jaffar. "Progressive reasoning over recursively-defined strings", Computer Aided Verification, CAV 2016, Lecture Notes in Computer Science, vol. 9779, eds. Chaudhuri S., Farzan A., Springer, 2016. P. 218-240.
- F. Yu, T. Bultan, O. H. Ibarra. "Relational string verification using multi-track automata", Implementation and Application of Automata, CIAA 2010, Lecture Notes in Computer Science, vol. 6482, eds. Domaratzki M., Salomaa K., Springer, 2010. P. 290-299.
- T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett, M. Deters. "An efficient SMT solver for string constraints", Formal Methods in System Design, V. 48. No. 3. 2016. P. 206-234.
- J. Karhumaki, W. Plandowski, F. Mignosi. "The expressibility of languages and relations by word equations", Automata, Languages and Programming, ICALP 1997, Lecture Notes in Computer Science, vol. 1256, eds. Degano P., Gorrieri R., Marchetti-Spaccamela A., Springer, 1997. P. 98-109.
- J. Karhumaki, H. Maurer, G. Paun, G. Rozenberg (eds.). Jewels are forever. Contributions on theoretical computer science in honor of Arto Salomaa, Springer, 1999, 379 p.
- Ю. И. Хмелевский. Уравнения в свободной полугруппе//Тр. МИАН СССР, т. 107, 1971. С. 3-288.
- Г. С. Маканин. Проблема разрешимости уравнений в свободной полугруппе//Матем. сб., 103(145):2(6) 1977. С. 147-236.
- С. А. Романенко. Прогонка для программ на Рефале-4, Препринт № 211, Институт Прикладной Математики им. М. В. Келдыша АН СССР, 1987, 23 с.
- J. Karhumaki. Combinatorics of words.
- M. Huova. Combinatorics of words. New aspects on avoidability, defect effect, equations and palindromes, Ph.D. Thesis, Turku Centre for Computer Science, 2014, 140 p.
- M. H. Sørensen. Turchin's supercompiler revisited, Ms. Thesis, Department of Computer Science, University of Copenhagen, 1994, 143 p.
- A. Jez. "Recompression: a simple and powerful technique for word equations", J. ACM, V. 63. No. 1. (March 2016), 4, 51 p.
- С. М. Абрамов, А. Ю. Орлов. Компиляция в императивные языки синтаксического отождествления языка Рефал//Труды международной конференции "Программные системы: теория и приложения". Т. 1 (ИПС РАН, г. Переславль-Залесский, май 2004), ред. С. М. Абрамов, Физматлит, М., 2004. С. 403-448.
