信息物理系统(Cyber-Physical System, CPS)是一种新的智能系统,它集成了信息计算,信息通信和系统控制过程。在信息物理系统中,信息计算过程和物理控制过程彼此之间通过有线和无线网络交互,并且系统也在网络空间中操控物理实体。这样,在时间和空间上,网络世界和物理世界之间频繁的发生相互作用。因此,在CPS系统建模时应该考虑到时间和空间信息。传统方法在处理这些信息时往往只注重其中的一个方面,在处理CPS中复杂的信息时,显然是不能满足要求的。因此,摆在我们面前的一个重要问题是：如何捕捉信息物理系统中的时间和空间信息进行建模,并利用这些信息描述系统中的逻辑属性和行为约束。一方面,为了描述这些具有时间和空间特征的辑属性和行为约束,我们需要构造一种具有时空特征的逻辑语言。另一方面,为了能够捕获时间和空间信息到CPS模型,现有的大多数模型并不能完全满足CPS系统设计的要求,所以需要一个新的理论模型来建模CPS系统。时态逻辑在形式化方法方面有重要的作用,它能够满足对实时系统中约束条件的描述和系统的符号化表示,以及在时间相关的命题演算方面的需求。其中,命题时态逻辑PTL是最为常用的一种。空间逻辑是一个适合空间表示和推理的逻辑,常见的有RCC-8, BRCC, S4U以及S4u的其它分支。其中,S4u的表达能力最强。如果将PTL和S4u有效的结合,那么这样就能同时满足对时间和空间信息的表达。在系统建模方面,混成自动机能够有效的对CPS系统的离散行为和连续行为进行建模。然而,对位置相关的信息不能有效的表示,特别是对空间约束的描述。这样我们需要对混成系统在空间变量和空间表达式方面进行扩充,提高其建模能力,使得能够满足对CPS系统的建模。因此,本文为了建模时空关系,根据PTL,S4。和扩展逻辑语言的方法,构造了一种时空逻辑语言,并且给出了相应的语义。这种逻辑语言用来表达各种逻辑表达式的逻辑运算(包括空间表达式,时钟表达式,连续表达式,离散表达式等)。这样时间,空间以及其它形式的变量能够一起进行计算。基于这种逻辑语言,我们对混成系统在空间变量和空间表达式方面进行扩展,从而构造了一种时空自动机模型。并且,基于标记迁移系统,给出了相关的形式化语义(包括状态语义,状态转移语义,迹语义以及并行组合语义)。之后,利用我们的时空逻辑,描述了CPS系统中几种经典的性质(包括安全性,持续性等)。当然其它更复杂的性质也可以用该逻辑系统来表达。最后,在上述工作的基础上,以一个列车控制系统为例,进行系统建模,语义描述和性质描述,具体说明了时空混成自动机和时空逻辑的用法和作用。