Search code examples
model-checking

What is the interpretation of <>P -> (!P U R)

What is the interpretation of <>P -> (!P U R)? This seems to be contradiction since in future P is expected and checking the absence of P until R. Model checking tool passes this via BDD as well as BMC techniques.

Solution

  • I don't see any contradiction.

    The property is made true by any Buchi automaton s.t.

    • P is always false [because the premise of the implication is false], or
    • At some point in the future P becomes true, yet for some time P may be false until R becomes true.

    i.e.

    enter image description here

    In natural language, one would express that property as follows: "If, by any chance, sooner or later P becomes true, then it must be the case that the 'event' R fired first".

    For instance, you can imagine P be "sending answer message" and R be "received input message" and the whole property be "no unsolicited answer message is ever sent".