| 郭婧,徐中伟.基于嵌套树的对等博弈应用研究[J].高技术通讯(中文),2015,25(10-11):895~904 |
| 基于嵌套树的对等博弈应用研究 |
|
| |
| DOI： |
| 中文关键词: 对等博弈， 嵌套树， 交替树自动机， μ 演算， 概要 |
| 英文关键词: |
| 基金项目: |
|
| 摘要点击次数: 2869 |
| 全文下载次数: 2307 |
| 中文摘要: |
| 进行了软件系统性质验证研究。首先提出了用嵌套树表示软件程序的方法，以解决软件系统的抽象表示问题，该方法能在表示程序顺序结构的同时，更好地表示调用返回关系。然后定义了嵌套树上的μ 演算，以便将要验证的需求性质用公式表示，并把公式转化成非确定对等嵌套树自动机。最后将自动机与嵌套树结合，转化形成博弈图，并用对等博弈条件来判断博弈的输赢，这等同于检验验证公式是否在嵌套树上成立。相比直接验证，这种判定方法表达更为直观，且更有利于整个过程的自动化。研究表明，将嵌套树中的调用关系展开可形成概要标签树，嵌套树的对等博弈理论也可以应用到概要标签树中。 |
| 英文摘要: |
| |
|
查看全文
查看/发表评论 下载PDF阅读器 |
| 关闭 |
|
|
|
