logicstatenfamodel-checking

Model Checking : Bad Prefixes using NFA

We use NFA to model BadPrefixes for the safety property.I want to understand for a given Safety property , how to model the NFA.

The following images are for reference. enter image description here

enter image description here

enter image description here

For instance, for safety property P2 ,Can someone explain how to know how many states are required(solution has 4) and which logic to use on the edges, how in Fig.,3 and Fig.4 , the edges are selected to satisfy the badprefixes P1 and P2.Thanks.

Solution

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

    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.