一类线性时段不变式的验证优化与实现

来源 :电脑知识与技术 | 被引量 : 2次 | 上传用户：aa4578

【摘要】

：

线性时段不变式是一类重要的时段演算公式。文献[1]中提出一种验证算法,能够针对以时间自动机建模的系统,模型检验其是否满足一个扩展的线性时段不变式。在验证一类特定公式时,该算法需要引入O(b)个辅助变量,且需全程保留它们的值,会导致检验这类公式所需的变量数和复杂度急剧增长。该文提出一种基于系统反转的模型检验方法,并为线性时段不变式的模型检验问题提供一种全新的解决思路

【作者】

：

胡棐禹

【机构】

：

同济大学软件学院

【出处】

：

电脑知识与技术

【发表日期】

：

2016年02期

【关键词】

：

模型检验时间自动机线性时段不变式切变反向系统 model checking timed automata linear duration invar

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

其他文献

“世界性建筑”的观念与诠释——布鲁诺·陶特的东方经历及其现代建筑普遍性视角

自形成起,国际风格就被视为现代建筑普遍性的一种表现,并由此带来国际风格与地域传统之间的对立和纷争。作为现代建筑运动主要参与者的布鲁诺·陶特,由于晚年在日本、土

期刊

布鲁诺·陶特世界性建筑客观性普遍性跨文化Bruno Tautweltarchitektursachlichkeituniversal

任务驱动教学法在《网络应用服务管理》教学中的应用

摘要：该文针对目前我院开放教育《网络应用服务管理》课程教学的现状及存在的问题，并结合教学案例详细阐述了任务驱动教学法在该课程教学实施过程中的应用。实践证明，任务驱动教学法能有效地提高学生在搭建、管理、部署各种网络应用服务器的方法和技巧。　　关键词：任务驱动；虚拟机；网络应用服务；服务器　　中图分类号：G642 文献标识码：A 文章编号：1009-3044（2016）21-0132-02　　1 背

期刊

任务驱动虚拟机网络应用服务服务器

日本轨道站城协同指向型的城市开发策略和方法

针对国内城市轨道建设中站城分离的现状问题,研究日本城市轨道站城协同的开发策略和方法,借鉴其轨道建设和城市开发一体化的经验。日本通过逐步进阶的轨道发展过程,轨道站周

期刊

轨道建设站城协同高密度城市城市开发rail constructionstation-city coordinationhigh-density ci

基于FPGA的频率特性测试仪的设计

该频率特性测试仪主要包括系统控制部分,双路同步DAC部分,被测网络部分,信号采集处理部分,显示部分和电源部分。全系统以FPGA为主体,正交扫频信号源采用双通道高速DA模块实现

期刊

FPGADDS正交信号发生器幅频特性相频特性FPGA DDS orthogonal signal generator amplitude frequ

上海市高校试办高水平运动队的现状及对策

采用文献资料、问卷调查及专家访谈等研究方法，对上海市高校开展高水平运动队建设的现状进行研究。结果表明：上海市高校试办高水平运动队已具规模，在吸纳运动员生源过程中具有感

期刊

上海市高校高水平运动队学训矛盾体教结合Shanghai City institutions of higher learning high-lev

基于框架的高校科研管理系统的研究

摘要：随着信息化的快速发展和国家对于高校科研的重视，科研项目经费大量的流入高校，如何高效、有效、合理的对科研经费进行管理成为了高校中的疑难问题。为了能够使经费管理系统，进而利用网络和信息化手段建立高校科研管理信息系统，弥补目前系统的缺陷，高校科研经费管理系统成为提高高校管理效率和服务水平成为必然趋势。本文中主要对高校科研经费管理进行了深入的剖析，采用SSM框架开发的方式对管理系统进行了一定的研究和

期刊

高校科研项目经费信息化框架University researchproject fundinginformation technologyS

广州地铁站厅空间环境主观评价研究

为了解及提升地铁站厅公共空间的环境品质,选取广州市内6个具代表性的站厅,运用使用后评价方法,对站厅室内空间尺度及装修、功能组织及流线设计、信息指示及便民设施、物理环

期刊

广州地铁站厅空间品质主观满意度使用后评价metro station Hallspace qualitysubjective satisfaction

RoboCup3D守门员的防守策略研究

摘要：在Robocup3D比赛中，防守一直是一个重要的研究方向。该文提出了一种基于迭代扩展卡尔曼滤波（IEKF）的足球定位方法。这种方法能为为守门员提供精确的足球位置信息，从而提高守门员的扑球与截球成功率。守门员的防守策略包括扑球、主动截球解围等动作，在不同情况下做出合适的选择才能够的更好地提高防守效率与成功率。　　关键词：迭代扩展卡尔曼滤波；扑球；防守策略　　中图分类号：TP242 文献标识码：

期刊

迭代扩展卡尔曼滤波扑球防守策略Iteraative Extend Kalman Filterball-catchingdefensive strate

基于微信公众平台的翻转课堂教学设计及应用研究

摘要：高职院校需要培养高技能复合型人才，急需改变传统的教学模式。该文尝试充分挖掘微信公众平台的教育功能，构建了基于微信公众平台的翻转课堂教学模式，并以高职《中小型网络组建技术》课程为例，开展了基于该模式的教学实践研究，先学后教，以学生为中心，教师进行个性化指导，能力培养为主，全面提高课堂教学质量。　　关键词：微信公众平台；翻转课堂；先学后教；网络组建；能力培养　　中图分类号：G642 文献标识

期刊

微信公众平台翻转课堂先学后教网络组建能力培养

广府传统建筑柱础之时间特征

广府传统建筑柱础经历了一个由模仿中原官方样式,到根植于地域文化进行创新发展的过程,其柱础类型具有较清晰的先后时间特征,而时间特征又与柱础的材料以及在建筑中所处的位

期刊

广府传统建筑柱础类型时间特征

一类线性时段不变式的验证优化与实现

与本文相关的学术论文