环境演算与CTL*逻辑:安全属性分析模型
185 浏览量
更新于2024-06-17
收藏 787KB PDF 举报
"这篇论文探讨了如何利用环境演算(Ambient Calculus)和CTL*逻辑(Computation Tree Logic with Stars)进行安全属性分析。作者Radu Mardare和Corrado Priami来自意大利特伦托大学信息与通信学院,他们提出了一种更具有表现力的逻辑,以替代原有的环境逻辑,该逻辑基于单一模态但能处理移动性和动态层次的位置。此外,他们结合了时间逻辑,以便在分析模型的安全问题时重用模型检查算法。
文章首先介绍了环境演算作为一种描述安全问题数学模型的工具,特别适合表达位置及其移动性的层次结构。接着,作者讨论了环境逻辑,它使用两种类型的模态来分别处理空间和时间的断言。然而,他们提出使用单一模态的CTL*逻辑可以更有效地描述这些实体的行为,因为它只关注计算系统对初始状态的修改,而这些修改可以通过环境演算的命题分支时间逻辑来重建系统的实际状态。
论文中还详细阐述了如何构建标记语法树,这是从环境演算的语法树中派生出来的,并增加了标记以支持Kripke结构的命题分支时态逻辑。可达性关系是通过环境演算的约简来定义的,这决定了语法树之间的关系。他们提供了一个算法来计算状态间的可达性,并将其与时态逻辑的模型检测算法相结合,从而在环境演算框架下实现模型检测。
论文强调了这种方法在处理安全问题上的优势,特别是在考虑如防火墙等需要高度保密性的系统时。通过使用时态逻辑,能够更好地分析和验证系统是否满足特定的安全属性。此外,这项工作得到了欧洲研究项目DEGAS和MIUR-COFIN01项目MEFISTO的部分资助。
关键词涉及环境演算、时态逻辑、集合论和模型检测,表明这篇论文涵盖了理论计算机科学的多个核心领域,对于理解如何在动态计算环境中分析安全性和验证系统行为具有重要的学术价值。"
2011-07-18 上传
2010-08-09 上传
2021-10-11 上传
论文
2024-08-06 上传
2024-07-12 上传
2024-06-16 上传
2024-07-12 上传
2024-07-26 上传
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 5
- 资源: 2万+
最新资源
- 计算机人脸表情动画技术发展综述
- 关系数据库的关键字搜索技术综述:模型、架构与未来趋势
- 迭代自适应逆滤波在语音情感识别中的应用
- 概念知识树在旅游领域智能分析中的应用
- 构建is-a层次与OWL本体集成:理论与算法
- 基于语义元的相似度计算方法研究:改进与有效性验证
- 网格梯度多密度聚类算法:去噪与高效聚类
- 网格服务工作流动态调度算法PGSWA研究
- 突发事件连锁反应网络模型与应急预警分析
- BA网络上的病毒营销与网站推广仿真研究
- 离散HSMM故障预测模型:有效提升系统状态预测
- 煤矿安全评价:信息融合与可拓理论的应用
- 多维度Petri网工作流模型MD_WFN:统一建模与应用研究
- 面向过程追踪的知识安全描述方法
- 基于收益的软件过程资源调度优化策略
- 多核环境下基于数据流Java的Web服务器优化实现提升性能