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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.