随着信息技术和网络技术的迅速发展，计算机网络在日常生活中的应用日益普遍。如何确保其正确性和安全性成为日益紧迫的问题.在现有的诸多理论和方法中，模型检测以其简洁明了和自动化程度高的特点而受人关注。以色列学者伯努利将时序逻辑引入计算机科学，把它作为系统建模和验证工具取得了非常大的成功，绝大部分以线性时序逻辑为基础的模型检测技术都是基于自动机理论实现的。　　本文在详细介绍了线性时序逻辑（Linear Temporal Logic简称LTL）和自动机理论的基础上，分析了线性时序逻辑在建模规约中的可行性；研究了线性时序逻辑公式转化为自动机的具体算法；引入了集合论中势的概念重点讨论了安全性的各种形式化定义以及等价性证明。所作的主要工作如下：　　1、结合模型检测和自动机理论，重点研究了非确定性自动机（NFA）转化为确定性自动机（DFA）的方法和原理以及Büchi自动机的合并和空集的检测。　　2、将自动机理论与模型检测原理相结合，研究了基于线性时序逻辑（LTL）下的模型检测，设计了LTL转化为自动机的具体算法并分析了算法的正确性和优越性.　　3、基于安全性的各种形式化定义，引入了集合论中势的概念证明了不同定义之间的等价关系并结合自动机的语言特征给出了安全性的判别原理。