Automata Minimization Techniques and Applications

Minimization of Symbolic Automata Presented By: Loris D Antoni Joint work with: Margus Veanes 01/24/14, POPL14

What is automata minimization? 2

Deterministic Finite Automaton A = (Q,q0,F, , ) a b a q q0 b 3

Automata Minimization Minimization = find and collapse equivalent states s Non final p distinguishable s Final q 4

a a 2 5 5 1 a b b a,b a,b 0 b a a 3 4 6 6 b b a,b a,b a,b a,b 0 1,3 2,4 6 5,6

A simple Application: Random Password generation Given constraints: Length is k: "^.{5,20}$" Contains 2 capital letters: "[A-Z].*[A-Z]" Contains a digit: "\d Generate random instances with uniform distribution that match all the above conditions. 6

Key idea ^.{5,20}$ [A-Z].*[A-Z] \d 7

Problems Minimization Big automaton Big alphabet 216 characters in UTF16 Symbolic Automata 8

Symbolic Finite Automaton (SFA) A = (Q,q0,F, , ) Input sort: in this case int x. x mod 2=1 x. x mod 2=0 x. x mod 2=0 q q0 x. x mod 2=1 Separate theory for the input alphabet SMT SOLVER 9

Symbolic Finite Automata (SFA) x. x mod 2=1 x. x mod 2 =0 x. x mod 2=0 Execution p q Example x. x mod 2=1 1 2 5 3 p p q p p p is final accept the input 10

Advantages of Symbolic Automata Alphabet is represented symbolically UTF16 abstracted using BDDs Integer using predicates over integers Succinctness at most n2 transitions One transition captures many symbols BUT: do DFA algorithms generalize to SFAs? 11

An example: SFA intersection REQUIREMENTS: Input theory must be a Boolean algebra, and decidable 1 A1: p1 q1 1 2 X X A1 A2: p1 p2 q1 q2 2 A2: p2 q2 delete when 1 2 unsatisfiable 12

Moores algorithm s a p p distinguishable distinguishable a s q q n2 iterations over k symbols O(kn2) 13

Symbolic Moores algorithm p p satisfiable distinguishable distinguishable q q Initially D = F x (Q\F) U (Q\F) x F for each (p ,q ) in D, (p,q) not in D let , guards of (p,p ), (q,q ) m transitions O(m2 f(k)) k = size of biggest predicate in SFA if(isSat( )) add (p,q) to D 14

Sometimes Moore is Less From: Rani Abdellatif Sent: Tuesday, November 13, 2012 12:55 PM To: Margus Veanes Cc: Patrick McFalls Subject: RE: Password generation help Margus, I tested the perf of the sample you sent me with password lengths from 8 to 15 chars and here are the results: Chars Time ms 8 171 9 406 10 1061 11 2044 12 3698 13 6271 14 11591 15 18362 18 sec for 15 characters! the culprit should scale up to 128 characters! This time is the time it takes to run sfa.Determinize(rex.Solver).Minimize(rex.Solver). The time required to create the SFA or generate samples once it s created is quite small in comparison. We are expecting 15 characters to be on the shorter end of password we ll generate, going up to 128 characters. 15

Hopcrofts algorithm: intuition Q\F F 16

Hopcrofts algorithm: intuition S A R a a a 17

Hopcrofts algorithm: intuition R b P1 P2 P4 b P3 Keep partitioning with respect to W for every input symbol 18

Hopcrofts algorithm: intuition Let s assume I already split according to R R P1 P2 19

Hopcrofts algorithm: intuition Let s assume I already split according to R Q R P1 P2 Do I need to consider both P1 and for P2 future splitting? 20

Hopcrofts algorithm: intuition Let s assume I already split according to R a Q R P1 a a P2 Do I need to consider both P1 and for P2 future splitting? 21

Hopcrofts algorithm: intuition Let s assume I already split according to R a a Q R P1 a P2 Do I need to consider both P1 and for P2 future splitting? 22

Hopcrofts algorithm: intuition Let s assume I already split according to R a Q R P1 a a P2 Do I need to consider both P1 and for P2 future splitting? NO I ONLY NEED ONE! 23

Hopcrofts algorithm P := {F, Q\F} W := {if |F|< |Q\F| then F else Q\F} while return while W != { } R:=pickFrom(W) foreach log niterations O(kn log n) foreach a in S := -1(R,a) while while T P. T S {} T \S {} P,W := split(P, P S , P\S) return partitioned DFA 24

Hopcrofts algorithm example P2 P1 R a a 2 5 5 1 a b b a,b a,b 0 b a a 3 4 6 6 b b PARTITION: {P1, P2} TO ANALYZE: {P2}

Hopcrofts algorithm example P11 P12 P2 R a a 2 5 5 1 a b b a,b a,b 0 b a a 3 4 6 6 b b PARTITION: {P11, P12, P2} TO ANALYZE: {P2, P12}

Hopcrofts algorithm example P11 P12 P2 R a a 2 5 5 1 a b b a,b a,b 0 b a a 3 4 6 6 b b PARTITION: {P11, P12, P2} TO ANALYZE: {P12}

Hopcrofts algorithm example a a 2 5 5 1 a b b a,b a,b 0 b a a 3 4 6 6 b b a,b a,b a,b a,b 0 1,3 2,4 6 5,6

Symbolic Hopcrofts algorithm P := {F, Q\F} W := {if |F|< |Q\F| then F else Q\F} while return while W != { } R:=pickFrom(W) foreach foreach a in Alphabet might not be finite S := -1(R,a) while while T P. T S {} T \S {} P,W := split(P, P S , P\S) return partitioned DFA 29

Finitize the alphabet 1 2 1 2 5 8 4 '3 6 Predicates: 7 3 {x>5, x<10, x=3} Minterms: {x=3, x 5, 5<x<10, x 10} 30

Symbolic Hopcrofts algorithm P := {F, Q\F} W := {if |F|< |Q\F| then F else Q\F} while return while W {} R:=pickFrom(W) foreach log niterations O(2mnlog n+2mf(mk)) foreach in Minterms(A) S := -1(R, ) while return partitioned DFA while T P. T S {} T \S {} P,W := split(P, P S , P\S) We need something better 31

New Algorithm: Intuition R A P1 p P2 q \ What if ? 32

Example 1/2 Q\F R F -2<x<5 -5<x<3 2 5 5 1 x<0 true true 0 x 0 -2<x<5 -5<x<3 3 4 6 6 false -5<x<3

Example 1/2 R -2<x<5 -5<x<3 2 5 5 1 x<0 true true 0 x 0 -2<x<5 -5<x<3 3 4 6 6

Example 2/2 x 2 R x<2 x 5 r 5 p 6 q true x<5 Both p and q go to r, but x 2 x 5 ?? NO Then p is distinguishable from q

Example 2/2 x 2 R x<2 x 5 r 5 p 6 q true x<5 Both p and q go to r, but x 2 x 5 ?? NO Then p is distinguishable from q

New Algorithm P := {F, Q\F} W := {if |F|< |Q\F| then F else Q\F} while return while W { } log niterations O(n2log n f(nk)) R := pickFrom(W); S := -1(R, true); while P,W := split(P, P S , P\S, witness( -1(p1) -1(p2)) return partitioned DFA while A P. A S {} p1,p2. -1(p1) -1(p2) 37

Experiments 1. Randomly generated DFAs SFAs using BDDs (sort = bitvec 7 bits) 2. SFAs generated from regexes SFAs using BDDs (sort = bitvec 16 bits) 3. A corner case of Minterm generation SFAs using BDDs (sort = bitvec 20 bits) 4. Randomly generated SFAs over string x int SFAs over using Z3 (sort = string x int) 5. Monadic second order logic to DFA transformation SFAs using BDDs (sort = bitvec 40 bits)

1) Randomly generated DFAs 5 billion DFAs: 10 to 100 states, 2 to 50 symbols From [Almeida, Moreira, Reis, TR05]

2) SFAs generated from regexes (regexplib.com) 3000 regexes over UTF16 alphabet (216 elems) From [regexplib.com] Both axis logscale More States => Moore Worse

3) A corner case of Minterm generation This SFA has 2k minterms!! Logscale brics.automata.dk Uses intervals instead of BDDs

4) Randomly generated SFAs over string x int Randomly generated 10 SFAs over string x int and minimized all the intersections, complement, difference, and union of such SFAs Random generation causes many predicate overlaps minterms

5) MSO logic to DFA transformation [IJFCS05] State of the art for MSO

Conclusion Results Adapted classical minimization algorithm to the symbolic setting New minimization algorithm for symbolic automata (faster than previous ones) Future work Extend to tree automata Extend classical automata problems to SFAs Edit distance? Regex for symbolic automata? 44