Linear Temporal Logic and Computation Tree Logic

We give the syntactic definition of linear temporal logic (LTL) and computation tree logic (CTL) here:

ltl_expr :: bool_expr – Boolean expression

| ltl_expr

| ltl_expr – logical not

| ltl_expr ltl_expr – logical and

| ltl_expr ltl_expr – logical or

| ltl_expr ltl_expr – logical implies

| X ltl_expr – next state

| G ltl_expr – globally

| F ltl_expr – finally

| ltl_expr U ltl_expr – until

| ltl_expr R ltl_expr – releases

ctl_expr :: bool_expr – Boolean expression

| ctl_expr

| ctl_expr – logical not

| ctl_expr ctl_expr – logical and

| ctl_expr ctl_expr – logical or

| ctl_expr ctl_expr – logical implies

| EG ctl_expr – exists globally

| EX ctl_expr – exists next state

| EF ctl_expr – exists finally

| AG ctl_expr – forall globally

| AX ctl_expr – forall next state

| AF ctl_expr – forall finally

| E ctl_expr U ctl_expr – exists until

| A ctl_expr U ctl_expr – forall until

The bold symbols are terminal symbols. These symbols, except the parentheses “ ” and

“ ”, are called logic connectives. Among these logic connectives, , ,X,U is adequate for LTL since all other connectives can be expressed using connectives in the adequate set. The adequate sets of CTL contains one of , , one of EG, , , and all of

, ,EU .

The semantics of these temporal connectives are formally defined in [8]. The LTL system interprets the formulas in a linear time sequence. An LTL formula must hold in all execution sequences, while CTL ones can quantify existence or all paths since the formulas are interpret as computation trees. We informally state the semantics of LTL as follows: For any trace ,

1. X is true if holds in state .

3. G is true if holds in all states with 0.

4. U is true if holds in some state with 0 and holds in all states with

0 .

5. R is true if holds in all states with 0 up to and including the state where also holds. Alternatively, it may be the case that never holds in which case must hold in all states with 0.

We informally state the semantics of CTL as well: For any system represented as a model or a computation tree,

1. EX is true in a state if there exists a state such that a transition goes from to and is true in .

2. AX is true in a state if for all states where there is a transition from to , is true in .

3. EF is true in a state if there exists a trace such that is true in .

4. AF is true in a state if for all traces is true in . 5. EG is true in a state if there exists a infinite trace such that is

true in every .

6. AG is true in a state if for all infinite traces is true in every . 7. E U is true in a state if there exists a trace such

that is true in every state from to and is true in state .

8. A U is true in a state if for all traces is true in

every state from to

In SYN-sequence, no two events will be executed simultaneously. We also suppose that each event will be executed exactly within one state for other proposes, e.g. of counting the numbers that an event was executed. For example, we may have

specification such as the execution of event does not exceed three times. This can then be expressed as G F F F . Recall that each event can be executed exactly once in SYN-sequences.

To verifying SYN-sequences, one may often want to know whether the execution of event always happens before event . We denote this happened before relation as . This relation says that, along all possible execution paths, must be executed first, and then will be executed. Note that we assume no two events will be executed at the same time. This can be expressed as F XF or G F in temporal logic.

Now we are confident that this formula expresses always happens before . In this formula will be executed at least once. Then will also be executed at least once.

Since and cannot be executed simultaneously, this formula can be simplified to F F . The truth table of XF and F is given in Figure 4.1.

1 1

This tells us that along each trace will never be executed or will not be executed from some moment on. In reality, this formula specifies that will never happen after . Since we assume that each event will be executed exact once, this formula turns to mean 1 in the state where is executed. This asserts that will never happen

after . In all the other states along the path, this formula holds since is not executed.

Note that G F stands for the happened before relation on the assuming that each event will be executed exact in one state. The truth table of F is shown in Figure 4.2.

0 0 1

0 1 1

1 0 1

1 1 0

Figure 4.2. The truth table of F .

At a glance, we may think that these two formulae are quite different. First, F XF requires both and to be executed at least once, while G F allows both and not to be executed. Since we suppose each event to be executed exactly once, F XF should be augmented as

G F F F

1

1 1

1

F F

Hence these two formulae have the same effect.

A fallacious formula for happened before relation is G F . Since

G F

G F

G F

G G ,

this formula is error. If not, must be true in all states. This contradicts the assumption that each event will be executed in exactly one state.

Another well-known specification in concurrent system is that the execution of events and must be in parallel. We denote this parallel relation as . This can be

expressed as G . We suppose that the happened before

relation has higher priority than has. The truth table of this formula is shown Figure 4.3.

Sometimes we may want to check some properties involving shared data, e.g. the shared variables cannot be accessed in events and simultaneously. This can be expressed as

G , ,

where wildcards stand that we don’t care about the operation type of data access.

Let’s see one more specification: If there exists an execution loop of events , , , then this loop can iterate at most three times. For simplicity, we first define a symbol as following:

F F

The symbol stands for the execution loop of events , , . In this loop is executed in this state, and it is supposed that no two events will be executed simultaneously. Then the given specification is

G F F F

Before closing this section, we list some LTL properties which should hold in the SYN-sequence shown in Figure 3.3:

X p0.0 XX p0. 1 XXX p1.0 XXXX p0.2 p1.1 XXXX p0.2 XXXXX p0.3 p1.1

XXXX p0.2 XXXXX p0.3 XXXXXX p1.1 XXXXXXX p1.2 XXXX p0.2 XXXXX p1.1 XXXXXX p0.3 p1.2

XXXX p0.2 XXXXX p1.1 XXXXXX p0.3 XXXXXXX p1.2 XXXX p0.2 XXXXX p1.1 XXXXXX p1.2 XXXXXXX p0.3 XXXX p1.1 XXXXX p0.2 p1.2

XXXX p1.1 XXXXX p0.2 XXXXXX p0.3 p1.2

XXXX p1.1 XXXXX p0.2 XXXXXX p0.3 XXXXXXX p1.2 XXXX p1.1 XXXXX p0.2 XXXXXX p1.2 XXXXXXX p0.3 XXXX p1.1 XXXXX p1.2 XXXXXX p0.2 XXXXXXX p0.3 XXXXXXXX p1.3

where p . denotes event in process . One might find that this set of properties altogether completely describes the behavior of the given SYN-sequence. We will use this property set to validate the model we constructed later.