Verifying tolerant systems using polynomial approximations

Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, Geir E. Dullerud

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

Abstract

In this paper, we approximate a hybrid system with arbitrary flow functions by systems with polynomial flows; the verification of certain properties in systems with polynomial flows can be reduced to the first order theory of reals, and is therefore decidable. The polynomial approximations that we construct ε-simulate (as opposed to "simulate") the original system, and at the same time are tight. We show that for systems that we call tolerant, safety verification of a system can be reduced to the safety verification of the polynomial approximation. Our main technical tool in proving this result is a logical characterization of ε-simulations. We demonstrate the construction of the polynomial approximation, as well as the verification process, by applying it to an example protocol in air traffic coordination.

Original languageEnglish (US)
Title of host publicationProceedings - Real-Time Systems Symposium, RTSS 2009
Pages181-190
Number of pages10
DOIs
StatePublished - 2009
EventReal-Time Systems Symposium, RTSS 2009 - Washington, D.C., United States
Duration: Dec 1 2009Dec 4 2009

Publication series

NameProceedings - Real-Time Systems Symposium
ISSN (Print)1052-8725

Other

OtherReal-Time Systems Symposium, RTSS 2009
Country/TerritoryUnited States
CityWashington, D.C.
Period12/1/0912/4/09

Keywords

  • Approximation
  • Hybrid automata
  • Hybrid systems
  • Logical characterization
  • ε-simulation

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Verifying tolerant systems using polynomial approximations'. Together they form a unique fingerprint.

Cite this