| 自动机,逻辑与博弈 |
| |
| 引用本文： | 沈浩,孙永强.自动机,逻辑与博弈[J].计算机工程,2003,29(20):9-11. |
| |
| 作者姓名： | 沈浩 孙永强 |
| |
| 作者单位： | 上海交通大学计算机系,上海,200030 |
| |
| 基金项目： | 国家自然科学基金项目(60073033) |
| |
| 摘 要： | 讨论了特定的自动机、自动机的识别能力、逻辑的表达能力和博弈思想的关系。使用博弈思想可以比较容易地证明一元二阶逻辑(S1S和S2S)的可决定性。主要考虑线性时间(linear time)与分支时间(branch time)两种情况，通过这些逻辑与别的时态逻辑的表达能力的等价性可以证明其它逻辑也具有决定性，可以设计相应的自动机去解决模型检查(Model Checking)问题。
|
| 关 键 词： | 自动机 博弈 时态逻辑 互模拟 模型检查 |
| 文章编号： | 1000-3428(2003)20-0009-03 |
Automata, Logic with Game |
| |
| SHEN Hao,SUN Yongqiang.Automata, Logic with Game[J].Computer Engineering,2003,29(20):9-11. |
| |
| Authors: | SHEN Hao SUN Yongqiang |
| |
| 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. |
| |
| Keywords: | Automata Game Temporal logic Bisimulation Model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
