Direct formal verification of liveness properties in continuous and hybrid dynamical systems

Andrew Sogokon, Paul Jackson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper is concerned with proof methods for the temporal property of eventuality (a type of liveness) in systems of polynomial ordinary differential equations (ODEs) evolving under constraints. This problem is of a more general interest to hybrid system verification, where reasoning about temporal properties in the continuous fragment is often a bottleneck. Much of the difficulty in handling continuous systems stems from the fact that closed-form solutions to non-linear ODEs are rarely available. We present a general method for proving eventuality properties that works with the differential equations directly, without the need to compute their solutions. Our method is intuitively simple, yet much less conservative than previously reported approaches, making it highly amenable to use as a rule of inference in a formal proof calculus for hybrid systems.
Original languageEnglish
Title of host publication Formal Methods, 20th International Symposium. June 2015
Place of PublicationOxford, United Kingdom
PublisherSpringer-Verlag GmbH
Pages514-531
Number of pages18
Volume9109
ISBN (Electronic)978-3-319-19249-9
ISBN (Print)978-3-319-19248-2
DOIs
Publication statusPublished - Jun 2015
Event20TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS - Oslo, Norway
Duration: 24 Jun 201526 Jun 2015
http://fm2015.ifi.uio.no/

Conference

Conference20TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS
Abbreviated titleFM 2015
Country/TerritoryNorway
CityOslo
Period24/06/1526/06/15
Internet address

Fingerprint

Dive into the research topics of 'Direct formal verification of liveness properties in continuous and hybrid dynamical systems'. Together they form a unique fingerprint.

Cite this