Verification of bounded discrete horizon hybrid automata

Vladimeros Vladimerou, Pavithra Prabhakar, Mahesh Viswanathan, Geir Dullerud

Research output: Contribution to journalArticlepeer-review

Abstract

We consider the class of o-minimally definable hybrid automata with a bounded discrete-transition horizon. We show that for every hybrid automata in this class, there exists a bisimulation of finite index, and that the bisimulation quotient can be effectively constructed when the underlying o-minimal theory is decidable. More importantly, we give natural specifications for hybrid automata which ensure the boundedness of discrete-transition horizons. In addition, we show that these specifications are reasonably tight with respect to the decidability of the models and that they can model modern day real-time and embedded systems. As a result, the analysis of several problems for these systems admit effective algorithms. We provide a representative example of a hybrid automaton in this class. Unlike previously examined subclasses of o-minimally defined hybrid automata with decidable verification properties and extended o-minimal hybrid automata, we do not impose re-initialization of the continuous variables in a memoryless fashion when a discrete transition is taken. Our class of hybrid systems has both rich continuous dynamics and strong discrete-continuous coupling, showing that it is not necessary to either simplify the continuous dynamics or restrict the discrete dynamics to achieve decidability.

Original languageEnglish (US)
Article number6096371
Pages (from-to)1445-1455
Number of pages11
JournalIEEE Transactions on Automatic Control
Volume57
Issue number6
DOIs
StatePublished - Jun 6 2012

Keywords

  • Cyber physical systems
  • hybrid automata
  • o-minimality
  • verification

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Computer Science Applications
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Verification of bounded discrete horizon hybrid automata'. Together they form a unique fingerprint.

Cite this