Bounded uncontrollable variables in dReal3

[kquine]

It is sometimes useful to allow (bounded) uncontrollable variables, such as (continuously provided) input from another component. For example, consider a thermostat system with the flow:

 d/dt[x] = K * (h - ((1 - c) * x + c * xO));

where the variable xO denotes the outside temperature that can have any value in bound [a,b] during each mode. Currently this feature is not explicitly supported in dReal3, but would be useful for many purposes, e.g., elementary compositional analysis of hybrid systems.

[soonhokong]

@kquine, here let me summarize what we discussed yesterday, especially what needs to be done in the solver to support the feature. @scungao, we're happy to hear your opinion on this as well.

Let me take the above example, where xO represents the input from another component. Let's assume that this input channel xO has a range [0, 10]. In computing a trajectory of x, I think we should treat the variable xO as a constant. That is, d/dt[xO] = 0. At the same time, we should not branch on xO because we know nothing more than its range. To implement this, we need the following items:

• [ ] handle unspecified ode variable as a constant. For example, if d/dt[xO] = 0 is not given, but xO is used in other ODE definitions, we treat it as a constant parameter.
• [x] extend (declare-fun x () Real) syntax to allow users to specify different precision per variable. In the above example, we should have precision 10 for the variable xO to prevent any branching on xO. Maybe, something like (declare-fun x () Real [10.0])?

I think the two should be enough implementation-wise. Here are some remarks:

• By assigning an interval to xO, we over-approximate the behavior of xO. It even includes non-continuous trajectories of xO which might be infeasible in some examples.
• Note that we introduce another layer of over-approximation in solving ODEs. If the interval of xO is too big, the ODE integration will diverge and end up indicating that it can hit almost anything, which is not so much useful.
• In case of delta-sat where we generate a counter-example, we cannot generate a trace for xO. We can generate a counterexample which only includes the variables in our own components.

I don't think implementing the two items are hard. But I will assign higher priorities to other issues, for now.

[scungao]

I probably asked about this before, but does CAPD allow interval parameters? Namely, something like dx/dt = [1,2]*x.

[soonhokong]

You can introduce a new variable for [1, 2], let's call it p = [1, 2]. Then you can define an ODE as d[x]/dt = p * x. This is possible.

[soonhokong]

and p is treated as a parameter (d[p]/dt = 0).

[scungao]

I know. But it's something different; p itself may follow some complex dynamics. But in terms of interval bounds they may be equivalent and that needs a proof. Anyway I assume it doesn't take interval parameters then?

On Apr 29, 2015, at 14:20, Soonho Kong [email protected] wrote:

and p is treated as a parameter (d[p]/dt = 0).

— Reply to this email directly or view it on GitHub.

[soonhokong]

Anyway I assume it doesn't take interval parameters then?

I'm afraid that we're using the same terminology for the different things. Let me elaborate what we have in CAPD4. In CAPD4, we have ODE variables and ODE parameters. The only difference between them is that you can define their dynamics for ODE variables while ODE parameters are assumed to be constants (d/dt[p] = 0). Both of ODE variables and parameters can have interval initial values in an integration.

[scungao]

What I wonder is whether syntactically you can write interval arithmetic in the ODEs, like instead of dx/dt = 2_x, write dx/dt = [1,2]_x. The benefit is that way you don't need to name the parameter at all and no need to control it in ICP.

On Apr 29, 2015, at 14:49, Soonho Kong [email protected] wrote:

Anyway I assume it doesn't take interval parameters then?

I'm afraid that we're using the same terminology for the different things. Let me elaborate what we have in CAPD4. In CAPD4, we have ODE variables and ODE parameters. The only difference between them is that you can defines their dynamics for ODE variables while ODE parameters are assumed to be constants (d/dt[p] = 0). Both of ODE variables and parameters can have interval initial values in an integration.

— Reply to this email directly or view it on GitHub.

[soonhokong]

I don't think it's possible. Actually, CAPD people recommended us to use a variable even for a constant. So I don't think they will implement that in the future...

The benefit is that way you don't need to name the parameter at all and no need to control it in ICP.

We can introduce the auxiliary parameter variables between ICP and CAPD, so that it won't affect ICP. That's one thing we can do.

[soonhokong]

@kquine, I just implemented the first item in my first reply. Please take an example, src/tests/nra_ode/multi_precision_01.smt2. To specify a precision for a variable, use the following syntax:

(declare-fun v_0_0 () Real [1.0])

When dReal does branching in ICP, it takes this per-variable precision into an account and does not perform branching on v_0_0 if its interval width is smaller than 1.0. The following is an excerpt from the test run. As you see v_10_t has a wider interval than x_10_t.

...
v_10_t : [-18, 18] = [-1.646772665550875, -1.586156869328274]
...
x_10_t : [0, 15] = [0.3500000000000001, 0.3505841407878279]
...

[soonhokong]

For now, to use this feature, you have to edit an .smt2 file manually. I'll update dReach soon to automate the process.