SU-CS238V FEB182025 — Jemoka Knowledge Base

Key Sequence Notation New Concepts Important Results / Claims Taylor Models Concrete Reachability Questions Interesting Factoids Partitioning As a way to prevent wrapping effect, you can partition your initial set into smaller chunks and propagate them separately, and then union them together. Discrete Reachability Remember: we can represent discrete systems using directed graphs. reachable sets for discrete systems Breadth-first search to get the reachable sets. We can terminate the BFS by checking if one subset of points is contained within another:

\begin{equation} \mathcal{R}_{1:d} \subseteq \mathcal{R}_{1:d-1} \end{equation}

and once we have this we know that the set outputs are going to be invariant. Probabilistic Reachability “Will this thing or that thing be reached first?” — “it allows us to tell us the distribution over reachable states at each time stamp” occupancy analysis The probability of occupancy tells us the distribution over reachable states at each time stamp

\begin{equation} P_{1}\left(s\right) = P_{s}\left(s\right) \end{equation}

For t > 1:

\begin{equation} P_{t+1} \left(s\right) = \sum_{s’ \in \mathcal{S}}^{} T\left(s’, s\right) P_{t}\left(s’\right) \end{equation}

finite horizon reachability What if we want to know the probability any of an entire set of states is reached? Call it R_{t}: for t = 1, we have:

\begin{equation} R_{1} \left(s\right) = \begin{cases} 1, \text{if } s \in \mathcal{S}_{T}\\ 0 \end{cases} \end{equation}

for t > 1, we write:

\begin{equation} R_{t+1} \left(s\right) = \begin{cases} 1, \text{if } s \in \mathcal{S}_{T} \\ \sum_{s’ \in \mathcal{S}}^{} T\left(s, s’\right) R_{t}\left(s’\right), \text{otherwse} \end{cases} \end{equation}

this is not a probability distribution over all states! it doesn’t sum to 1—its just the probability of any given node reaching at that set. Discrete State Abstractions Converting continuous state to Discrete State Abstractions. Grid up your input state space, and take the entire grid and propagate it using any inclusion functions. At every step, map back to the grid and us that as the current reachable (possibly non-convex) set. A finer partition will result in less overapproximation.