# How did this work apply weakest precondition rule on their example car problem?

While reading the example given in [1]., I couldn't understand how the authors set up the logic to compute the weakest preconditions (wp) in their car example in section 4.2.

The dynamics of the problem are given by -

$$x' = x + 0.1v$$

$$v' = v + 0.1a + \epsilon$$

I don't see the authors working on the former equation, only the latter. In addition, while reading about wp from the book [2], I learned that one needs to come up with a suitable postcondition. I believe the postcondition here is $$v <= 1$$. Why did the authors start the wp computation using $$v_1 <=1 \land v_2 <= 1$$? Also, in the next step they do $$v_1<=1 \land v_1 + 0.1a_1 + \epsilon_1 <= 1$$. Why did they only expand the equation on the right of the conjunction?

Here is how I imagined it should have been done (based on my very limited knowledge of wp computations -

We have the equation $$v' = v + 0.1a + \epsilon$$ and we have a horizon of 2. Therefore, we write this equation 2 times (because that's how RL algorithms are unrolled) -

$$v_1 = v_0 + 0.1a_0 + \epsilon_0$$

$$v_2 = v_1 + 0.1a_1 + \epsilon_1$$

Now we set up a postcondition on $$v_2$$ such that $$v_2<=1$$ and then work backwards. My understanding is probably wrong, but I'd like the reader to see where I am getting confused.

Please let me know if any clarification from my side is needed.

Regarding the relation between $$x'$$ and $$x$$ and also $$v_2$$ and $$v_1$$: My understanding here is that $$x'$$ represents the subsequent state of the variable $$x$$. This is because of the following line in the paper - "A policy, in interaction with the environment, generates trajectories (or rollouts) $$x_0,u_0, x_1,u_1, \ldots, u_{n-1}, x_n$$ where $$x_0 \sim p_0$$, each $$u_i \sim \pi(x_i)$$, and each $$x_{i+1} \sim P(x_i, u_i)$$." Here we can see that each state can be obtained from the subsequent state except the initial state.

[1]. Anderson, Greg, Swarat Chaudhuri, and Isil Dillig. "Guiding Safe Exploration with Weakest Preconditions." International Conference on Learning Representations. 2023.

[2]. Pierce, Benjamin C., et al. "Software foundations." Webpage: http://www. cis. upenn. edu/bcpierce/sf/current/index. html (2010).

• That the car's position, $x$, is mostly ignored in that example wp calculation is due to the fact that the car's position occurs neither in the postcondition ($v \leq 1$) nor in the right-hand-side of the equation for $v$. With the safety horizon being $2$, the postcondition after $2$ iterations is $v_1 ≤ 1 ∧ v_2 ≤ 1$. The second iteration affects ($x_2$ and) $v_2$ only. Computing wp once yields the assertion between the two iterations. That's $v_1 ≤ 1 ∧ v_1 + 0.1a_1 + ε_1 ≤ 1$.
– Kai
Feb 4 at 22:47
• @Kai "With the safety horizon being 2, the postcondition after 2 iterations is $v1≤1∧v2≤1$." I see. Why didn't the authors include $v_0$, i.e $v0<=1∧v1≤1∧v2≤1$ Feb 5 at 2:51
• @Kai - "The second iteration affects (x2 and) v2 only. Computing wp once yields the assertion between the two iterations. That's v1≤1∧v1+0.1a1+ε1≤1" -> Why did the author then work on both sides in the next step. This is taken from the paper - "Stepping back one more time, we find the condition $v_0 + 0.1a_0 + \varepsilon_2 \leq 1 \land v_0 + 0.1a_0 + 0.1a_1 + \varepsilon_1 + \varepsilon_2$ \leq 1" Feb 5 at 2:55
• @Kai, Thank you for your comments. Please let me know if any clarification is needed from my followup comments. Feb 5 at 2:56

1.

I don't see the authors working on the former equation, only the latter.

That's because $$x$$ doesn't matter:

• it does not occur in the postcondition ($$v \leq 1$$) investigated here
• it does not occur in the RHS of the equation for $$v$$

Why did the authors start the wp computation using $$v_1 \leq 1 \wedge v_2 \leq 1$$?

They state that their safety horizon is $$2$$, that is, they want to express that the safety condition holds both after $$1$$ step and after $$2$$ steps. In their notation, where $$v_i$$ refers to the value of $$v$$ after $$i$$ steps, that's exactly expressed by the condition $$v_1 \leq 1 \wedge v_2 \leq 1$$.

3.

Also, in the next step they do $$v_1 \leq 1 \wedge v_1+0.1 a_1 + \epsilon_1 \leq 1$$. Why did they only expand the equation on the right of the conjunction?

Because the 2nd iteration of the step function affects the variables subscripted with $$2$$. The LHS of the conjunction has only a $$1$$-subscripted variable, $$v_1$$. It is thus invariant under the substitution $$[v_2 \mapsto 𝑣_1+0.1 a_1 + \epsilon_1]$$ performed to compute the weakest precondition.

Why didn't the authors include $$v_0$$?
(a) They state in the example that $$v_0 = 0.9$$, trivially satisfying $$v_0 \leq 1$$ and (b) $$v_0$$ is not affected by the dynamics.
Because both sides refer to $$v_1$$, which is assigned to in that step. Whence the substitution applies meaningfully to both.