You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Instead of computing ΦᵏX(0) and checking whether the intersection with B is empty, one can backpropagate B using (Φᵏ)⁻¹B. In other words, ΦᵏX(0) ∩ B = ∅ ⟺ X(0) ∩ (Φᵏ)⁻¹B = ∅.
(Note that Φ is invertible. This was the description for the homogeneous case, but it can be generalized.)
Possible benefits:
B often has a concise H-representation while X(0) depends on the precision. Hence the concrete backpropagation can be more efficient (symbolic propagation does not care).
The abstraction only takes place in X(0), so there is a simple abstraction-refinement algorithm: approximate X(0) by a box; if the intersection is nonempty, add more template directions (or use a different discretization algorithm). (Again, symbolic representation does not care.)
(Only if there are no inputs:) There is no error because B as well as (Φᵏ)⁻¹B are exact.
Downsides:
B is typically unbounded.
The possible property of B being decomposed/sparse cannot be exploited.
Instead of computing
ΦᵏX(0)
and checking whether the intersection withB
is empty, one can backpropagateB
using(Φᵏ)⁻¹B
. In other words,ΦᵏX(0) ∩ B = ∅ ⟺ X(0) ∩ (Φᵏ)⁻¹B = ∅
.(Note that
Φ
is invertible. This was the description for the homogeneous case, but it can be generalized.)Possible benefits:
B
often has a concise H-representation whileX(0)
depends on the precision. Hence the concrete backpropagation can be more efficient (symbolic propagation does not care).X(0)
, so there is a simple abstraction-refinement algorithm: approximateX(0)
by a box; if the intersection is nonempty, add more template directions (or use a different discretization algorithm). (Again, symbolic representation does not care.)B
as well as(Φᵏ)⁻¹B
are exact.Downsides:
B
is typically unbounded.B
being decomposed/sparse cannot be exploited.Related:
The text was updated successfully, but these errors were encountered: