【摘 要】
：
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质间的满足关系
【机 构】
：
中国科学院软件研究所计算机科学重点实验室北京100080
【基金项目】
：
国家高技术研究发展计划(863计划)，国家自然科学基金，国家重点基础研究发展计划(973计划)
论文部分内容阅读
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质间的满足关系转化为逻辑公式间的蕴涵关系.同时,采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏,并可用逻辑蕴涵来表示反应系统间的求精关系.该文首先给出了LTLC的一个简单介绍,然后讨论了如何使用LTLC对反应系统进行表示与推理,最后证明了一个关于LTLC的可判定性结果.此结果可用于有穷状态反应系统的自动验证.
其他文献
在线群体交互有助于数字图书馆发挥其服务人类需求的潜力,但如何量化在线群体交互对个人信息访问方面的影响还有待进一步研究.该文用隐Markov模型(HMM)来建模交互用户的状态
消除由于光照等条件变化而对图像颜色值产生的影响是进行彩色图像的识别和分析的关键 .该文从表面反射的有限维线性模型出发 ,在理想情况下导出了颜色值从非标准光照到标准光照的线性转换关系 .实际上 ,由于成像系统本身采用了一些处理技术 ,使得转换关系应为非线性 .文中提出了新的监督颜色校正方法 ,通过在图像摄取环境中放置监督色板 ,并借鉴监督学习的思想 ,分别采用线性回归、多项式回归和BP神经网络三种方
近两年来,兴平化肥厂在生产经营取得显著成绩的同时,选择企业文化做为两个文明建设的最佳“结合点”,大力培育、建构兴化的企业文化内涵,并且初步形成了与兴化实际情况相适应
2009年伊始，在国家一系列方针、政策刺激下，国内轿车消费再度高潮热涨。前几年高速增长的表现，也使得中国成为全球竞争激烈的汽车市场之一。正是在这种繁荣背后，我们要静心思考…
同为“终身工作制”,为什么生产效率相差悬殊? 同样崇尚勤劳节俭,为什么劳动态度大不相同?