格值交替树自动机

交替(树)自动机因其本身关于取补运算的简洁性及其与非确定型(树)自动机的等价性,成为自动机与模型检测领域研究的一个新方向.在格值交替自动机与经典交替树自动机概念的基础上,引入格值交替树自动机的概念,并研究了格值交替树自动机的代数封闭性和表达能力.首先,证明了对格值交替树自动机的转移函数取对偶运算,终止权重取补之后所得自动机与原自动机接受语言互补这一结论.其次,证明了格值交替树自动机关于交、并运算的封闭性.最后,讨论了格值交替树自动机和格值树自动机、格值非确定型自动机的表达能力;证明了格值交替树自动机与格值树自动机的等价性,并给出了二者相互转化的算法及其复杂度分析;同时,提供了用格值非确定型自动机来模拟格值交替树自动机的方法.

基于嵌套树的对等博弈应用研究

进行了软件系统性质验证研究。首先提出了用嵌套树表示软件程序的方法,以解决软件系统的抽象表示问题,该方法能在表示程序顺序结构的同时,更好地表示调用返回关系。然后定义了嵌套树上的μ-演算,以便将要验证的需求性质用公式表示,并把公式转化成非确定对等嵌套树自动机。最后将自动机与嵌套树结合,转化形成博弈图,并用对等博弈条件来判断博弈的输赢,这等同于检验验证公式是否在嵌套树上成立。相比直接验证,这种判定方法表达更为直观,且更有利于整个过程的自动化。研究表明,将嵌套树中的调用关系展开可形成概要标签树,嵌套树的对等博弈理论也可以应用到概要标签树中。