An Automata-Theoretic Approach to Design Synthesis

TF07：设计综合的自动机理论方法随着计算机化系统变得越来越大，越来越复杂，并且越来越分散，越来越多的设计工作进入了验证和验证工作。人们越来越需要通过设计来保证系统的可靠性、正确性和效率的形式化方法。研究人员将通过建立计算系统的自动设计综合理论来解决这一挑战。新技术将能够在更短的设计周期内以更低的成本开发出更高质量的系统。该项目的目标是发展自动化系统设计综合的基本理论。最终的目标是在设计生产力方面有明显的提高。这个项目的重点将是为基于断言的设计综合开发算法工具。研究人员将发展自动机和博弈论的方法，以基于断言的意向系统设计。虽然游戏和自动机的主要焦点传统上是有限对象（或非常简单的无限对象），但有必要将这种方法扩展到我们在大多数实际应用中面临的更复杂的情况，而这种方法尚未得到充分开发或利用。这个项目的智力价值在于游戏、自动机和逻辑之间的相互作用。我们的目标是在这一领域取得根本性的进步，旨在发展自动化设计技术。这些对于开发可靠、健壮和可伸缩的计算系统至关重要。

TF07: An Automata-Theoretic Approach to Design SynthesisAs computerized systems are becoming larger, more complex, and increasingly distributed, a larger and larger portion of the design effort goes into the validation and verification effort. There is a growing need for formal methods that guarantee systems reliability, correctness, and efficiency by design. The investigators will address this challenge by contributing to the the establishment of a theory of automated design synthesis of computing systems. The new techniques will enable the development of systems of higher quality within shorter design cycles and with lower costs. The goal of the project is the development of a fundamental theory for automated system design synthesis. The ultimate goal is a demonstrable improvement in design productivity.The focus of this project will be the development of algorithmic tools for assertion-based design synthesis. The investigators will develop automata- and game-theoretic approach to assertion-based intentional system design. While the main focus of games and automata has traditionally been on finite objects (or very simple infinite ones), it is necessary to extend this approach to the more complex situations that we face in most practical applications, and for which the method is not yet adequately developed or exploited. The intellectual merit of this project is the interplay between games, automata, and logic. Our aim is to make fundamental progress in this area, aimed at the development of automated design techniques. These are crucial for the development of reliable, robust, and scalable computing systems.