Spatio-temporal hybrid automata for cyber-physical systems

Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Close interactions between the cyber and physical worlds occur in time and space frequently. Therefore, both temporal and spatial information should be taken into consideration when modeling CPS systems. However, how we can capture temporal and spatial information into CPS models that allow describing the logical properties and constraints is still an unsolved problem in the CPS. In this paper, a spatio-temporal logic is provided, including the syntax and semantics, for describing the logical properties and constraints. Based on the logic, we propose an extended hybrid automaton, spatio-temporal hybrid automaton for CPSs. The automaton increases the ability to express spatial variables, spatial expression and related constraints on spatial terms. Then, we define formal semantics of spatio-temporal hybrid automata based on labeled transition systems. At the end of this paper, a Train Control System is introduced as a case study to show how to model the system behavior with spatio-temporal hybrid automata.