Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2015)

May 4, 2015, Istanbul, Turkey

Aniello Murano

Title of the talk: Reasoning about module checking

Abstract: Module checking has been introduced twenty years ago as a useful framework to verify the correctness of open systems, that are modules having continuous interaction with an external environment. As the correctness of open systems deeply relies on this interaction, classical approaches for closed-system verifications result to be inadequate. Early applications of module checking considered finite-state open systems in which the environments has perfect information about the module. Successively, the framework has been extended in several directions, including the infinite-state and the imperfect information settings. In this talk we will first recall the basic concepts and the main results regarding finite-state module checking with respect to specifications given in CTL*. Then, we will focus on open pushdown module checking both in the perfect and imperfect information settings. Finally we will move to multi-agent systems and provide a comparison with ATL* model checking.

Mike Wooldridge

Title of the talk: Rational Verification

Abstract: The standard approach to verification (as exemplified in the enormously successful model checking paradigm) is to take a system specification, expressed as a formula of temporal logic, and to check that the specification holds across all computations of the system. In this talk, we propose an alternative approach, which we refer to as "rational verification". In the rational verification paradigm, instead of checking whether a property holds on all computations, we aim to check whether it holds on *all computations that could arise through rational action by system components*. The model of rational action that we adopt is Nash equilibrium. We survey our work in this area, discussing possible models of systems and the preferences of system components, and highlighting complexity results.