Alternating-time Temporal Logic



**Session chair:** Michael Wooldridge

**Abstract:** Classical temporal logic enables the specification of on-going behaviors of reactive systems. The systems are modeled by labeled graphs, and path quantification enables the specification to refer to some or all computations of a system. This setting is well suited for specifying and reasoning about systems composed of a single agent. We introduce a computational framework for formally reasoning about multi-agent systems. The framework consists of three ingredients: a temporal-logic syntax (ATL) that explicitly talks about agents, a semantics (alternating transition systems) that captures the capabilities of individual agents, and an algorithm that extends classical model checking (enumerative and symbolic). The talk describes the development of the framework and its applications in formal verification, control, and AI. It also surveys extensions and generalizations, in particular the growing connection between formal methods for multi-agent systems and algorithmic game theory.

*Orna Kupferman will give this talk on the occasion of receiving the IFAAMAS Influential Paper Award for her joint paper with Rajeev Alur and Thomas A. Henzinger on alternating-time temporal logic.*

Keynote: Orna Kupferman - Alternating-time Temporal Logic

keynote

AAMAS is the largest and most influential conference in the area of agents and multiagent systems, bringing together researchers and practitioners in all areas of agent technology and providing and internationally renowned high-profile forum for publishing and finding out about the latest developments in the field. AAMAS is the flagship conference of the non-profit International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS).  

![](https://assets.underline.io/uploads/markdown_image/1/image/ce4604bd54468a006164d16e080204fb.jpg)

Please click on the button below to register for this event.

If you are registered and see this page please check the account email you are logged in with. It must be the same as for the registration.

If you still have trouble accessing the contact please contact support at aamas2021@underline.io 

Orna Kupferman

1

10

SHORT BIO

Presentations

Alternating-time Temporal Logic

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES