![](https://csdnimg.cn/release/download_crawler_static/1052006/bg9.jpg)
The Temporal Logic of Actions · 9
an A step iff s[[ A]] t equals true. We now define [[A]] to be true for a behavior iff the
first pair of states in the behavior is an A step (Note 5). Formally,
s
0
,s
1
,s
2
,...[[ A]]
∆
= s
0
[[ A]] s
1
(9)
RTLA formulas are built up from actions using logical operators and the temporal
operator ✷.Thus,ifA is an action, then ✷A is an RTLA formula. Its meaning is
computed as follows.
s
0
,s
1
,s
2
,...[[ ✷A]]
≡∀n ∈ Nat : s
n
,s
n+1
,s
n+2
,...[[ A]] b y ( 6 )
≡∀n ∈ Nat : s
n
[[ A]] s
n+1
by (9)
In other words, a behavior satisfies ✷A iff every step of the behavior is an A step.
In Section 2.4, we observed that if P is a predicate, then s[[ P ]] t equals s[[ P ]] .
Therefore,
s
0
,s
1
,...[[ P ]] ≡ s
0
[[ P ]]
s
0
,s
1
,...[[ ✷P ]] ≡∀n ∈ Nat : s
n
[[ P ]]
In other words, a behavior satisfies a predicate P iff the first state of the behavior
satisfies P . A behavior satisfies ✷P iff all states in the behavior satisfy P .
WewillseethattherawlogicRTLAistoopowerful;itallowsonetomakeas-
sertions about behaviors that should not be assertable. We will define the formulas
of TLA to be a subset of RTLA formulas.
4.2 Describing Programs with R TLA Formulas
We have defined the syntax and semantics of RTLA formulas, but have given no
idea what RTLA is good for. We illustrate how RTLA can be used, by describing
the simple Program 1 of Figure 1 as an RTLA formula. This program is written in
a conventional language, using Dijkstra’s do construct [Dijkstra 1976], with angle
brackets enclosing operations that are assumed to be atomic. An execution of this
program begins with x and y both zero, and repeatedly increments either x or y (in
a single operation), choosing nondeterministically between them. We now define
an RTLA formula Φ that represents this program, meaning that σ[[ Φ ]] e q u a l s true
iff the behavior σ represents a possible execution of Program 1.
The formula Φ is defined in Figure 2. The predicate Init
Φ
asserts the initial
condition, that x and y are both zero. The semantic meaning of action M
1
is a
relation between states asserting that the value of x in the new state is one greater
than its value in the old state, and the value of y is the same in the old and new
states. Thus, an M
1
step represents an execution of the program’s atomic operation
of incrementing x. Similarly, an M
2
step represents an execution of the program’s
other atomic operation, which increments y. The action M is defined to be the
disjunction of M
1
and M
2
,soanM step represents an execution of one program
operation. Formula Φ is true of a behavior iff Init
Φ
is true of the first state and
every step is an M step. In other words, Φ asserts that the initial condition is true
var natural x, y =0;
do true → x := x +1
true → y := y +1 od
Fig. 1. Program 1—a simple program, written in a
conventional language.
ACM Transactions on Programming Languages and Systems, Vol ?, No. ?, November 1993.