Home » Node » 6005

Next CS&E Seminar -- 24 Nov. 2011 @ 12 -- Francesco Belardinelli

The next CS&E Seminar will be 

24 November 2011
12.00 @ Aula Magna

Francesco Belardinelli
Imperial College London, UK 

First-order Languages  for the Specification of Multi-agent Systems.

Propositional modal languages (temporal, epistemic, deontic, etc.) are a success story on the applications of logic to computer science. Today a  wealth of tools and techniques based on these formalisms are available  for the specification and verification of distributed and multi-agent systems. Still, as increasing complex scenarios (services, e-commerce, e-business) are tackled by the verification community, the need for even more expressive languages is widely felt. Predicate modal languages extend their propositional counterparts with first-order logic, which is typically considered the most "convenient"  setting to formalise natural language. However, predicate modal logic is ridden with bad computational complexity and highly undecidable. We will review some of these undecidability results, and then point to computationally tractable fragments of predicate modal logic. Our investigation is aimed at finding predicate modal logics that are expressive enough to describe a vast class of multi-agent systems, and yet enjoy nice computational complexity in most cases of interest.

Dr Francesco Belardinelli received his PhD from the Scuola Normale Superiore in Pisa, where he also attended the undergraduate programme and received his "Diploma di Licenza". He received his MA in Philosophy from the University of Pisa.
He is currently a Research Associate at the Department of Computing, Imperial College London, working on the EU STREP project ACSI (Artifact Centric Service Interoperation).
Dr Belardinelli's main research interests are focused on logic-based formalisms for reasoning about autonomous systems, in particular, extensions to first-order of modal temporal and epistemic logics, as well as their properties (axiomatisations, decidability, complexity, model checking).

 

© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma