Complete and Efficient Checks for Branching-Time Abstractions

完整有效的分支时间抽象检查

• 批准号: EP/E028985/1
• 负责人: Michael Huth
• 金额: $ 52.18万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2007
• 资助国家: 英国
• 起止时间: 2007 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FE028985%2F1
• 关键词: Complete; Efficient; Checks; Branching; Time

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.

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

项目成果

On the Complexity of Semantic Self-minimization

论语义自我最小化的复杂性

• DOI: 10.1016/j.entcs.2009.08.002
• 发表时间: 2009
• 期刊: Electronic Notes in Theoretical Computer Science
• 作者: Antonik A

The Rabin index of parity games: Its complexity and approximation

平价游戏的拉宾指数：其复杂性和近似值

• DOI: 10.1016/j.ic.2015.06.005
• 发表时间: 2015
• 期刊: Information and Computation
• 影响因子: 1
• 作者: Huth M

Foundations of Software Science and Computational Structures

软件科学和计算结构基础

• DOI: 10.1007/978-3-642-19805-2_3
• 发表时间: 2011
• 作者: Levy P

Computational modeling of the EGFR network elucidates control mechanisms regulating signal dynamics.

EGFR 网络的计算模型阐明了调节信号动态的控制机制。

• DOI: 10.1186/1752-0509-3-118
• 发表时间: 2009
• 期刊: BMC systems biology
• 作者: Wang DY

Partial Solvers for Parity Games: Effective Polynomial-Time Composition

奇偶游戏的部分求解器：有效的多项式时间组合

• DOI: 10.48550/arxiv.1609.04085
• 发表时间: 2016
• 期刊: arXiv e-prints
• 作者: Ah-Fat Patrick