摘要翻译：
模型检测是一种很有前途的技术，已应用于许多硬件和软件系统的验证。在本文中，我们引入了模型更新的概念，以开发一个扩展模型检查功能的自动系统修改工具。定义了计算树逻辑(CTL)模型的基元更新操作，形式化了CTL模型更新的最小变化原则。这些基本的更新操作，以及底层的最小更改原则，作为CTL模型更新的基础。为我们的CTL模型更新方法提供了基本的语义和计算特征。然后我们描述了一个实现该方法的形式化算法。我们还对著名的微波炉实例和Andrew File System1进行了CTL模型更新的两个案例研究，并从这两个案例中我们进一步提出了一种在复杂系统修改中优化更新结果的方法。
---
英文标题：
《CTL Model Update for System Modifications》
---
作者：
Yulin Ding, Y. Ding, Yan Zhang, Y. Zhang
---
最新提交年份：
2011
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Software Engineering        软件工程
分类描述：Covers design tools, software metrics, testing and debugging, programming environments, etc. Roughly includes material in all of ACM Subject Classes D.2, except that D.2.4 (program verification) should probably have Logics in Computer Science as the primary subject area.
涵盖设计工具、软件度量、测试和调试、编程环境等。大致包括ACM所有主题课程D.2的材料，除了D.2.4（程序验证）可能应该有计算机科学中的逻辑作为主要主题领域。
--

---
英文摘要：
  Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this paper, we introduce the concept of model update towards the development of an automatic system modification tool that extends model checking functions. We define primitive update operations on the models of Computation Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These primitive update operations, together with the underlying minimal change principle, serve as the foundation for CTL model update. Essential semantic and computational characterizations are provided for our CTL model update approach. We then describe a formal algorithm that implements this approach. We also illustrate two case studies of CTL model updates for the well-known microwave oven example and the Andrew File System 1, from which we further propose a method to optimize the update results in complex system modifications.
---
PDF链接：
https://arxiv.org/pdf/1111.0054