Hybrid Automata for Formal Modeling and Verification of Cyber-Physical Systems

Abstract

The defining feature of a cyber-physical system(CPS) is the presence of a tight integration of the discrete control(the “cyber”) with the analog environment (the “physical”) viasensors and actuators over wired or wireless communicationnetworks. Hence the functional correctness of a CPS is cruciallydependent not only on the dynamics of the analog physicalenvironment, but also on the decisions taken by the discretecontrol that alter the dynamics of the environment. The frameworkof Hybrid automata—introduced by Alur, Courcoubetis,Henzinger, and Ho—provide a formal model and specificationlanguage to analyze the interaction between the discrete andcontinuous parts of a cyber-physical system. Hybrid automatacan be considered as generalizations of finite state automataaugmented with a finite set of real-valued variables whosedynamics in every state is governed by a set of differentialequations. Moreover, discrete transitions of hybrid automataare guarded by constraints over the values of these real-valuedvariables, and enable discontinuous jumps in the evolution ofthe real-valued variables. Considering the richness of alloweddynamics in a hybrid automata, it is perhaps not surprisingthat the fundamental verification questions, like reachability, areundecidable in general. In this paper we concentrate on thereachability problem for hybrid automata and precisely characterizevarious boundaries between decidable and undecidablesub-classes of hybrid automata.