The Raw Logic
Raw Temporal Logic of Actions (RTLA)
- Elementary temporal formulas are actions.
- Action A is true on behavior sigma:
- <s0, s1, ...>[[A]]
<=> s0[[A]]s1
- First pair s0,s1 of behaviors is an A step.
- Temporal operator:
- <s0, s1, ...>[[always A]]
<=> forall n in Nat:
<sn, sn+1, ...>[[A]]
<=> forall n in Nat:
sn[[A]]sn+1.
- Predicates:
- <s0, s1, ...>[[P]] <=> s0[[P]]
- <s0, s1, ...>[[always P]]
<=> forall n in Nat: sn[[P]]
TLA formulas will be subset of RTLA formulas.
Author: Wolfgang Schreiner
Last Modification: May 14, 1998