Artur Jeż(University of Wrocław)
hosted by seminar series "Certified Verification with Applications"
"Recompression-based algorithm for word equations"
In this talk I will present the currently ``best in theory'' algorithm for solvingsystems of equations of the form u = v, where both u, v are words of letters and variablesand a solution assigns to each variable a word so that those formal equalities are turnedinto true equalities of words.The algorithm is based on simple compression rules, which replace pairs of different lettersab by a fresh letter c or by replacing maximal substring of the form a^\ell by new symbols a_\ell.In order to make this approach sound and complete, rules replacing a variable X by aX or Xa are also applied.The crucial and surprisingly simple part of the analysis shows that with appropriate choice of subwords to be replaced,the kept equation is of linear length, which shows that the whole algorithm is in PSPACE.In the second part I will discuss some advantages of the algorithm (simplicity, robustness and ease of generalizations)possible extensions (regular constraints, involution, terms)as well is downfalls (practicality, heavy use of nondeterminism, bottom-up approach).
Bio: Artur Jeż graduated mathematics and computer science at the University of Wrocław in 2006. He pursued his PhD at the same University under the supervision of Krzysztof Loryś and Alexander Okhotin. He completed his PhD thesis on connections between Conjunctive Grammars and Equations over Sets of Natural Numbers in 2010. He was employed as assistant professor at the University of Wrocław in 2010–2012 and then he was a postdoc at Max Planck Institute for Computer Science (Saarbruecken, Germany) in 2012–14, most of the time as a Humboldt Foundation fellow. Afterwards he returned to Wrocław, in 2015 he received habilitation and since 2018 he is an associate professor. In recent years Artur Jeż is mostly interested in grammar compression and its connections to word equations and similar topics.
|Time:||Thursday, 02.12.2021, 13:00|