Backward reachability for LTI systems

[schillic]

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.

---

Related:

• https://www.cs.ubc.ca/~mitchell/Papers/myHSCC07.pdf
• https://systemanalysisdpt-cmc-msu.github.io/ellipsoids/doc/chap_reach.html