diff --git a/src/regexp.rs b/src/regexp.rs
--- a/src/regexp.rs
+++ b/src/regexp.rs
@@ -201,6 +201,33 @@ impl RegexpDFA {
 		return RegexpDFA{rules, end_states, alphabet_index: self.alphabet_index.clone()};
 	}
 
+	pub fn find_distinguishing_string(&self, other: &RegexpDFA) -> Option<String> {
+		if self.rules == other.rules && self.end_states == other.end_states {
+			return None;
+		}
+
+		let product = self.build_product_automaton(other);
+		let n = product.alphabet_index.len();
+		let reverse_alphabet_index: HashMap<usize, char> = HashMap::from_iter(product.alphabet_index.iter().map(|(&k, &v)| (v, k)));
+
+		let mut queue = VecDeque::from([(0, "".to_string())]);
+		let mut visited = HashSet::new();
+		while !queue.is_empty() {
+			let (state, acc) = queue.pop_front().unwrap();
+			if product.end_states.contains(&state) {
+				return Some(acc);
+			}
+			for (i, target) in product.rules[state*n..(state+1)*n].iter().enumerate() {
+				if !visited.contains(target) {
+					queue.push_back((*target, acc.clone()+&String::from(reverse_alphabet_index[&i])));
+					visited.insert(target);
+				}
+			}
+		}
+
+		panic!();
+	}
+
 	fn find_equivalent_states(&self) -> Vec<(usize, usize)> {
 		let n = self.alphabet_index.len();
 		let state_vec: Vec<usize> = (0..self.rules.len()/n).collect();
@@ -256,4 +283,26 @@ impl RegexpDFA {
 
 		return RegexpDFA{rules, end_states, alphabet_index: self.alphabet_index.clone()};
 	}
+
+	fn build_product_automaton(&self, other: &RegexpDFA) -> RegexpDFA {
+		let n = self.alphabet_index.len();
+		let m = other.rules.len() / n;
+		let k = self.rules.len() / n;
+
+		let mut rules = vec![];
+		let mut end_states = HashSet::new();
+
+		for s1 in 0..k {
+			let row1 = &self.rules[s1*n..(s1+1)*n];
+			for s2 in 0..m {
+				let row2 = &other.rules[s2*n..(s2+1)*n];
+				rules.extend(row1.iter().zip(row2.iter()).map(|(x, y)| x*m + y));
+				if (self.end_states.contains(&s1)) ^ (other.end_states.contains(&s2)) {
+					end_states.insert(s1*m + s2);
+				}
+			}
+		}
+
+		return RegexpDFA{rules, end_states, alphabet_index: self.alphabet_index.clone()}.reduce().normalize();
+	}
 }