Temporal Logic - LTL - 1

Temporal logic allows expressing properties that a system should satisfy along time. We will first talk about linear temporal logic which expresses properties over every possible path. For example, let's consider the following model:

Let r be the proposition representing that the system is running and h the proposition representing the the system has halted.

Then we could check whether it always holds that this system will always halt. According to the state machine representation this is false: We can consider the path r,r,r,r,... and never get to the halt state.

With linear temporal logic we can express the property "the system will always halt" and other properties referring to time.

For example, the operator G formula (globally) indicates that from a given state, every state state satisfies formula (formula can be any linear temporal logic formula.

For instance, the formula G (r or h) is true. Every state of every path starting from the initial state satisfies that r or h hold. However, the formula G r is not satisfied by every path.

The operator F formula indicates that formula will be true at some state in the future.

The given example does not satisfy F h (because of the given counterexample where the second state is not reached..

However the formula F r, holds (a state satisfying r is reached at the first state)

In future posts we will consider some other examples and other operators.