A generic transducer-based approach to modelling and verifying infinite-state systems: techniques, applications, and tools

一种基于传感器的通用方法来建模和验证无限状态系统：技术、应用程序和工具

• 批准号: EP/H026878/1
• 负责人: Anthony Lin
• 金额: $ 31.97万
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FH026878%2F1
• 关键词: generic; transducer; based; approach; modelling

Computers have become so complex today that the likelihood of subtle errors is greater than ever before. Moreover, since computerised systems are ubiquitous (e.g. planes, railways, and nuclear power plants), the impact of such errors will certainly be far-reaching. In the past such errors have resulted in a loss of time, money, and even human lives. The development of (fully-automatic) model checking technologies --- pioneered by the recent ACM Turing Award winners Clarke, Emerson, and Sifakis --- has been so influential in minimising the likelihood of subtle errors that model checking has been adopted by major companies including IBM, Intel, Motorola, and NASA. Despite its success, model checking suffers from the inherent state-explosion problem, which remains difficult today even though a substantial progress has been made in the past two decades. The past fifteen years have seen an increasing level of awareness amongst researchers that modelling computerised systems as infinite-state systems is not only more suitable, but might also help circumvent the notorious state-explosion problem. Such a modelling approach views the parameters that cause the state-explosion problem as potentially unbounded or infinite. These include the sizes of arrays, stacks, queues, integer or real valued variables, discrete-time or real-time clocks, and the number of processes in distributed protocols. Instead of the state-explosion problem, such abstractions as infinite-state systems yield undecidability in general. The field of infinite-state model checking aims to develop tools and techniques to deal with this problem. Broadly speaking, approaches to infinite-state model checking can be classified as follows:1. Restrictions to decidable formalisms.2. General (undecidable) formalisms with the aid of decidable semantic restrictions or semi-algorithmsMost research in infinite-state model checking thus far adopts only one of these approaches without seriously considering the other. Moreover, little has been done to see the connections between these two approaches. This is unfortunate since both approaches have their own disadvantages that can be considerably minimised only by considering both approaches in parallel. The project proposes a particular hybrid approach taking into account the two aforementioned approaches simultaneously. The goal is to systematically develop generic tools and techniques for infinite-state model checking aiming for both sound theoretical foundations and practical applicability. This project focuses on general formalisms that are inspired by various notions of finite-state transducers, as they are known to be clean, expressive, and most amenable to theoretical analysis.

今天的计算机已经变得如此复杂，以至于出现细微错误的可能性比以往任何时候都大。此外，由于计算机化系统无处不在（如飞机、铁路和核电站），这些错误的影响肯定会很深远。在过去，这样的错误导致了时间、金钱甚至人的生命的损失。（全自动）模型检测技术的发展-由最近的ACM图灵奖获得者Clarke，Emerson和Sifakis开创-在最大限度地减少细微错误的可能性方面非常有影响力，模型检测已被包括IBM，Intel，Motorola和NASA在内的大公司采用。尽管模型检验取得了巨大的成功，但它仍然存在固有的状态爆炸问题，尽管在过去的二十年里取得了很大的进展，但这一问题仍然很困难。在过去的15年里，研究人员越来越意识到，将计算机化系统建模为无限状态系统不仅更合适，而且可能有助于规避臭名昭著的状态爆炸问题。这种建模方法将导致状态爆炸问题的参数视为潜在的无界或无限。这些包括数组、堆栈、队列、整数或真实的值变量、离散时间或实时时钟的大小，以及分布式协议中进程的数量。而不是状态爆炸问题，这种抽象的无限状态系统产生一般的不可判定性。无限状态模型检测领域的目标是开发工具和技术来处理这个问题。一般来说，无限状态模型检测的方法可以分为以下几类：1。对可判定形式主义的限制。一般（不可判定的）形式主义的援助，可判定的语义限制或semi-algorithms大多数研究在无限状态模型检测迄今为止只采用这些方法之一，而没有认真考虑其他。此外，很少有人看到这两种方法之间的联系。这是不幸的，因为这两种方法都有自己的缺点，只有同时考虑这两种方法才能大大减少这些缺点。该项目提出了一种特别的混合方法，同时考虑到上述两种方法。我们的目标是系统地开发通用工具和技术的无限状态模型检测，旨在既健全的理论基础和实际适用性。这个项目的重点是一般形式主义的灵感来自各种概念的有限状态传感器，因为他们被称为是干净的，表达，最适合理论分析。

项目成果

Expressive languages for path queries over graph-structured data

• DOI: 10.1145/1807085.1807089
• 发表时间: 2010-06
• 期刊: Proceedings of the twenty-ninth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems
• 作者: Pablo Barceló;Carlos A. Hurtado;Leonid Libkin;Peter T. Wood

The Complexity of Verifying Ground Tree Rewrite Systems

• DOI: 10.1109/lics.2011.36
• 发表时间: 2011-06
• 期刊: 2011 IEEE 26th Annual Symposium on Logic in Computer Science
• 作者: Stefan Göller;A. Lin

Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems

通过地面树重写系统细化进程重写系统层次结构

• DOI: 10.1145/2629679
• 发表时间: 2014
• 期刊: ACM Transactions on Computational Logic
• 影响因子: 0.5
• 作者: Göller S

Logic for Programming, Artificial Intelligence, and Reasoning

编程逻辑、人工智能和推理

• DOI: 10.1007/978-3-642-45221-5_9
• 发表时间: 2013
• 作者: Benzmüller C

Concurrency Makes Simple Theories Hard

并发使简单的理论变得困难

• DOI: 10.4230/lipics.stacs.2012.148
• 发表时间: 2012
• 作者: Goller, S.