线性时态逻辑（LTL）是目前被广泛应用的系统性质规范语言,被应用在模型检查、程序综合等领域。本文主要讨论的是有限线性时态逻辑公式（LTLf）。LTLf公式与LTL公式的区别是一个是解释在有限序列上的,一个是解释在无限序列上的。本文的核心是探索有限线性时态逻辑公式到与其等价的自动机的转换问题,并提出了两种新的算法,将LTLf公式转换成等价的非确定性有限自动机（NFA）和确定性有限自动机（DFA）。NFA可被应用到LTLf可满足性检查,DFA可被应用到程序综合方向。程序综合是一种自动生成某种系统模型的技术,该系统模型的形式符合用户定义的规范,在程序综合方面研究的问题是,给定一个性质规范公式,是否有一个模型在任何情况下都满足性质规范。模型检查技术用来对交互式系统进行验证,在模型检查方向,首先将给定的性质规范取反,生成等价的自动机,再与系统模型做交运算,判断得到的新自动机接收语言是否为空,若为空,则系统满足该性质。本文实验分别将Aaltaf与现有的两个性能最好的LTL到自动机转换的工具MONA和SPOT进行比较。实验表明,本文的工具Aaltaf所生成的自动机和另外两个工具相比略占优势。考虑到另外MONA和SPOT已经被持续开发并维护超过十年,Aaltaf目前只是一个原型,还有很大提升空间。