Stability Preserving Simulations and Bisimulations for Hybrid Systems

Pavithra Prabhakar, Geir Dullerud, Mahesh Viswanathan

Research output: Contribution to journalArticle

Abstract

Pre-orders and equivalence relations between processes, like simulation and bisimulation, have played a central role in the minimization and abstraction based verification and analysis of discrete-state systems for modal and temporal properties. In this paper, we investigate the pre-orders and equivalence relations on hybrid systems which preserve stability. We first show that stability with respect to reference trajectories is not preserved by either the traditional notion of bisimulation or the more recently proposed stronger notions with additional continuity constraints. We introduce the concept of uniformly continuous simulation and bisimulation - namely, simulation and bisimulation with some additional uniform continuity conditions on the relation - that can be used to reason about stability of trajectories. Finally, we show that uniformly continuous simulations and bisimulations are widely prevalent, by recasting many classical results on proving stability of dynamical and hybrid systems as establishing the existence of a simple, obviously stable system that (bi)-simulates the given system through uniformly continuous (bi)-simulations. We also discuss briefly a new abstraction method for stability analysis which is based on the foundations developed in the paper.

Original languageEnglish (US)
Article number7084618
Pages (from-to)3210-3225
Number of pages16
JournalIEEE Transactions on Automatic Control
Volume60
Issue number12
DOIs
StatePublished - Dec 2015

Keywords

  • Hybrid control systems
  • abstractions
  • bisimulations
  • formal verification
  • simulations

ASJC Scopus subject areas

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

Fingerprint Dive into the research topics of 'Stability Preserving Simulations and Bisimulations for Hybrid Systems'. Together they form a unique fingerprint.

  • Cite this