LIRa session: Roberto Ciuni

On February 7, at 16:15 we will have a LIRa session with Roberto Ciuni.

Please note that the time of the talk is 16:15-18:00 and not our usual time-slot.

Everyone is cordially invited!

Speaker: Roberto Ciuni, (Ruhr University Bochum)
Title: Completeness of a Group STIT with Next Operator
Date and Time: Thursday, February 7, 2013, 16:15-18:00
Venue: Science Park 904, Room D1.115

Group STIT logics are raising some interest in the logical modelling of multi-agent systems, due to their ability to express what agents do when they combine their individual efforts and form a group (or coalition).
As usual with STIT logics, they are interpreted on trees endowed with a ‘choice function’ and a non-empty set of agents. Temporal STIT logics are also raising some interest, since some form of temporal expressivity is essential to express non-instantaneous agency (cases where there is a temporal hyatus between the action and the outcome). Here I present a group STIT logic which combines Chellas’ stit operators [A] for group agency with a `next’ operator X. The logic is interpreted on a class of structures which I call choice
T x W frames and. I show that the logic is complete relative to T x W frames by applying the Sahlqvist techniques. The interesting point is that Sahlqvist techniques are not directly applicable to choice T x W frames. A key part in the strategy of the completeness proof is then proving an isomorphism between the frames and the structures generated by the Sahlqvist axioms I present as a Hilbert system for the logic. I then add some reamarks over the distinction between additive and superadditive frames, the impact of additivity on completeness, and the connection between additivity and permutation.