Title of the talk: Reasoning about module checking
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.
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