现实世界中，许多问题的解决常常需要同时考虑时间信息和空间信息，因此时空推理便应运而生。近年来，时空推理已成为十分活跃的研究方向，在地理信息系统、自治机器人导航、时空数据库、图像理解、形式化验证以及人工智能等领域都有着广泛的应用。时空推理由时序推理和空间推理发展而来。简单地说，时空推理就是从时间和空间两个维度对所研究对象进行的推理，该对象占据了一定空间，并随着时间发生变化。目前，针对时序推理和空间推理方面的研究工作已经分别有了丰富的积累，如何结合这两方面的工作是当前时空推理的研究重点之一，将理论研究向应用领域推广也是时空推理的主要研究目标。本文围绕基于逻辑的时空推理展开研究和讨论，主要工作概括如下：　　首先本文提出了时空逻辑系统PPTLSL，该逻辑通过结合分离逻辑（separation logic）和命题投影时序逻辑（Propositional Projection Temporal Logic，简称PPTL），具备了同时描述空间和时间两个维度信息的表达能力。PPTLSL的空间维度是一个表达能力较强的分离逻辑片段，时间维度为能够表达完全正则性质的PPTL。研究了PPTLSL的判定性和复杂性问题，证明了PPTLSL为可判定的，其复杂性与PPTL相同的重要结论。为了证明PPTLSL的可判定性，提出了一种从PPTLSL到其子集RPPTLSL （Restrcited PPTLSL）的等价可满足转换，接着证明了RPPTLSL能够重用PPTL的判定过程，从而完成了PPTLSL的可判定性证明。分析了PPTLSL的判定复杂度，其中等价可满足转换的复杂度为多项式级别（polynomial），RPPTLSL重用了PPTL的判定过程，其复杂度为非基本（non-elementary），因此PPTLSL的判定复杂度也是非基本的。PPTLSL的判定过程为后续PPTLSL的应用奠定了坚实的理论基础。　　然后，针对现有带指针操作的程序（简称指针程序）验证工作缺少时间维度信息的问题，提出了基于PPTLSL和建模、仿真、验证语言（Modeling，Simulation and Verification Language，简称MSVL）的模型检测方法。内存可以看作空间的一个实例，程序执行过程中内存结构的变化是时空信息的一种体现，一般称之为内存演化性质。本文所提出的模型检测方法采用MSVL编码指针程序，PPTLSL描述内存演化性质。根据PPTLSL的判定过程，PPTLSL可以等价可满足地转换为RPPTLSL，而RPPTLSL和MSVL都是投影时序逻辑（Projection Temporal Logic，简称PTL）的子集，因此程序和性质属于同一个逻辑系统，从而避免了额外的提取程序模型的工作，简化了模型检测过程。基于范式转换技术，分别构造程序和性质的范式图（Normal Form Graph，简称NFG），接着根据自动机理论，生成程序NFG和性质NFG的乘积，用以检查程序是否满足性质。以经典的并发程序和现实应用为案例，说明了所提方法的有效性和可行性。　　最后，将PPTLSL应用于智能规划（简称规划）领域，提出了基于PPTLSL的规划方法。传统的基于时序逻辑的智能规划方法仅能描述规划问题的时序搜索控制信息（Search Control Knowledge，简称SCK），忽略了某些规划问题中存在的空间维度信息，仍然无法缓解状态爆炸问题。因此，本文所提出的规划方法以缩减搜索的状态空间为目标，从规划问题需要满足的时空约束切入，利用PPTLSL描述规划问题的时空SCK，配合前向搜索机制，实现了相应的规划算法，并开发了规划器。选取学术界公认的国际规划竞赛（International Planning Competition，简称IPC）中具有代表性的标准规划问题进行实验，实验表明，基于PPTLSL的规划方法适合解决同时涉及时间和空间信息的规划问题，且规划效率高于当今世界上绝大多数优秀的规划器所采用的方法，而且可以获得更优的规划解。