非干扰定时系统的控制与综合
计算机科学中的逻辑
2012-07-23 v1 形式语言与自动机理论
系统与控制
摘要
本文关注建模为定时自动机的安全定时系统的综合。系统必须满足的安全属性是非干扰属性。直观而言，非干扰确保从高层域到低层域不存在任何因果依赖。文献中已定义了多种非干扰概念，本文重点关注强非确定性非干扰 (SNNI) 及其两种基于 (双) 模拟的变体 (CSNNI 和 BSNNI)。我们考虑由定时自动机指定的定时系统的定时非干扰属性，并研究以下两个问题：(1) 检查是否可能找到一个子系统使其具有非干扰性；如果是，(2) 计算一个（最大的）具有非干扰性的子系统。
引用
@article{arxiv.1207.4984,
title = {Control and Synthesis of Non-Interferent Timed Systems},
author = {Gilles Benattar and Franck Cassez and Didier Lime and Olivier H. Roux},
journal= {arXiv preprint arXiv:1207.4984},
year = {2012}
}