Automata as Abstractions

Here, we propose to consider automata directly as abstract systems, and show that the resulting framework is complete. By using non-alternating automata, we can identify a minimal set of concepts needed to create complete abstraction frameworks. Moreover, we show that this proposal serves to clarify a large body of work on abstraction: existing frameworks can be embedded easily into the automation framework, and results in automata theory can be used to give simpler proofs of theorems about abstraction. We expect that, by making this explicit connection, the theory of abstraction can benefit from results in the better-studied field of automata theory.