Specifying cyber physical system safety properties with metric temporal spatial logic

The safety properties of Cyber-Physical Systems have characteristics of both time and spatial attributes. Although various hybrid logic languages have been proposed to represent and reason both time and spatial attribute, most of them are not concerned on the quantitative problem which is important for mission-critical CPSs to specify and verify safety properties. In this paper, we propose a language named metric temporal-spatial logic (MTSL) to solve the problem. MTSL is the combination result of the metric temporal logic (MTL) and the spatial logic S4u. It can represent and reason CPS safety properties with both temporal and spatial attributes in a time quantitative manner. Based on different expressivity requirements, we define two kinds of MTSL languages named MTSLtPC and MTSLtOC. Their computational complexity of satisfiability problem are analysed. Moreover, in order to construct a decidable metric temporalspatial logic which can be used to define safety properties, we also point out that one may use safety metric temporal logic (SMTL) as the temporal language. The application of MTSLs are illustrated by case studies coming from transportation domain.