模型检测是公认的一种比较有效的验证系统正确性和可靠性的方法。在一些安全至关重要的领域检测预知系统的响应时间、事件调度的延迟等一系列的参数尤为重要。实际上大部分的实时系统都有自己的有效活动时间,即我们只需要检测其在某段时间内的性能和参数,也就是对离散实时系统的模型检测。因此对离散实时时态逻辑的模型检测便成为课题组要解决的关键问题,Real-Time Temporal Logic RTCTL*从很大程度上扩展了逻辑描述范围,是一种表达力更强的规范描述逻辑,因此对RTCTL*的研究在形式化验证领域中有着重要的影响和意义。论文的主要研究工作概括如下:1.根据离散实时系统的特征与性质提出并构造了弱公平性约束的有限状态迁移系统Just Discrete System(JDS)作为计算模型,并对JDS之间的同步并行计算规则进行了详细的定义;2.在CTL*语法和语义的基础上扩展定义并解释了RTCTL*的语法和语义,并通过一系列的等式转换添加了一些额外的操作到RTCTL*中;3.通过将RTCTL*公式映射为状态公式,把RTCTL*的符号化模型检测问题转化为CTL的模型检测问题,并对不同类型的RTCTL*公式在模型检测过程中需要借助的第三者(temporal tester)给出构造方法,提出了基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测算法,并从理论上证明了算法的可靠性和完备性;4.论证了生成反例与产生证据这两个概念的对称性,构造了与上述模型检测算法对应的证据生成算法,并同时证明了算法的正确性。