Verifying average dwell time of hybrid systems

Research output: Contribution to journalArticlepeer-review

Abstract

Average dwell time (ADT) properties characterize the rate at which a hybrid system performs mode switches. In this article, we present a set of techniques for verifying ADT properties. The stability of a hybrid system A can be verified by combining these techniques with standard methods for checking stability of the individual modes of A. We introduce a new type of simulation relation for hybrid automataswitching simulationfor establishing that a given automaton A switches more rapidly than another automaton B. We show that the question of whether a given hybrid automaton has ADT a can be answered either by checking an invariant or by solving an optimization problem. For classes of hybrid automata for which invariants can be checked automatically, the invariant-based method yields an automatic method for verifying ADT; for automata that are outside this class, the invariant has to be checked using inductive techniques. The optimization-based method is automatic and is applicable to a restricted class of initialized hybrid automata. A solution of the optimization problem either gives a counterexample execution that violates the ADT property, or it confirms that the automaton indeed satisfies the property. The optimization and the invariant-based methods can be used in combination to find the unknown ADT of a given hybrid automaton.

Original languageEnglish (US)
Article number3
JournalTransactions on Embedded Computing Systems
Volume8
Issue number1
DOIs
StatePublished - Dec 1 2008

Keywords

  • Hybrid systems
  • Optimization-based verification
  • Simulation relation

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Verifying average dwell time of hybrid systems'. Together they form a unique fingerprint.

Cite this