How to construct an NFA Ai for the given Regular property P1 and P2?

manpreet Best Answer 2 years ago

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 b.com/tag/labels">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 b.com/tag/link">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.