How can I model the 'Eventually' behavior in Linear Temporal Logic (LTL) using the Temporal Operator blocks in Simulink Design Verifier 2.2 (R2012a)?

I am trying to use Simulink Design Verifier 2.2 (R2012a) to represent the 'Eventually' operator in Linear Temporal Logic (LTL).

Is there any way this can be done using the available blocks in this block library?

Answer 1

[MathWorks Support Team]

The 'Eventually' temporal operator can be briefly explained as follows. Let us think about the statements:

    1. Eventually A

This states that at some unspecified point down the line, A must become true.

    2. If A, then eventually B

This states that once A is true, B must be set to true at some point down the line. Additionally, A needs to remain true until B becomes true.

The way behavior like this can be modeled with the Simulink Design Verifier blocks is to use the Extender block. Setting the Extension Period to 'Infinite' ensures that an input will stay true for as long as is necessary. This can then be coupled with an External Reset for whenever the input needs to be set back to false. The documentation for the Extender block discusses this in more detail:

 <http://www.mathworks.com/help/toolbox/sldv/ref/extender.html>

In other words, to model 'Eventually' behavior, the input would be indefinitely extended until the output becomes true. Once this output is true, it can be fed back to the External Reset of the block and the input will be reset to false. For the example of "If A, then eventually B", this would enforce that A remain true (or positive) until B eventually also becomes true (or positive).