Describing Programs with RTLA
- InitPhi asserts initial condition.
- Action A1 asserts effect of first guarded command.
- Action A2 asserts effect of second guarded command.
- Action A asserts effect of non-deterministic composition.
- Formular Phi represents whole program:
- InitPhi is true in first state.
- Every step is an A step.
Each equivalent formula is a valid representation of the program.
Author: Wolfgang Schreiner
Last Modification: May 14, 1998