自动机,逻辑与博弈

摘要

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