本文在对时间自动机进行深入研究的基础上，提出了公式时钟自动机。在公式时钟自动机中，每一个事件对应一个命题、并且针对给定命题集上的每个线性命题时态逻辑公式，本文定义两个时钟：公式记录时钟与公式预测时钟。前者记录公式最近一次被满足时距目前的时间，后者预测下一次公式将被满足时距目前的时间。然后讨论了公式时钟自动机的确定性和非确定性，公式时钟自动机识别的语言类在并、交、补运算下的封闭性；并证明了确定的公式时钟自动机和非确定的公式时钟自动机表达能力的等价性，这意味这每一个非确定的公式时钟自动机都能转换为一个与之识别相同时间语言的确定的公式时钟自动机；将时间字扩展为无穷的，从而定义了公式时钟Büchi自动机与公式时钟Muller自动机；最后给出了用它进行实时系统的形式化验证方面及对实时系统建模的应用。