-
题名描述逻辑的动态时序扩展
被引量:5
- 1
-
-
作者
孙永新
赵希顺
符志强
-
机构
中山大学逻辑与认知研究所
仲恺农业工程学院计算机科学与工程学院
-
出处
《计算机应用研究》
CSCD
北大核心
2012年第2期536-541,共6页
-
基金
国家自然科学基金资助项目(60970040)
-
文摘
在一些基于本体的动态应用中,需要描述组合动作和变化域的时间特性。为了对这类应用建模,通过整合动态时序逻辑和描述逻辑,提出一类描述逻辑扩展。分析了该类扩展的基本形式DLTLALC的语法和语义,并提出一种可终止的tableau算法判别DLTLALC公式可满足性。利用该类扩展,可以表达组合动作执行过程中域变化的时间特性,该类扩展为语义Web服务等动态应用建模和推理提供了一条有效途径。
-
关键词
动态时序描述逻辑
动作推理
表判定算法
语义WEB服务
-
Keywords
dynamic linear temporal description logics
reasoning about actions
tableau decision algorithm
semantic Web service
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名带测试动作的动态时序逻辑扩展
- 2
-
-
作者
孙永新
赵希顺
-
机构
仲恺农业工程学院计算机科学与工程学院
中山大学逻辑与认知研究所
-
出处
《计算机应用研究》
CSCD
北大核心
2012年第9期3269-3273,共5页
-
基金
国家自然科学基金资助项目(60970040)
-
文摘
作为一种动态知识表示形式,动态时序逻辑(DLTL)尤适用于正规程序验证,然而它不直接支持测试动作,这使得其应用受到一定限制。为支持测试动作,提出一个DLTL扩展DLTL+和一个判定DLTL+公式可满足性的tableau算法,并给出了算法的正确性以及其时间复杂度为2O(n)的证明。分析表明,DLTL+提供了一种直接的、有效的测试动作支持方式,该方式比已知的其他方式更具有实际应用价值。
-
关键词
测试动作
动态时序逻辑
扩展
TABLEAU算法
计算复杂性
-
Keywords
test action
dynamic linear temporal logic(dltl)
extension
tableau algorithm
computational complexity
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于动态时序描述逻辑的动作理论
- 3
-
-
作者
孙永新
赵希顺
-
机构
中山大学逻辑与认知研究所
仲恺农业工程学院信息科学与技术学院
-
出处
《计算机科学》
CSCD
北大核心
2014年第9期210-214,238,共6页
-
基金
国家自然科学基金项目(61272059)
教育部基地重大项目(11JJD7200020)资助
-
文摘
动态时序描述逻辑(DLTLDL)是一类描述逻辑的动态时序扩展。提出一种基于DLTLALCIO的动态域建模方法,利用该方法可构造出刻画动态域知识的DLTLALCIO理论,并解决动作推理中的框架问题和分支问题。动作推理问题,如动作可执行性和投影问题等,可归结为关于DLTLALCIO理论的推理问题,并最终归结为DLTLALCIO的公式可满足性问题。DLTLALCIO公式可表达动作和时间约束,相对于其他基于描述逻辑的动作形式,基于DLTLALCIO的动作形式在需要执行复杂查询,尤其是含时间或动作的查询的应用场合具有更好的适用性。
-
关键词
动态时序描述逻辑
动作推理
动态域
动作理论
-
Keywords
dynamic linear temporal description logic
Reasoning about action
dynamic domain
Action theory
-
分类号
TP181
[自动化与计算机技术—控制理论与控制工程]
-
-
题名离散实时线性动态逻辑的符号化模型检测
- 4
-
-
作者
骆翔宇
许杭娜
曾昊晟
陈祖希
杨帆
-
机构
华侨大学计算机科学与技术学院
华侨大学机电及自动化学院
-
出处
《计算机科学》
CSCD
北大核心
2020年第9期204-212,共9页
-
基金
国家自然科学基金重点项目(61733006)
国家自然科学基金面上项目(61170028)
+1 种基金
福建省自然科学基金面上项目(2015J01255)
福建省高等学校新世纪优秀人才支持计划项目(2013FJ-NCET-ZR03)。
-
文摘
实时系统的错误往往十分危险甚至是致命的,使用模型检测来保证复杂实时系统的正确性是十分有效的。针对模型检测中传统时态逻辑无法表达实时性质和所有正则属性的问题,文中首先提出一种具有表达离散实时性质、所有正则属性能力的离散实时线性动态逻辑(Real-Time Linear Dynamic Logic,RTLDL);然后使用类似程序控制流标记的方法为RTLDL公式定义起止标记,根据起止标记关系构造时态测试器,提出基于时态测试器的RTLDL符号化模型检测算法;最后基于翻译的方法在模型检测器NuXmv上实现了所提算法,并针对护栏控制系统案例与线性动态逻辑(Linear Dynamic Logic,LDL)模型检测器MCMAS-LDLK进行实验比较。实验结果表明,无论对于LDL还是RTLDL公式的检测,提出的算法的效率均显著优于MCMAS-LDLK。
-
关键词
符号化模型检测
时态测试器
实时线性动态逻辑
离散实时系统
-
Keywords
Symbolic model checking
temporal tester
Real-time linear dynamic logic
Discrete real-time systems
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-