Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published June 2012 | public
Journal Article

Verification of Bounded Discrete Horizon Hybrid Automata

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.

Additional Information

© 2011 IEEE. Manuscript received July 15, 2010; revised May 22, 2011 and October 22, 2011; accepted November 17, 2011. Date of publication December 07, 2011; date of current version May 23, 2012. This work was supported in part by the Air Force Office of Scientific Research (AFOSR) under Grant FA9550-09-1-0221 and in part by the National Science Foundation (NSF) under Grant 0729500. Recommended by Associate Editor H. Marchand.

Additional details

Created:
August 19, 2023
Modified:
October 17, 2023