Newcomer Questions

[kacem belout]

Hi,

I am a beginner with the temporal logic of actions, and I have some questions about :

1.  Concerning the evaluation semantics rule (definition) of an action-formula A with respect to a behavior σ ; which says that A is true for a behavior if and only if A is true for the first pair of states of this behavior. A is a logical formula that represents an individual system action.

 

<s₀, s₁, . . . >[[A]] iff < s₀, s₁>[[A]]

 

Now, for a behavior from the set of allowed behaviors of a system(a program) characterized by the Phi- safety fomula Φ ≡ Init ˄ □[Next]_f , I can see that the individual action-formulas A which respect this evaluation semantics rule are only the ones representing the first actions in the system design(i.e. first actions or initial actions by default) the others do not (i.e. they are false), especially if the preconditions of the system actions are defined in terms of their control-state information. Is this observation reasonable ?. Is it possible and reasonable to transform the action-formulas representing the system actions, to make them as if they are starting from the initial state, in order to respect the evaluation semantics rule ?

 

2.  In TLA, a system(a program) is usually characterizd by the Phi-safety formula,   Φ ≡ Init ˄ □[Next]_f

 

And in RTLA(Raw TLA), we can write the following form :

Φ ≡ Init ˄ □ Next

 

The two logical formula forms are temporal formulas characterizing the set of all allowed(possible) behaviors(infinite or finite sequences of states).

 

Now, with respect to the implicit transition system(TS)-based model of a program, which is also called the control-flow transition graph, the two above formula forms are capturing the TS-Runs, nammely its dynamic behavior (walks through/above the graph(as dynamic image)).

 

So, what about the following logical formula form with respect to the transition system model(transition graph := < Control-States, Transition Relation >) ?:

 

Φ ≡ Init ˄ Next

 

In TLA context, is it reasonable to say that this formula form is characterizing the set of allowed sequences made up only of two states (two-state sequences) ?. Can I say that this formula is the static image(photo) of the transition graph ?

 

3.  question about the TLA proof system.

In TLA context, systems(programs) are specified in terms of their actions. But in the TLA proof system, I can not see(find) proof rules about actions, that is, rules that permit to deduce some action from the set of system actions, as in traditional predicate logic proof system.

 

Thanks.

[Leslie Lamport]

I could not understand Question 1.  Are you aware that the formula Init /\ [][Next]_vars is true of a behavior if and only if Init is true in the initial state and EVERY SUCCESSIVE PAIR of states in the behavior satisfies Next or is a stuttering step?

 

Question 2: The formula Init /\ Next, interpreted as a temporal-logic formula, makes an assertion about the first two states of the behavior.  It makes no assertion about the subsequent states, so it allows behaviors that do anything else in subsequent states.

 

Question 3: Actions are ordinary formulas, so there is no need for special rules to reason about them.  More precisely, the only special rules needed are the following ones for the prime operator:

 

   - c’ = c if c is a constant

 

   - Prime distributes over constant operators—e.g., (x+y)’ = x’ + y’

Leslie