License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.ICCSW.2012.42
URN: urn:nbn:de:0030-drops-37638
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3763/
Go to the corresponding OASIcs Volume Portal

Denman, William

Abstracting Continuous Nonpolynomial Dynamical Systems

pdf-format:
8.pdf (0.7 MB)

Abstract

The reachability problem, whether some unsafe state can be reached, is known to be undecidable for nonlinear dynamical systems. However, finite-state abstractions have successfully been used for safety verification. This paper presents a method for automatically abstracting nonpolynomial systems that do not have analytical or closed form solutions. The abstraction is constructed by splitting up the state-space using nonpolynomial Lyapunov functions. These functions place guarantees on the behaviour of the system without requiring the explicit calculation of trajectories. MetiTarski, an automated theorem prover for special functions (sin, cos, sqrt, exp) is used to identify possible transitions between the abstract states. The resulting finite-state system is perfectly suited for verification by a model checker.

BibTeX - Entry

@InProceedings{denman:OASIcs:2012:3763,
  author =	{William  Denman},
  title =	{{Abstracting Continuous Nonpolynomial Dynamical Systems}},
  booktitle =	{2012 Imperial College Computing Student Workshop},
  pages =	{42--48},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-48-4},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{28},
  editor =	{Andrew V. Jones},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3763},
  URN =		{urn:nbn:de:0030-drops-37638},
  doi =		{10.4230/OASIcs.ICCSW.2012.42},
  annote =	{Keywords: Formal Verification, Automated Theorem Proving, Abstraction, Nonpolynomial System, MetiTarski}
}

Keywords: Formal Verification, Automated Theorem Proving, Abstraction, Nonpolynomial System, MetiTarski
Collection: 2012 Imperial College Computing Student Workshop
Issue Date: 2012
Date of publication: 09.11.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI