I am reading the example given in [1], section 4.2. It deals with applying weakest precondition (wp) rules to ensure that the velocity of a car doesn't exceed a certain limit. We have the following reinforcement learning equation and we want to constrain it across 2 timesteps -
$v' = v + 0.1a + \epsilon$
Based on a previous question that I asked [2], I modified the description given in that example to look more like a typical program with constraints (given by {}).
$\{v_0 + 0.1a_0 + \epsilon_2 \le1 \land v_0 + 0.1a_0 + \epsilon_2 + 0.1a_1 + \epsilon_1 \le 1\}$
$v_1 = v_0 + 0.1a_0 + \epsilon_2$
$\{v_1 \le1 \land v_1 + 0.1a_1 + \epsilon_1 \le 1\}$
$v_2 = v_1 + 0.1a_1 + \epsilon_1$
$\{v_1 \le1 \land v_2 \le 1\}$
My question is, how will the program check the first precondition ($\{v_0 + 0.1a_0 + \epsilon_2 \le1 \land v_0 + 0.1a_0 + \epsilon_2 + 0.1a_1 + \epsilon_1 \le 1\}$), since at time step 0, it won't know the value of $a_1$.
Please let me know if any clarification from my side is needed.
[1]. Anderson, Greg, Swarat Chaudhuri, and Isil Dillig. "Guiding Safe Exploration with Weakest Preconditions." International Conference on Learning Representations. 2023.
[2]. How did the authors of Spice apply weakest precondition rule on their example car problem?
