Hi Johan:

please develop an example that shows how AC
can be used to check that an automaton superimposed
on the system by the AC does not enter an illegal
state.

The goal is to use AC to check for errors in a system.

Meta-level compilation [ECCH00] is a system for 
finding bugs in programs. 

See:
Flow-Sensitive Type Qualifiers. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. Computer Science Division Tech Report UCB//CSD-01-1162. University of California, Berkeley. November 2001. A conference version of this techincal report will appear in PLDI 2002.

http://www.cs.berkeley.edu/~jfoster/

-- Karl