Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>You can encode the differential equation easily in Z3 as it is just a set of n linear (affine) functions over n^2 + n real constants (n^2 from a_ij, n from b_i) and n real variables (x_i). You can encode this directly in Z3.</p> <pre><code>dotx_1 = a_11 * x_1 + a_12 * x_2 + a_13 * x_3 + ... + a_1n * x_n + b_1 dotx_2 = a_21 * x_1 + a_22 * x_2 + a_13 * x_3 + ... + a_2n * x_n + b_2 ... dotx_n = a_n1 * x_1 + a_n2 * x_2 + a_n3 * x_3 + ... + a_nn * x_n + b_n </code></pre> <p>Here's a link for a 2x2 version of this in Z3Py: <a href="http://rise4fun.com/Z3Py/pl6P" rel="noreferrer">http://rise4fun.com/Z3Py/pl6P</a></p> <p>However, encoding the solution of the ODEs will be difficult, as the solution of linear ODEs involve exponentials (transcendental functions). For the class of ODEs with solutions that can be represented as polynomials (over the a_ij constants, x_i variables, and/or a time variable t), you would be able to encode the (exact) solutions as polynomials in Z3 (see, e.g., [1]).</p> <p>For the general solutions that involve transcendentals however, you have many possible options, depending on what you are trying to accomplish. One option is modeling the transcendentals as uninterpreted functions. There is some work in various SMT-LIB benchmarks that do this, but I am not so familiar with these, so hopefully someone else can point out a link to them. This would be most useful if you wanted to prove some lemmas about the solutions of such ODEs. Some tools like MetiTarski maintain upper and lower bound approximations of transcendentals (using, e.g., truncated Taylor series, which are polynomials, and hence representable in Z3), but I'm not aware of the status of this in Z3, but it looks like there may be some support that Leonardo could comment on more [6].</p> <p>If you are doing reachability computations, then you could overapproximate the reach set, which can be done with simpler (more abstract) representations of the solutions of the ODEs. For instance, you could apply a variant of the hybridization technique [2] and overapproximate the linear dynamics with rectangular dynamics, e.g., partition an interesting subset of the state space, then in each partition, under and over approximate each dimension dotx_i = a_i1 x_1 + a_i2 x_2 + ... + b_i with dothatx_i \in [C, D] for some constants C and D chosen to ensure every solution of the original (concrete) x_i is contained in the set of overapproximated (abstract) solutions hatx_i. The set of solutions of hatx_i from time 0 to t is in the interval [C t + x_i(0), D t + x_i(0)], where x_i(0) is the initial condition of x_i at time zero, and t is the bounded real time you want to compute the reach set up-to. You can do this over all dimensions. To compute the C, D (which will likely vary for each partition and each dimension), depending on how much you care about soundness, you can simply (numerically) maximize and minimize the original ODE dotx_i in each partition.</p> <p>From your other posts, it looks like you are trying to simulate hybrid systems. Simulation will still suffer the problems in trying to represent transcendentals, as even trying to model one trajectory (instead of modeling the set of possible trajectories) will require representing the solution, which is in general transcendental. To my knowledge, this is still done in the simulation community numerically [see, e.g., 3], but there is work on "guaranteed" (sound) integration, which provides bounds on how far off the numerical solution is from the actual (analytic) solution [4, 5].</p> <p>[1] Symbolic reachability computations for families of linear vector fields. Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Journal of Symbolic Computation, 32(3):231-253, September 2001. <a href="http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf" rel="noreferrer">http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf</a></p> <p>[2] E. Asarin, T. Dang, A. Girard, Hybridization methods for the analysis of nonlinear systems, Acta Informatica, 43:7, 2007, 451-476, <a href="http://www.springerlink.com/content/q6755l613l856737/" rel="noreferrer">http://www.springerlink.com/content/q6755l613l856737/</a></p> <p>[3] Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later, Cleve Moler and Charles Van Loan, SIAM Review, Vol. 45, No. 1 (Mar., 2003), pp. 3-49, <a href="http://www.jstor.org/stable/25054364" rel="noreferrer">http://www.jstor.org/stable/25054364</a></p> <p>[4] Automatic, guaranteed integration of analytic functions, Martin C. Eiermann, BIT NUMERICAL MATHEMATICS, 1989, <a href="http://www.springerlink.com/content/q2k30rtx2h2n1815/" rel="noreferrer">http://www.springerlink.com/content/q2k30rtx2h2n1815/</a></p> <p>[5] GRKLib: a Guaranteed Runge Kutta Library, Bouissou, O., Martel, M., Scientific Computing, Computer Arithmetic and Validated Numerics, 2006, <a href="http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402398" rel="noreferrer">http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402398</a></p> <p>[6] Real Algebraic Strategies for MetiTarski Proofs, Grant Olney Passmore, Lawrence C. Paulson, and Leonardo de Moura. Conference on Intelligent Computer Mathematics (CICM/AISC), 2012, <a href="http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf" rel="noreferrer">http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf</a></p>
    singulars
    1. This table or related slice is empty.
    1. POEncoding of first order differential equation as First order formula
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USTaylor
    1. USTaylor
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POEncoding of first order differential equation as First order formula
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COthanx for such a detailed explainaion. You rightly pointed out that i am trying to simulate a hybrid system. But this does not end here, my purpose is to verify certian properties of such systems, which obviously need to take in to account all possible trajectories. I have come across methods like approximating affine dynamics with rectangular one , but it is very much a manual method, and does not tighly enclose possible solutions of ODEs(unill too many approx models are chosen). I am looking for an automaic and sound method for ODE soluions, which in addition could be inegrated with Z3 .
      singulars
      1. PO
      1. UShafizul asad
    2. COIf you want a fully integrated method, your best option is probably to overapproximate the exponentials then. This will be a lot of work though. You could check out more on how MetiTarski does this. Here's another citation (with a tutorial-like explanation) on how this has been done in PVS: Verified Real Number Calculations: A Library for Interval Arithmetic, Daumas, M. and Lester, D. and Munoz, C., 2009. Alternatively, you could look at making calls to either SpaceEx or PHAVer, which are automatic and support affine dynamics. You could then parse the reach sets they generate into Z3.
      singulars
      1. PO
      1. USTaylor
    3. COI know a bit about SpaceEx which is actually an improved version of PHAver.Do you think they could be called from Z3???or do you mean to do it an offline manner?
      singulars
      1. PO
      1. UShafizul asad
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload