Is there anything well-known about the algorithmic decidability of the satisfiability of an ODE $\dot{x}=f(x)$, $x: [0,1]\to R^n$ with an initial condition $x(0)=x_0$, given that $f(x)$ belongs to some specified class of functions -- for example, component-wise polynomial?
$\begingroup$
$\endgroup$
4
-
$\begingroup$ Please define "satisfiabiity". $\endgroup$– Alexandre EremenkoCommented Jan 13, 2014 at 2:01
-
$\begingroup$ Existence of a $C^1$ solution. $\endgroup$– Peter FranekCommented Jan 13, 2014 at 2:21
-
$\begingroup$ I think the standard Picard existance theorem would answer the question as posed, and it only requires that $f(x)$ be Lipschitz. But then it's not clear to me what the "decidability" and "differential-algebra" tags have to do with the question. $\endgroup$– Igor KhavkineCommented Jan 13, 2014 at 3:33
-
1$\begingroup$ The Theorem you mention only gives local solution (on some neighborhood). My question is about the existence of a global solution, on [0,1] (or, (0, infty)..) $\endgroup$– Peter FranekCommented Jan 13, 2014 at 3:34
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
3
If $f$ is a polynomial, then $C^1$ solution is the same as analytic solution. For analytic solutions, very similar questions are considered in the paper
MR1011182
Denef, J., Lipshitz, L.
Decision problems for differential equations.
J. Symbolic Logic 54 (1989), no. 3, 941–950,
which also contains a survey of earlier results.
I suppose that one can conclude from this paper, and the results cited in it, that the question is undecidable. They also mention some cases when it is decidable.
answered Jan 13, 2014 at 3:37
-
$\begingroup$ Do you maybe know where I can find the paper you are referring at? Do you maybe have a link? Or can you send it to me? $\endgroup$ Commented Aug 28, 2015 at 0:58
-
1$\begingroup$ If you are in a US university, and your library does not have it, use ILL service (interlibrary loan). If you are in other country, ask your librarian. $\endgroup$ Commented Aug 28, 2015 at 1:08
-
1$\begingroup$ If none of the above helps, write to the authors, and request a copy. $\endgroup$ Commented Aug 28, 2015 at 1:09
$\begingroup$
$\endgroup$
In the the paper Boundedness of the Domain of Definition is Undecidable for Polynomial ODEs by Daniel S. Graça et al. (preprint version) they prove the undecidability of deciding the boundedness of the maximal domain of solution of a polynomial ODE.
answered Jan 13, 2014 at 9:25