 The possible executions of complex programs can be next defined compositionally. For instance, a program “first α, then β” is a complex program, more specifically a sequence. A possible execution can be represented in an LTS by composing a two-step transition —hence a transition which can be signified by R(α;β)—between the states x and x′: there is a possible execution in x of the program α that finishes in a state y and there is a possible execution in y of the program β that finishes in x′. If the proposition A is true in x′, then the formula &lt;α;β&gt;A will be true in the state x. The programs α and β could be complex program themselves. Yet more programs can be expressed with more constructs that we will present in due time. 