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.