@Article{ayari.ea:decision:2003,
  title         = {Decision Procedures for Inductive Boolean Functions based
                  on Alternating Automata},
  author        = {Abdelwaheb Ayari and David Basin and Felix Klaedtke},
  journal       = {Theoretical Computer Science},
  volume =       "300",
  number =       "1--3", 
  pages =        "301--329",
  month =        "May",
  year          = 2003,
  abstract      = {We show how alternating automata provide decision
                  procedures for the equivalence of inductively defined
                  Boolean functions that are useful for reasoning about
                  parameterized families of circuits. We use alternating word
                  automata to formalize families of linearly structured
                  circuits and alternating tree automata to formalize
                  families of tree structured circuits. We provide complexity
                  bounds and show how our decision procedures can be
                  implemented using BDDs. In comparison to previous work, our
                  approach is simpler, yields better complexity bounds, and,
                  in the case of tree structured families, is more general.}
}