描述逻辑的动态时序扩展

在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。

带测试动作的动态时序逻辑扩展

作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。

基于动态时序描述逻辑的动作理论

动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。

离散实时线性动态逻辑的符号化模型检测

实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。