Spatio-Temporal Logic For Cyber-Physical Systems

Cyber-Physical Systems (CPSs) integrate computing, communication and control processes, which are new intelligent systems. In CPSs, computation process and physical control process interact with each other through wired and wireless networks, and CP-S will operate the physical entities in cyberspace. 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. Tra-ditional approaches for processing information only pay attention in one aspect of them, but for complex information in CPS this can not work. However, how do we capture temporal and spatial information into CPS models that allows for describing the logical properties and constraints is still an unsolved problem in the CPS. In order to specify the logical properties and constraints with time and space, a spatio-temporal logic is need to constructed. The requirements of capturing temporal and spatial information into CPS models determine that most existing models cannot fully meet the requirements of CPS system design, so a new theoretical model is needed to design a unified CPS system.Temporal logic has found an important application in formal methods, where it is used to specify requirements of real-time systems on rules and symbolism for represent-ing, and reasoning about propositions qualified in terms of time. Propositional temporal logic (PTL) is one of the best known temporal logics. Spatial logic is a number of log-ics suitable for qualitative spatial representation and reasoning, such as RCC-S, BRCC, S4u and other fragments of S4u. The most expressive spatial formalism of them is S4u. The hybrid of PT L and S4u is able to cover the expression both spatial and temporal information.Cyber-physical systems can be usefully modeled as hybrid automata combining the physical dynamics within modes with discrete switching behavior between modes. How-ever, the location information can not be captured into models, especially spatial con-straints. We need to extend spatial variables and spatial expressions into hybrid automata to increase the ability of expression for CPSs.In this paper, for modeling the relations between spatial terms and time, we propose a spatio-temporal logic based on PTL, Sr4u and the method to enrich a logic. The logic is used to express the logical connections between all kinds of expressions (including spatial expressions) in CPS. Thus, time, spatial terms and other type of variables can calculate together. We constructs a spatio-temporal hybrid automaton for Cyber-Physical Systems, which is an extension of hybrid automata with spatial variables, spatial expressions based on spatio-temporal logic. Then, we give formal semantics (including states, transition, trace and parallel composition) of the automaton based on labeled transition systems. After that, we use the spatio-temporal logic to specify some classical properties of CPSs (such as Safety Property, Guarantee Property, Obligation Property, Response Property, Persistence Property, Reactive Property). Without doubt, more complex properties can be expressed by the logic. In the end of the paper, a Train Control System is employed as a case study to show the usage of spatio-temporal hybrid automata.