Let AP = {a; b; c}.

Consider the following regular safety properties:

(a) P1: If a becomes valid, afterwards b stays valid ad infinitum or until c holds.

(b) P2: Between two neighbouring occurrences of a, b always holds.

Construct an NFA Ai for each property Pi such that L(Ai) = BadPref(Pi).

Hint: You may use a symbolic NFA with propositional formulae over the set AP as transition labels.

In the above question,

  1. What is symbolic NFA?
  2. What would be the propositional formula for P1 and P2?
  3. How to construct an NFA from the above two statement?
  4. Are there any concrete steps to do it?

The NFA for bad prefixes would be just the negation of an NFA right?

I have the solution for it, but I don't understand how did they arrive at the solution.

It would be great if somebody could explain or provide a link on how to do it?

Note: I hope it's not related to LTL since it is not part of the syllabus. Anyways, I believe that one can only construct NBA from the LTL or CTL formula right?

Thank you very much.

  • $\begingroup$ The "ad infinitum" could be an indication that you're not dealing with a regular language as recognized by an NFA but with infinite sequences, ie the usual models for LTL. I'd ask the person who set the exercise to clarify. $\endgroup$ – Kai Mar 9 '18 at 11:05
  • $\begingroup$ @Kai: Yes, you are right (when asked to draw an NFA). I am sorry, I left out a part of a question. Now I have updated the question. We have to draw the NFA for the bad prefixes. $\endgroup$ – Riya208 Mar 11 '18 at 8:47

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.