【摘 要】
：
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质间的满足关系
【机 构】
：
中国科学院软件研究所计算机科学重点实验室北京100080
【基金项目】
：
国家高技术研究发展计划(863计划)，国家自然科学基金，国家重点基础研究发展计划(973计划)
论文部分内容阅读
引进一个称为LTLC的连续时间时序逻辑,用来对反应系统进行规范与验证.LTLC的一个重要特点是它能在统一的逻辑框架下表示反应系统及其性质,这样就可将系统与性质间的满足关系转化为逻辑公式间的蕴涵关系.同时,采用非负实数集作为时间域还使我们可以利用标准的存在量词来表示变量隐藏,并可用逻辑蕴涵来表示反应系统间的求精关系.该文首先给出了LTLC的一个简单介绍,然后讨论了如何使用LTLC对反应系统进行表示与推理,最后证明了一个关于LTLC的可判定性结果.此结果可用于有穷状态反应系统的自动验证.
其他文献
在线群体交互有助于数字图书馆发挥其服务人类需求的潜力,但如何量化在线群体交互对个人信息访问方面的影响还有待进一步研究.该文用隐Markov模型(HMM)来建模交互用户的状态
消除由于光照等条件变化而对图像颜色值产生的影响是进行彩色图像的识别和分析的关键 .该文从表面反射的有限维线性模型出发 ,在理想情况下导出了颜色值从非标准光照到标准光照的线性转换关系 .实际上 ,由于成像系统本身采用了一些处理技术 ,使得转换关系应为非线性 .文中提出了新的监督颜色校正方法 ,通过在图像摄取环境中放置监督色板 ,并借鉴监督学习的思想 ,分别采用线性回归、多项式回归和BP神经网络三种方