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

We have several definitions and notations here, let's go through these first:

  • We are given a set of atomic propositions AP. It is not said here explicitly, but usually this means we are interested in languages that have as alphabet the power set of AP. So for AP = {a,b,c}, our alphabet would be Sigma = { {}, {a}, {b}, {c}, {a,b}, {a,c}, {b,c}, {a,b,c} }.

  • As you can see, writing out this power set alphabet can be a lot of work. For this reason, there is an alternative notation based on propositional formulas. Consider a propositional formula phi over the variables AP. We can take a symbol x from Sigma and in phi set all atomic propositions contained in x to true and all other atomic propositions to false. Then we evaluate phi and it becomes true or false. We can understand phi to refer to all those x from Sigma for which phi evaluates to true.

    For example, the formula phi="a and not b" refers to the symbols {a} and {a,c}. The formula phi="a" refers to the symbols {a},{a,b},{a,c},{a,b,c}. The formula phi="not a" refers to the symbols {},{b},{c},{b,c}. The formula phi="not a and not b and not c" refers only to the symbol {}. The formula phi="true" refers to all symbols from Sigma. The formula phi="false" refers to no symbol (not to be confused with the symbol {}). And so on ...

    This logic is the notation used on the NFA edges in your example.

  • We call a language L over finite words "regular" if there is a NFA that accepts L.

  • We call a language L over infinite traces a "safety property" if every trace not in L has a bad prefix, meaning a finite prefix w, such that no infinite continuation of w is in L.

  • We call a safety property "regular" if the language of its bad prefixes is regular. Note we are dealing with two different notions of "regular" here, one for languages of finite words and one for safety properties over infinite traces.

General approach

You are dealing with the problem of going from an informal description of a safety property to a formal description of the language of its bad prefixes. There is no general rule for how to do this, but remember that on an intuitive level, a safety property means "some bad event never happens". The language of the bad prefixes is then exactly those finite words for which "the bad event happens at some point". Your approach would therefore be to analyze what the "bad event" is.

(This is a general problem in model checking of course, when going from informal descriptions to a formal model there is a risk of not perfectly capturing the original description.)

Consider P1: The bad event is "a becomes valid and afterwards b is valid only finitely many steps and becomes false before c becomes true". We can turn this into a slightly more verbose description: "a becomes valid, afterwards we see some b's but no c's and then we see no b and no c". We can use this description to derive a formal definition for "the bad event happens at some point". I personally find regular expressions more intuitive than NFAs, so I would first try to build a regular expression and then build the NFA from that afterwards:

(true)* a (b and not c)* (not b and not c) (true)*

This regular expression describes all finite words where at some point the bad event happens. We use the (true)* at the beginnging and the end because we do not care what happens before or after the bad event. The regular expression is already very close the NFA in your example, in general it should be easy to build NFAs from such regular expressions. You can see that the notation based on propositional formulas makes this much more compact compared to writing out the symbols explicitly, e.g. writing "a" is shorter than writing the full regular expression ({a} + {a,b} + {a,c} + {a,b,c}).

This is not the only solution, instead of requiring to see (b and not c)* before seeing (not b and not c), it would also suffice to require to see (not c)* before seeing (not b and not c). This would result in the regular expression:

(true)* a (not c)* (not b and not c) (true)*

The only difference to the first solution would be that instead of requiring to match the first (not b and not c) we see, we could also skip over some (not b and not c)'s because they also match (not c), as long as we match a (not b and not c) eventually. So in a way the first solution is the better one because the resulting NFA is more deterministic.

Consider P2: The bad event would be having two a's such that in between at some point b does not hold. Turning this into a slightly more verbose description, we would get "we see a, afterwards we see some b's without seeing a, then we reach a point where we see neither b nor a, afterwards we see any symbols until we reach the closing a". Turning this into a regular expression for "the bad event happens at some point" gives us:

(true)* a (b and not a)* (not b and not a) (true)* a (true)*

Again this is very similar to the NFA in your example, it should be easy to see how to construct an NFA from such an expression. As before we could also obtain an alternative solution, by relaxing the (b and not a)* to (not a)*, the only difference would be that this would allow to skip over some (not b and not a), as long as we match one eventually. Also, we could strengthen the middle (true)* to (not a)*, requiring us to match the first closing a instead of allowing to skip over some a's before matching the closing a:

(true)* a (not a)* (not b and not a) (not a)* a (true)*

Regarding the number of states

Since you asked about how to know the number of states: I would first try to obtain some NFA and then check if it can be simplified. For the NFAs in your example, I see no way to further reduce the number of states, but in general minimizing NFAs is a hard problem (reference), so there is no efficient algorithm for that. Of course, if you obtain a fully deterministic automaton, you can apply the standard algorithm for minimizing DFAs.


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.