基于符号模型检测的SDG模型可诊断性验证

由于定量信息和非线性因果关系的丢失,符号有向图(signed directed graph,SDG)模型的可诊断性需要进一步地进行校核与验证。为此,提出了基于符号模型检测的SDG模型可诊断性形式化验证方法。首先定义了SDG模型的有限状态变迁系统形式化描述,建立了符号模型验证器(symbolic model verifier,SMV)模型;其次利用SDG的深层知识,构造了可诊断性函数,设定了可诊断性上下文,给出了可诊断性定义。然后,构造了SDG耦合孪生SMV模型,定义了可诊断性的计算树时态逻辑公式,提出了验证算法SDGD_CSMV。最后,通过一个实例验证了可诊断性的判定和算法的有效性。

赋权有向图中最小生成树问题的显式整数规划模型

就具有不对称权重的有向图中的最小生成树问题，本文首次建立了相应的显式整数规划模型，这一模型可以成功地运用整数规划软件包如Ｌｉｎｄｏ等求解。并进一步将这一模型推广到随机最小生成树问题，也即具有随机变量权重的有向图中的最小生成树问题，并设计了相应的求解算法，给出了数值例示。