guideline for handling interpolation and extrapolation in TL

[TomyYamy]

When time = [0, inf], then we have time bounded trajectory traj_time = [s-time, e-time], how we handle the start bound = [0, s-time) and the end bound = [e-time, inf]?

I think now we just ignore the start bound = [0, s-time)
For the end bound = [e-time, inf], we expect the extrapolation of the end of trajectory, then calculate [e-time, end of bound of timed operator].
That makes sense, other wise, the robustness trajectory becomes shorten and shorten in every nest of formula.

[TomyYamy]

I guess online does not use "extrapolation" from the end point of traj. But offline use "extrapolation".

[TomyYamy]

it relates #60

[TomyYamy]

Finally I find even either online, offline, we will not use extrapolation.
I misunderstand when I implement "unbounded" timed operator

[TomyYamy]

We discussed

rho(O[T1,T2]phi, w, t) =   -inf                                                      if t<T1
                           max_{t' in ([t-T2, t-T1] \cap [0,inf))} rho(phi, w, t')   otherwise

I think that is related in this issue.

It depend on how we define dense time robustness.
I think regarding not using extrapolation notion, we should not return any information for "if t<T1".
I'm not sure that is semantically correct. let's discuss it.

[TomyYamy]

Still we need to discuss which is better to return either [] or inf/-inf when there are no data points.

[TomyYamy]

We will keep use only interpolation because it leads misunderstanding for "application user".
However "TL user" need it in specific case. Still we remain it.

[TomyYamy]

It relates #112