摘要： 讨论了特定的自动机、自动机的识别能力、逻辑的表达能力和博弈思想的关系。使用博弈思想可以比较容易地证明一元二阶逻辑(S1S和S2S)的可决定性。主要考虑线性时间(linear time)与分支时间(branch time)两种情况，通过这些逻辑与别的时态逻辑的表达能力的等价性可以证明其它逻辑也具有决定性，可以设计相应的自动机去解决模型检查(Model Checking)问题。

关键词: 自动机, 博弈, 时态逻辑, 互模拟, 模型检查

Abstract: This article covers certain automata, recognizative power of automata, expressive power of logic, and their relation with games. It applies these results to prove the decidability of certain related monadic second-order logic(S1S and S2S). It considers two cases of linear and branching time. These logics are equivalent to some temporal logics on expressive power, and are also very useful in proving decidability of other temporal logic. With decidability some automata can be designed to solve model checking problem.

中图分类号: 

• TP301