Resumable analysis

[mforets]

Sometimes one doesn't know the time horizon of interest for the reachability computation, and it would be useful to be able to resume a computation.

For example, say you start with :T=>1.0 but then you realize that this time horizon is not enough and want to try :T=>2.0. Most tools will need to run again the whole computation, although it would be faster if you can resume from the final step of the first computation.

The idea is to have an option like :resumable such that one fix a time horizon, observe the results, then be able to resume the computation from the final step.

CC @nikos-kekatos

[schillic]

I see two fundamentally different ways here.

Let k_n be the last iteration of the previous run.

1. Read in X(k_n) and use it as the new X(0) (i.e., skip discretization). Continue normally.
2. Start as usual, but do not compute X(1), X(2), .... Instead compute X(k_n + 1), X(k_n + 2), .... This means that you have to start with Phi' = Phi^{k_n}.

I expect 2. to be more precise, but also more expensive due to the additional matrix multiplications.

EDIT: Note that 1. only works if all input variables have been in the output. So 2. should also be the more general solution!

[mforets]

i think that these ways are good; with option 2 looks we can reuse the existent functions, but starting with the shifted sequence. however i think one also needs to store intermediate sets $Wi(k)$ in equation (19) which correspond to the evolution due to the inputs and initial states equal to zero.

[schillic]

True, I completely forgot about the inputs. But we only need the very last set, right?

[mforets]

yes.

[nikos-kekatos]

Having a resumable option would be a nice feature! At least, from my experience with reachability tools (especially, SpaceEx), the need to continue/pause the computations has been important.

However, I think that we need to distinguish between what is going on with SpaceEx and with other tools. SpaceEx employs variable time steps (adjust them for each direction), searches for a fixed point, and differentiates between local and global time horizon.

That said, your LazySets reachability algorithm should be more straightforward. I guess there are two main operations that should be applied:

(i)for plotting, save original results, project in 2D/3D, compute new sets, project again in 2D/3D and concatenate, and

(ii) find the new initial set guaranteeing over-approximation. This probably is direct as long as we clarify what the final set should be, what type of dynamics we have, etc.