--- a/ChengsongTanPhdThesis/Chapters/RelatedWork.tex	Tue Nov 08 23:24:54 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/RelatedWork.tex	Fri Nov 11 00:23:53 2022 +0000
@@ -49,3 +49,30 @@
 for regexes, attack string that exploit the worst-time 
 scenario, and "attack automata" that generates
 attack strings.
+
+
+
+
+
+
+Thanks to our theorem-prover-friendly approach,
+we believe that 
+this finiteness bound can be improved to a bound
+linear to input and
+cubic to the regular expression size using a technique by
+Antimirov\cite{Antimirov95}.
+Once formalised, this would be a guarantee for the absence of all super-linear behavious.
+We are working out the
+details.
+
+ 
+To our best knowledge, no lexing libraries using Brzozowski derivatives
+have similar complexity-related bounds, 
+and claims about running time are usually speculative and backed by empirical
+evidence on a few test cases.
+If a matching or lexing algorithm
+does not come with certain basic complexity related 
+guarantees (for examaple the internal data structure size
+does not grow indefinitely), 
+then they cannot claim with confidence having solved the problem
+of catastrophic backtracking.