Workshop in Logics for Multi-Agent Systems

Aniello Murano (University of Naples Federico II)

Title: Formal Aspects of Strategic Reasoning in MAS

Date and time: September 2nd at 2 pm

Abstract:

In formal system design, model checking is a well-established method to automatically check for global correctness of systems. In such a framework, in order to verify whether a system is correct with respect to a desired property, we describe its structure with a mathematical model, specify the property with a temporal logic formula, and check formally that the model satisfies the specification. This method has been first conceived for closed systems whose behavior is completely determined by their internal states and transitions.

In late 90s, interest has arisen in analyzing the behavior of individual components (or sets of components) in systems with multiple entities. The interest began in the field of reactive systems, which are systems that interact continually with their environments and whose behaviour depends on this interaction. Successively, researchers have looked for logics to reason about, and verify strategic behavior of agents in multi-agent systems.

The aim of this talk is to report on the main developments made in the last 20 years in formal verification of reactive and multi-agent systems. In particular, we will report on CTL module checking, ATL model checking, and Strategy Logic.

The Workshop invited talks and coffee break will take place in room MF105 at the Manufacture des Tabacs of the University Toulouse 1 Capitole.

See the detailed building map here (look for Building F).