automated strategic reasoning

在计算机系统的设计和实现中，使用形式化方法来确保健壮、正确的行为。传统的计算机操作模式涉及行为的线性序列，但今天的系统是许多组件之间的复杂交互，包括系统环境和人类用户。因此，分析是通过组件之间的逻辑博弈完成的，其中每个组件都试图满足其指定的需求，而不管其他组件做什么：形式主义包括分支时间和竞争的代理联盟。这个项目是利用研究人员最近在自动逻辑推理方面的突破，通过这样的模型来提供系统开发和验证的一般实用技术。

Formal methods are used to ensure robust correct behaviour in design and implementation of computer systems. Traditional models of computer operation involve a linear sequence of behaviour but today’s systems are complex interactions between many components including the environment of the system and human users. Thus analysis is done via a logical game between components where each is trying to meet its specified requirements regardless of what others do: formalisms include branching time and competing coalitions of agents. This project is to take early advantage of recent breakthroughs in automated logical reasoning with such models by the investigator to deliver general practical techniques of system development and verification.