Suppose I have modeled the behavior of my system by Deterministic Finite Automaton (DFA) A, and I need to check if it satisfies a safety condition. I have created another DFA S, which represents the behavior that invalidates the safety property. Then I need to take intersection of these two to see if A contains bad traces. Finally, I need to code A into C program.

  • Could you please introduce me to a few tools that take two DFA as input and tell me if the intersection is not empty?

  • Are there tools that translate the DFA directly to C or Java Code?

Many Thanks

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.