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.
<s0, s1, . . . >[[A]] iff < s0, s1>[[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.