SIKS/ICS Master Class

Logic and Agents:

It is all in the game


Utrecht University

24 November 2004


In recent years the tendency is for agent research to be more oriented towards practice. As a consequence it seems that logic and logical formalisms are less important for the progress of the field. With this masterclass we want to show that this is a wrong conception and that logic and formal methods can be of great assistance to us for solving problems in the area of multi-agent systems. This masterclass presents some current research on logic and agents with an underlying focus on the interaction between agents in a multi-agent system.



12.55 – 13.00


13.00 – 13.45

Johan van Benthem (UVA):

Update and Revision in the Course of a Game

13.45 – 14.30

Wiebe van der Hoek(University of Liverpool):

ATL for Verifying Agent Systems


14.30 – 15.00



15.00 – 15.30

Virginia Dignum (UU):

Contracts in Agent Societies

15.30 – 16.00

Catholijn Jonker (NICI)

Properties of Negotiation: The behaviour of negotiators

16.00 – 16.30

Cees Witteveen (Delft University)

Diagnosis and Revision in Planning

16.30 – 17.30



The masterclass is co-organized by the SIKS research school and the Institute for Information and Computer Sciences, Utrecht University. 
Participation is free of charge, but registration is required. Coffee and drinks are included. 
If you want to participate in the masterclass, please send an email before 17 november 2004 to Frank Dignum,, containing your name and affiliation.



The Master class takes place in the Uithof, Utrecht University, room theta of the Educatorium, Leuvenlaan 3.

Directions on how to get to the Uithof can be found here.



Presenter: Johan van Benthem, Universiteit van Amsterdam.

Title: Update and Revision in the Course of a Game

Understanding agents' behaviour in the course of a game involves both information update and belief revision about
future expectations. We give a temporal framework where the two live together in harmony, and show what sort of
logical issues arise. This setting also allows for combination and comparison with other epistemic-temporal frameworks.
Ref. J. van Benthem, 'Update and Revision in Games', lecture notes, Stanford University, June 2004.



Presenter: Wiebe van der Hoek, University of Liverpool.

Title: ATL for Verifying Agent Systems

In this talk I will informally introduce Alternating-time Temporal Logic, a branching-time like logic in which one
can reason about what coalitions of agents can bring about, by choosing appropriate strategies.
I will then argue how model checking ATL can be used to deal with the effectiveness, feasibility and synthesis 
problem of adding social laws to an agent system. Then, I will briefly address extensions of ATL with a notion of 



Presenter: Virginia Dignum, Utrecht University

Title: Contracts in Agent Societies

Agents in a multi-agent system do not just cooperate because they happen to be part of the same system. 
If we want the agents to cooperate we have to either program the rules of cooperation as part of all the agents 
or we have to devise a mechanism that forces the cooperation. In open agent systems, where agents may come and go, 
the first solution is not feasible. We think that in these open environments agents should have “contracts” to regulate their interactions. 
The formal specification of the contracts is based on some form of deontic logic, which allows us to proof some properties
of the agent interactions resulting from the contracts.

Presenter: Catholijn Jonker, NICI, Nijmegen

Title: Properties of Negotiation: The behaviour of negotiators



Presenter: Cees Witteveen, Technical University Delft

Title: Diagnosis and Revision in Planning

We discuss the application of ideas from model-based diagnosis and revision to single-agent and

multi-agent planning systems and illustrate their potential use for plan integration and replanning.