【摘 要】
：
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL
【机 构】
：
桂林电子科技大学计算机科学与工程学院
论文部分内容阅读
时态描述逻辑ALC-LTL将描述逻辑ALC的描述能力与线性时态逻辑LTL的刻画能力结合起来,在具有较强描述能力的同时还使得可满足性问题保持在EXPTIME-完全这个级别。针对ALC-LTL缺少有效的判定算法的现状,将LTL的Tableau判定算法与描述逻辑ALC的推理机制有机地结合起来,给出了ALC-LTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。该算法具有很好的可扩展性。当ALC-LTL中的描述逻辑从ALC改变为任何一个具有可判定性特征的描述逻辑X时,只需要对算法进行简单修改,就可
其他文献
以模型检验为目标,从时间的约束角度出发,提出一种基于XML文档的Web应用的模型抽取方法。模型抽取由时间及相关链接的提取、模型构造和结果显示3部分组成。首先,通过对Web应
针对直线式时栅传感器的动态测量,提出了直线式时栅传感器的主要动态误差源。采用直线光栅尺,光栅测量值作为直线式时栅传感器空间位置测量的标准量,直线式时栅传感器的预测测量值与之进行比较,从而得到动态预测测量的误差值。对测量的误差值进行数据的预处理:数据的截断和采样、异常数据剔除,预处理后对误差值进行频谱分析,提取出幅值和相位,以便于用软件实现谐波修正,提高直线式时栅传感器的精度。
容栅千分传感器广泛应用于位移测量中,设计的容栅千分传感器,将普通容栅传感器在线路板上的刻线划分移植到了半导体硅片上,利用了半导体的工艺技术,实现刻线划分的高精度、高密度,从而达到普通线路板无法达到的精度,将容栅传感器的分辨力提高至0.001mm。
结合已有的键盘记录器,分析了Windows中从用户按键到应用程序处理消息的过程,并针对该过程详细分析了可能出现的安全威胁。在此基础上提出了基于硬件辅助虚拟化的反键盘记录
为了有效组织和管理远程教学环境中存在的分布、异构资源,基于分层建模思想,提出了一种远程教育资源管理系统资源管理模型。同时,在该模型基础上,基于池化技术和异步消息通信
针对单视觉通道唇读系统中唇部特征的提取问题提出了基于DCT+ONPP的特征提取方法。相对于保持全局结构特性的PCA方法,ONPP是一种既保持局部邻域几何特性又兼顾全局的线性降维技术。实验证明提出的方法优于DCT+PCA的特征提取方法。另外还对邻域点个数对系统性能的影响做了相应的研究,发现邻域点为3时该方法具有较好的识别效果。
针对当前OSGi规范没有对服务的实时性提出具体标准和详细解决方案的问题,试图将Java实时规范（Real-Time Specification for Java,RTSJ）整合到OSGi架构中,以提供一种在动态实时
并发程序的测试路径具有不可预测性,而Petri网在描述并发方面具有其它系统模型无法比拟的优势。因此通过Petri网来产生并发程序的测试路径：对有并发程序的源代码构造的Petri网
开源FUSE文件系统用户模块实现方式采用多线程并发模型,在高并发条件下,线程间的同步将降低系统的吞吐率,增加响应时间。基于流水线分段数据通信思想和异步事件网络驱动模型,
针对面向对象方法的数学理论基础相对薄弱的问题,利用共代数方法从范畴论及观察的角度研究面向对象的形式语义及行为关系。首先,给出类和对象的共代数描述,其中抽象类定义成