# How to Specify the Behavior of Automata for Verification

I am wondering what it takes to "verify" or "prove" that an automaton is correct. What the components are that are required. It seems that an automaton would be an easier thing to formally verify as sound than say an arbitrary function. Not sure though what needs to be verified in an automaton, which is what brings up the question.

Thank you!

It feels to me like this has already been explained before (1, 2). To prove that an automaton is correct, you first must define what correctness means to you. Usually that is done by writing a specification of what it means to be correct. Then, you prove that an automaton meets the specification.

If you're interested in knowing how to do that, that's a broad subject that people have written entire books about. I suggest reading a textbook on model checking (particularly of finite-state systems).

How do you know what the specification should be? Well, you have to figure out what correctness means, or the requirements are. That's not really a question about computer science but rather a question about your application or your business domain and what problem you are trying to solve or what you're trying to do with the automaton.

If you're asking "what to verify", we can't answer that, because that's something you have to decide: you have to decide what properties you want to prove. It's like asking 'how do I prove the natural numbers?' You can't. You have to decide what theorem you want to prove, before you can ask how to prove it. If you ask a mathematician how to know what theorems to prove, the answer will probably be something like "well, you have to figure out what you want to know or what is interesting to know".

• Thank you for your post. I am still having a disconnect though when it comes to applying the principles of verification. I think a textbook on model checking finite state systems sounds like the best idea now. I don't have a sense of "what to verify" which is bothering me lol. Jun 21, 2018 at 19:05
• The tricky part is, stateful program specifications are often given in terms of automata... So, it might be hard to write a good specification for an automaton that is not fundamentally equivalent to the implementation. Jun 22, 2018 at 7:23
• @xuq01, I hear you and I think that's a valid caution, but I don't think I fully agree. I think it's common to have a specification be broken down into a bunch of properties, where each property is simpler than the entire implementation. e.g., for a traffic light, one property is "never show green in two opposing directions", which is simpler than the implementation of the logic of the traffic light. Also, each property might be expressed as either an automaton or in temporal logic, so it doesn't have to be an automaton.
– D.W.
Jun 22, 2018 at 7:50
• @D.W. Yes, sure. I would say that would be a good way to go. Essentially, we're verifying by proving extensional properties. But then proving against a "full" specification can often be difficult because of the "the program is the specification" problem. Jun 22, 2018 at 8:36