Raw Temporal Logic of Actions (RTLA)
- Elementary temporal formulas are actions.
- Action A is true on behavior sigma:
- <, , ...>[[A]]
[[A]]
- First pair of behaviors is an A step.
- Temporal operator:
- <, , ...>[[always A]]
forall in Nat:
<, , ...>[[A]]
forall in Nat:
[[A]].
- Predicates:
- <, , ...>[[]] [[]]
- <, , ...>[[always ]]
forall in Nat: [[]]
TLA formulas will be subset of RTLA formulas.