Decision procedures for inductive Boolean functions based on alternating automata

We show how alternating automata provide decision procedures for the equality of inductively defined Boolean functions and present applications to 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 for deciding the equality of function (or circuit) families and show how our decision procedures can be implemented using BDDs. In comparison to previous work, our approach is simpler, has better complexity bounds, and, in the case of tree-structured families, is more general.

Authors

• Abdelwaheb Ayari
• David Basin
• Felix Klaedtke

Keywords

• Alternating automaton
• Inductive Boolean function
• Verification
• Parameterized circuit