Take a program (infinite state) and automaton for specification , and run both and in parallel. reports an error if it gets into a state from which it cannot reach an accepting state.

Advantage: works for infinite-state systems, and for very expressive specifications

Disadvantage: run-time checking only, we cannot tell anything about executions that the program did not experience.

See Monitoring oriented programming