Suppose we have a finite state system given by an automaton , compile the specification into an automaton and check , that is
that is, check that the product of automata and accepts no strings (each string would be a counterexample).
Some of the operations that we can do on specifications:
Suppose we have specification
(open (read+write)* close)*
but our language is as in the Example with Procedures, so it contains many other actions (startLog, endLog, p1Start, p1End, …)
Theorem: Let be a regular language in alphabet and be a disjoint alphabet. Define
Then is also a regular.
One possibility is to treat procedure calls as gotos.
This corresponds to approximating context-free language of the procedure with a regular one - union of control-flow graphs.