diff --git a/thys/Buchi_Complementation/code/DwyerAC98.ltl b/thys/Buchi_Complementation/code/DwyerAC98.ltl
new file mode 100644
--- /dev/null
+++ b/thys/Buchi_Complementation/code/DwyerAC98.ltl
@@ -0,0 +1,55 @@
+G!a
+G!a | (!b U a)
+G(!a | G!b)
+G(!a | b | G!b | (!c U b))
+G(!a | b | (!c W b))
+Fa
+!a W (!a & b)
+G!a | F(a & Fb)
+G(!a | b | (!b W (!b & c)))
+G(!a | b | (!b U (!b & c)))
+!a W (a W (!a W (a W G!a)))
+G!a | ((!a & !b) U (a | ((!a & b) U (a | ((!a & !b) U (a | ((!a & b) U (a | (!b U a)))))))))
+G!a | (!a U (a & (!b W (b W (!b W (b W G!b))))))
+G(!a | G!b | ((!b & !c) U (b | ((!b & c) U (b | ((!b & !c) U (b | ((!b & c) U (b | (!c U b))))))))))
+G(!a | ((!b & !c) U (c | ((b & !c) U (c | ((!b & !c) U (c | ((b & !c) U (c | (!b W c) | Gb)))))))))
+Ga
+G!a | (b U a)
+G(!a | Gb)
+G(!a | b | G!b | (c U b))
+G(!a | b | (c W b))
+!a W b
+G!a | (!b U (a | c))
+G!a | F(a & (!b W c))
+G(!a | b | G!b | (!c U (b | d)))
+G(!a | b | (!c W (b | d)))
+G(!a | Fb)
+G!a | ((!b | (!a U (!a & c))) U a)
+G(!a | G(!b | Fc))
+G(!a | b | G!b | ((!c | (!b U (!b & d))) U b))
+G(!a | b | ((!c | (!b U (!b & d))) W b))
+G!a | (!a U (!a & b & X(!a U c)))
+G!a | (!b U (a | (!b & c & X(!b U d))))
+G!a | (!a U (!a | G!b | (!b U (!b & c & X(!b U d)))))
+G(!a | G!b | (!c U (b | (!c & d & X(!c U e)))))
+G(!a | G!b | (!b U (c | (!b & d & X(!b U e)))))
+(!a U b) | G(!a | XG!c)
+G!a | ((a | !b | X(a R (a | !c))) U (a | d))
+G!a | (!a U (a & ((!b U c) | G(!b | XG!d))))
+G(!a | G!b | ((b | !c | X(b R (b | !d))) U (b | e)))
+G(!a | ((b | !c | X(b R (b | !d))) U (b | e)) | G(!c | XG!d))
+G(!a | XG!b | XF(b & Fc))
+G!a | ((!b | X(!a U (c & Fd)) | X(a R !c)) U a)
+G(!a | G(!b | XG!c | X(!c U (c & Fd))))
+G(!a | G!b | ((!c | X(!b U (d & Fe)) | X(b R !d)) U b))
+G(!a | ((!b | X(!c U (d & Fe)) | X(c R !d)) U (c | G(!b | X(!c U (d & Fe)) | X(c R !d)))))
+G(!a | F(b & XFc))
+G!a | ((!b | (!a U (!a & c & X(!a U d)))) U a)
+G(!a | G(!b | (c & XFd)))
+G(!a | G!b | ((!c | (!b U (!b & d & X(!b U e)))) U b))
+G(!a | ((!b | (!c U (!c & d & X(!c U e)))) U (c | G(!b | (d & XFe)))))
+G(!a | F(b & !c & X(!c U d)))
+G!a | ((!b | (!a U (!a & c & !d & X((!a & !d) U e)))) U a)
+G(!a | G(!b | (c & !d & X(!d U e))))
+G(!a | G!b | ((!c | (!b U (!b & d & !e & X((!b & !e) U f)))) U b))
+G(!a | ((!b | (!c U (!c & d & !e & X((!c & !e) U f)))) U (c | G(!b | (d & !e & X(!e U f))))))
diff --git a/thys/Buchi_Complementation/code/analysis.py b/thys/Buchi_Complementation/code/analysis.py
new file mode 100755
--- /dev/null
+++ b/thys/Buchi_Complementation/code/analysis.py
@@ -0,0 +1,45 @@
+#!/usr/bin/python
+
+import sys, random, subprocess, time
+
+def read(path):
+	f = open(path, "r")
+	text = f.read()
+	f.close
+	return text
+def write(path, text):
+	f = open(path, "w")
+	f.write(text)
+	f.close()
+
+def stats(entries, finished):
+	entry_count = "{}".format(len(entries))
+	finished_ratio = "{:.2f} \\%".format(100 * len(finished) / len(entries)) if entries else "N/A"
+	finished_time = "{:.3f} s".format(sum(finished) / len(finished)) if finished else "N/A"
+	return "{} & {} & {}".format(entry_count, finished_ratio, finished_time)
+def stats_entries(entries, label, predicate):
+	entries = list(time for (state_count, result, time) in entries if predicate(state_count, result, time))
+	finished = list(float(time) for time in entries if time != "T")
+	print("{} & {}\\\\".format(label, stats(entries, finished)))
+
+if sys.argv[1] == "states":
+	entries = list(line.split() for line in read(sys.argv[2]).splitlines())
+	entries = list((int(state_count_1), int(state_count_2), result, time) for [state_count_1, state_count_2, result, time] in entries)
+	non_timeout = list(time for (state_count_1, state_count_2, result, time) in entries if time != "T")
+	print(all(result == "True" or time == "T" for (state_count_1, state_count_2, result, time) in entries))
+	print("completion rate: {}".format(len(non_timeout) / len(entries)))
+	print("{} {}".format(sum(state_count_1 for (state_count_1, state_count_2, result, time) in entries) / len(entries), sum(state_count_2 for (state_count_1, state_count_2, result, time) in entries) / len(entries)))
+
+if sys.argv[1] == "complement":
+	entries = list(line.split() for line in read(sys.argv[2]).splitlines())
+	entries = list(time for [state_count, time] in entries)
+	non_timeout = list(float(time) for time in entries if time != "T")
+	print(stats(entries, non_timeout))
+if sys.argv[1] == "equivalence":
+	cutoff = 20
+	entries = list(line.split() for line in read(sys.argv[2]).splitlines())
+	entries = list((max(int(state_count_1), int(state_count_2)), result, time) for [state_count_1, state_count_2, result, time] in entries)
+	print(all(result == "True" or time == "T" for (state_count, result, time) in entries))
+	for n in range(1, cutoff + 1): stats_entries(entries, n, lambda state_count, result, time: state_count == n)
+	stats_entries(entries, "> {}".format(cutoff), lambda state_count, result, time: state_count > cutoff)
+	stats_entries(entries, "total", lambda state_count, result, time: True)
diff --git a/thys/Buchi_Complementation/code/benchmark.py b/thys/Buchi_Complementation/code/benchmark.py
--- a/thys/Buchi_Complementation/code/benchmark.py
+++ b/thys/Buchi_Complementation/code/benchmark.py
@@ -1,91 +1,110 @@
 #!/usr/bin/python
 
 import sys, random, subprocess, time
 
 owl = "/home/Projects/owl/build/distributions/owl-minimized-20.XX-development/bin/owl"
 
 def read(path):
 	f = open(path, "r")
 	text = f.read()
 	f.close
 	return text
 def write(path, text):
 	f = open(path, "w")
 	f.write(text)
 	f.close()
 
 def get_state_count(path):
 	result = subprocess.run(["autfilt", path, "--stats=%s"], stdout = subprocess.PIPE, text = True)
 	return int(result.stdout.strip())
 
 def spot_generate_automaton(state_count, proposition_count):
 	seed = random.randrange(0x10000)
 	result = subprocess.run(["randaut", "--seed={}".format(seed), "--ba", "--states={}".format(state_count), str(proposition_count)], stdout = subprocess.PIPE, text = True)
 	return result.stdout
 def spot_generate_formula(proposition_count):
 	seed = random.randrange(0x10000)
 	result = subprocess.run(["randltl", "--seed={}".format(seed), str(proposition_count)], stdout = subprocess.PIPE, text = True)
 	return result.stdout.strip()
 
 def spot_simplify_automaton(path):
 	result = subprocess.run(["autfilt", "--ba", "--small", path], stdout = subprocess.PIPE, text = True)
 	return result.stdout
 def owl_simplify_automaton(path):
 	result = subprocess.run(["owl", "-I", path, "---", "hoa", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True)
 	return result.stdout
 
+def spot_to_buchi_automaton(path):
+	result = subprocess.run(["autfilt", "--ba", "--small", path], stdout = subprocess.PIPE, text = True, timeout = 60)
+	return result.stdout
+
 def spot_formula_to_nba(formula):
 	result = subprocess.run(["ltl2tgba", "--ba", formula], stdout = subprocess.PIPE, text = True)
 	return result.stdout
 def owl_formula_to_nba(formula):
 	result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2nba", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True)
 	return result.stdout
+def owl_formula_to_nba_opt(formula):
+	result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2nba", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True)
+	return result.stdout
 def owl_formula_to_dra(formula):
 	result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2dra", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True)
 	return result.stdout
+def owl_formula_to_dra_opt(formula):
+	result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2dra", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True)
+	return result.stdout
 
 def bc_complement(path1, path2):
-	subprocess.run(["./Autool", "complement_quick", path1, path2], timeout = 10)
+	subprocess.run(["./Autool", "complement_quick", path1, path2], timeout = 60)
 def bc_equivalence(path1, path2):
-	result = subprocess.run(["./Autool", "equivalence", path1, path2], timeout = 10, stdout = subprocess.PIPE, text = True)
+	result = subprocess.run(["./Autool", "equivalence", path1, path2], timeout = 60, stdout = subprocess.PIPE, text = True)
 	return result.stdout.strip() == "true"
 
 def complement(path_input, path_output):
 	start = time.time()
 	try: bc_complement(path_input, path_output)
 	except subprocess.TimeoutExpired: duration = "T"
 	else: duration = str(time.time() - start)
 	print("{} {}".format(get_state_count(path_input), duration))
 def equivalence(path_1, path_2):
 	start = time.time()
 	try: eq = bc_equivalence(path_1, path_2)
 	except subprocess.TimeoutExpired: eq = None; duration = "T"
 	else: duration = str(time.time() - start)
 	print("{} {} {} {}".format(get_state_count(path_1), get_state_count(path_2), eq, duration))
+	return eq
 
 if sys.argv[1] == "complement_automaton":
 	while True:
 		write("a.hoa", spot_generate_automaton(20, 4))
 		complement("a.hoa", "c.txt")
 if sys.argv[1] == "complement_formula":
 	while True:
 		write("a.hoa", spot_formula_to_nba(spot_generate_formula(4)))
 		complement("a.hoa", "c.txt")
 if sys.argv[1] == "equivalence_random":
 	while True:
 		write("a.hoa", spot_generate_automaton(100, 4))
 		write("b.hoa", spot_generate_automaton(100, 4))
 		equivalence("a.hoa", "b.hoa")
 if sys.argv[1] == "equivalence_simplify":
 	while True:
-		write("a.hoa", spot_generate_automaton(20, 4))
+		write("a.hoa", spot_generate_automaton(10, 4))
 		write("b.hoa", spot_simplify_automaton("a.hoa"))
 		equivalence("a.hoa", "b.hoa")
 if sys.argv[1] == "equivalence_translate":
 	while True:
 		formula = spot_generate_formula(4)
-		print(formula)
 		write("a.hoa", spot_formula_to_nba(formula))
-		write("b.hoa", owl_formula_to_nba(formula))
-		if not read("b.hoa"): continue
-		equivalence("a.hoa", "b.hoa")
+		write("b.hoa", owl_formula_to_dra_opt(formula))
+		write("c.hoa", spot_simplify_automaton("b.hoa"))
+		if equivalence("a.hoa", "c.hoa") == False: print(formula)
+if sys.argv[1] == "equivalence_translate_collection":
+	for formula in read(sys.argv[2]).splitlines():
+		print(formula)
+		try:
+			write("a.hoa", spot_formula_to_nba(formula))
+			write("b.hoa", owl_formula_to_dra_opt(formula))
+			write("c.hoa", spot_to_buchi_automaton("b.hoa"))
+			equivalence("a.hoa", "c.hoa")
+		except subprocess.TimeoutExpired: print("T")