1 Search Results for "Denman, William"


Document
Abstracting Continuous Nonpolynomial Dynamical Systems

Authors: William Denman

Published in: OASIcs, Volume 28, 2012 Imperial College Computing Student Workshop


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.

Cite as

William Denman. Abstracting Continuous Nonpolynomial Dynamical Systems. In 2012 Imperial College Computing Student Workshop. Open Access Series in Informatics (OASIcs), Volume 28, pp. 42-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Copy BibTex To Clipboard

@InProceedings{denman:OASIcs.ICCSW.2012.42,
  author =	{Denman, William},
  title =	{{Abstracting Continuous Nonpolynomial Dynamical Systems}},
  booktitle =	{2012 Imperial College Computing Student Workshop},
  pages =	{42--48},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-48-4},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{28},
  editor =	{Jones, Andrew V.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2012.42},
  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}
}
  • Refine by Author
  • 1 Denman, William

  • Refine by Classification

  • Refine by Keyword
  • 1 Abstraction
  • 1 Automated Theorem Proving
  • 1 Formal Verification
  • 1 MetiTarski
  • 1 Nonpolynomial System

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail