从命题时态逻辑产生上下文无关文法

摘要

线性命题时态逻辑能描述有限状态系统的无限行为。这种行为能用上下文无关文法准确地描述。根据该文法，可以构造一个满足时态逻辑公式的Ｋｒｉｐｋｅ结构。本文给出构造对应于命题时态逻辑公式的上下文无关文法及由该文法构造Ｋｒｉｐｋｅ结构的方法。