实时系统在各领域尤其是嵌入式领域有着广泛的应用，它一般被用在对时间要求非常高的装置上。对于很多实时系统，如果其设计在逻辑、时序方面出现偏差，将会引起严重的后果。随着实时硬件和软件系统的规模及功能迅速地增长，这类系统设计的复杂性和设计中包含微小错误的可能性也随之增长，这就给软件和硬件产品的可靠性带来了重大的挑战。所以工业界期望通过形式化方法和相应工具，在产品设计的早期阶段帮助设计人员发现逻辑错误。 时间自动机理论是对实时系统进行模型检验的一种有效的理论工具。Alur和Dill在上世纪90年代提出的时间自动机理论为时间自动机的模型检验的发展提供了扎实的基础。许多人认识到用时间自动机为实时系统建模非常直观和方便，因而把这一理论应用到工业案例的模型检验中。有关理论发展、工具开发和技术改进的文章不断涌现，这些成果已经在工业界的设计开发过程中得到了很好的应用。基于时间自动机的实时系统模型检验工具开始被工业界接受。 实时系统的许多重要属性可以通过检验系统状态的可达性来验证。时间自动机的可达性分析算法通常采用对符号状态的枚举来遍历其状态空间。符号状态由位置与时间区域组成，时间区域用形如x—y=(＜)n的原子公式的合取式来表示。在对时间自动机进行可达性分析的过程中，分析算法将生成大量的符号状态，往往导致对计算机内存的需求超出了可行的范围。这就是所谓的空间状态爆炸，它将导致验证工作的失败。 本文主要围绕时间自动机的可达性空间约减优化技术展开研究工作，主要内容包括以下几个方面： 1)描述了时间自动机的形式化定义，以及时间自动机可达性验证的基本算法。同时讨论了一些时间自动机检验过程中的数据结构与相关操作。 2)对目前的针对时间自动机可达性状态空间约减技术进行了探讨，将这些技术按照时钟约束优化和搜索路径优化分为两类，并对每种方法给出了相应的评价。 3)给出了一个消减符号状态个数的方法。该方法通过对符号状态间的依赖关系进行分析，在不影响分析结果的前提下消去某些时间区域的原子公式，从而来扩展符号状态。扩展后的符号状态包含有更加多的具体状态，通过删除掉那些被包含的符号状态可以减少算法存储的状态个数，可以节省存储空间。最后给出了相关的案例分析，结果表明这个算法有效地减少了某些时间自动机可达性分析过程中所需的存储空间。