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 = {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 |
|
Collection: |
|
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science |
|
Issue Date: |
|
2009 |
|
Date of publication: |
|
14.12.2009 |
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)