自动机,逻辑与博弈

• 作者: 孙永强 沈浩
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 自动机 博弈 时态逻辑 互模拟 模型检查
• 年，卷（期）: 2003,（20）
• 所属期刊栏目: 博士论文
• 页码范围: 9-11
• 页数: 3页
• 分类号: TP23
• 字数: 5850字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2003.20.004

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙永强	上海交通大学计算机系	72	373	10.0	15.0
2	沈浩	上海交通大学计算机系	31	159	8.0	11.0