Complete and Efficient Checks for Branching-Time Abstractions

计算机程序、汽车中的电子控制单元、软件工程中的模型驱动开发以及生物细胞中的非线性反馈系统都是动态系统或过程的例子，这些动态系统或过程都从它们在正式模型中的捕获和对这些模型的后续分析中受益匪浅。模型创建有助于文档、系统理解，并能促进变更管理。模型检查，即根据固定属性对模型进行分析，可以获得对这些模型所代表的动态系统的细微之处的重要见解，从而使系统验证具有预测能力。自动化或半自动化的模型生成和分析对于将模型检查转移到工业使用环境中的任何实际技术都是必要的。这种技术转移的障碍主要是由于缺乏可扩展性（模型检查要么无法确定，要么需要太多的时间和空间），以及缺乏现有模型检查方法的完全自动化。另一个障碍是，现有的方法不能处理混合路径量词的更复杂的属性，但在现代应用环境中需要，例如，一个系统总是可以达到一个可能发生某种循环反应的状态。“这项研究创建了一个模型检查框架，直接解决了这些障碍，为这一系列复杂的属性：可扩展性，通过减少所有模型检查那些有限状态和小模型的能力；以及通过扩展现有的谓词抽象技术（特别是反示例引导的抽象细化（CEGAR））来实现对更复杂属性设置的自动化。这一研究计划也将用于定量系统，其中系统的动力学由概率分布控制。总而言之，本建议的主要目的是开发一个框架，用于有效地建模，检查和精炼抽象，这些抽象是完整的（即人们总是可以通过一些有限状态抽象发现系统与任何属性的遵从性或不遵从性）和精确的（即抽象模型在其抽象的系统中拥有最大数量的真实属性），用于吸引分支时间和概率的属性。

Computer programs, electronic control units in cars, model-driven development in software engineering, and non-linear feedback systems within biological cells are all examples of dynamical systems or processes that benefit greatly from their capture in formal models and subsequent analysis of such models. Model creation aids documentation, system comprehension and can facilitate change management. Model checking, an analysis of a model with respect to a fixed property, can gain important insights into subtleties of the dynamical systems these models represent, enabling system validation with predictive power.Automated or semi-automated model generation and analysis are necessary for any realistic technology transfer of model checking into industrial use contexts. Barriers to such technology transfer are foremost due to the lack of scalability (model checks are either undecidable or take too must time and space) and to the lack of full automation of existing model-checking methodology. Another barrier is that existing approaches cannot deal with more complex properties that mix path quantifiers but are needed in modern application contexts, e.g. A system can always reach a state from which a certain cyclic reaction is possible.'' This research creates a model-checking framework that addresses these barriers directly for this full range of complex properties: scalability through the ability to reduce all model checks to those with finite-state and small models; and automation through an extension of existing predicate-abstractiontechniques, notably the counter-example-guided abstraction refinement (CEGAR), to this setting of more complex properties.This research programme will also be carried out for quantitive systems in which the dynamics of a system is governed by probability distributions.To summarize, the main aim of this proposal is to develop a framework for efficient modelling, checking, and refining of abstractions that are complete (i.e. one can always discover compliance or non-compliance of a system with any property through some finite-state abstraction) and precise (i.e. the abstract model enjoys a maximum number of properties that are true in the system it abstracts) for properties that appeal to branching time and probabilities.