A Hybrid Clock Logic System for CPS

Cyber-Physical System (CPS) is a typical intelligent system composed of agents. It has an important feature of spatial temporal constraints. To describe the constraints on agents, Chen proposed the spatial-temporal consistency language (STeC) in 2012 and the hybrid clock system in 2014. In this paper we will set up the hybrid clock logic systems (HCL) to specify the spatial temporal constraint property of agents in CPS. After giving the syntax and semantics of HCL, we consider the satisfaction relationship between a STeC design and HCL specification of a CPS agent. Some case studies show this satisfaction relationship is reasonable. We also introduce a model-checking algorithm for HCL.