License
when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2009.2334
URN: urn:nbn:de:0030-drops-23342
URL: http://drops.dagstuhl.de/opus/volltexte/2009/2334/

Taly, Ankur ; Tiwari, Ashish

Deductive Verification of Continuous Dynamical Systems

pdf-format:
Dokument 1.pdf (235 KB)


Abstract

We define the notion of inductive invariants for continuous dynamical systems and use it to present inference rules for safety verification of polynomial continuous dynamical systems. We present two different sound and complete inference rules, but neither of these rules can be effectively applied. We then present several simpler and practical inference rules that are sound and relatively complete for different classes of inductive invariants. The simpler inference rules can be effectively checked when all involved sets are semi-algebraic.

BibTeX - Entry

@InProceedings{taly_et_al:LIPIcs:2009:2334,
  author =	{Ankur Taly and Ashish Tiwari},
  title =	{{Deductive Verification of Continuous Dynamical Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{383--394},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Ravi Kannan and K. Narayan Kumar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2334},
  URN =		{urn:nbn:de:0030-drops-23342},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2009.2334},
  annote =	{Keywords: Deductive Verification, inductive invariants, continuous and hybrid dynamical systems, Theory of Reals }
}

Keywords: Deductive Verification, inductive invariants, continuous and hybrid dynamical systems, Theory of Reals
Seminar: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue date: 2009
Date of publication: 14.12.2009


DROPS-Home | Fulltext Search | Imprint Published by LZI