Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

+44 (0)20 7594 8414a.lomuscio Website

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

188 results found

Raimondi F, Lomuscio A, 2007, Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Journal of Applied Logic, Vol: 5, Pages: 235-251, ISSN: 1570-8683

Journal article

Van Der Hoek W, Lomuscio A, Wooldridge M, 2006, On the complexity of practical ATL model checking, Pages: 201-208

We investigate the computational complexity of reasoning about multi-agent systems using the cooperation logic ATL of Alur, Henzinger, and Kupferman. It is known that satisfiability checking is EXPTIME-complete for "full" ATL, and PSPACE-complete (in the general case) for the fragment of ATL corresponding to Pauly's Coalition Logic. In contrast, the model checking problems for ATL and Coalition Logic can both be solved in time polynomial in the size of the formula and the size of model against which the formula is to be checked. However, these latter results assume an extensive representation of models, in which all states of a model are explicitly enumerated. Such representations are not feasible in practice. In this paper we investigate the complexity of the ATL and Coalition Logic model checking problems for a more "reasonable" model representation known as SRML ("Simple Reactive Modules Language"), a simplified version of the actual model representation languages used for model checkers such as SMV and MOCHA. While it is unsurprising that, when measured against such representations, the model checking problems for ATL and Coalition Logic have a higher complexity than when measured against explicit state representations, we show that in fact the ATL and Coalition Logic model checking problems for SRML models have the same complexity as the corresponding satisfiability problems. That is, model checking ATL formulae against SRML models is EXPTIME-complete, and model checking Coalition Logic formulae against SRML models is PSPACE-complete. We conclude by investigating some technical issues around these results, and discussing their implications. Copyright 2006 ACM.

Conference paper

Lomuscio AR, Pecheur C, Raimondi F, 2006, Verification of knowledge and time with NuSMV., Twentieth International Conference on Artificial Intelligence

Conference paper

Kacprzak M, Lomuscio A, Niewiadomski A, Penczek W, Raimondi F, Szreter Met al., 2006, Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol, Meeting on Concurrency Specification and Programming, Publisher: IOS PRESS, Pages: 215-234, ISSN: 0169-2968

Conference paper

van der Hoek W, Lomuscio A, de Vink E, Wooldridge Met al., 2006, Preface, Pages: 1-2, ISSN: 1571-0661

Conference paper

Lomuscio A, Raimondi F, 2006, MCMAS: A model checker for multi-agent systems, 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 450-454, ISSN: 0302-9743

Conference paper

van der Hoek W, Lomuscio A, Wooldridge M, 2006, On the complexity of practical ATL model checking knowledge, strategies, and games in multi-agent systems, Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM

Conference paper

Lomuscio A, Wozna B, 2006, A combination of explicit and deductive knowledge with branching time: Completeness and decidability results, 3rd International Workshop on Declarative Agent Languages and Technologies, Publisher: SPRINGER-VERLAG BERLIN, Pages: 188-204, ISSN: 0302-9743

Conference paper

Lomuscio A, Raimondi F, 2006, Model checking knowledge, strategies, and games in multi-agent systems, Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM

Conference paper

Lomuscio A, Wozna B, 2006, A complete and decidable axiomatisation for deontic interpreted systems, 8th International Workshop on Deontic Logic in Computer Science (DEON 2006), Publisher: SPRINGER-VERLAG BERLIN, Pages: 238-254, ISSN: 0302-9743

Conference paper

Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Pages: 29-42, ISSN: 0302-9743

© Springer-Verlag Berlin Heidelberg 2006. This paper presents complexity results for model checking formulae of CTLK (a logic to reason about time and knowledge in multi-agent systems) in concurrent programs. We apply these results to evaluate the complexity of verifying programs of two model checkers for multi-agent systems: MCMAS and Verics.

Conference paper

Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications., Publisher: ACM, Pages: 548-550

Conference paper

van der Hoek W, Lomuscio A, de Vink E, Wooldridge Met al., 2006, Proceedings of LCMAS05 - Special issue, Electronic Notes of Theoretical Computer Science, Vol: 126

Journal article

Lomuscio A, Wozna B, 2006, A complete and decidable security-specialised logic and its application to the TESLA protocol, Proceedings of 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM

Conference paper

Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Proceedings of 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM

Conference paper

Lomuscio A, Nute D, 2005, Editorial, Pages: 369-370, ISSN: 1570-8683

Conference paper

Raimondi F, Lomuscio A, 2005, Towards symbolic model checking for multi-agent systems via OBDD's, 3rd International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2004), Publisher: SPRINGER-VERLAG BERLIN, Pages: 213-221, ISSN: 0302-9743

Conference paper

Wo┼║na B, Lomuscio A, Penczek W, 2005, Bounded model checking for knowledge and real time, the fourth international joint conference, Publisher: ACM Press

Conference paper

van der Hoek W, Lomuscio A, de Vink E, Wooldridge Met al., 2005, Proceedings of LCMAS04 - Special Issue, Electronic Notes of Theoretical Computer Science, Vol: 126

Journal article

Lomuscio A, Nute D, 2005, Deontic Logic in Computer Science - Special Issue, Journal of Applied Logic, Vol: 3

Journal article

Kacprzak M, Lomuscio A, Penczek W, 2004, From bounded to unbounded model checking for temporal epistemic logic, FUNDAMENTA INFORMATICAE, Vol: 63, Pages: 221-240, ISSN: 0169-2968

Journal article

Raimondi F, Lomuscio A, 2004, Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation, Pages: 630-637

We investigate the problem of the verification of epistemic properties of multiagent systems via model checking. Specifically, we extend and adapt methods based on ordered binary decision diagrams, a mainstream verification technique in reactive systems. We provide an algorithm, and present a software package that implements it. We discuss the software and benchmark it by means of a standard example in the literature, the dining cryptographers.

Conference paper

Kacprzak M, Lomuscio A, Penczek W, 2004, Verification of multiagent systems via unbounded model checking, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2004, Vol: 2, Pages: 638-645

We present an approach to the problem of verification of epistemic properties of multi-agent systems by means of symbolic model checking. In particular, it is shown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we base our discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show how it can be applied to the well-known train, gate and controller problem.

Journal article

Van Der Hoek W, Lomuscio A, 2004, A logic for ignorance, Pages: 117-133, ISSN: 1571-0661

We introduce and motivate a non-standard multi-modal logic to represent and reason about ignorance in Multi-Agent Systems. We argue that in Multi-agent systems being able to reason about what agents ignore is just as important as being able to reason about what agents know. We show a sound and complete axiomatisation for the logic. We investigate its applicability by restating the feasibility condition for the FIPA communication primitive of inform. © 2004 Published by Elsevier Science B.V.

Conference paper

Van Der Hoek W, Lomuscio A, De Vink E, Wooldridge Met al., 2004, Electronic Notes in Theoretical Computer Science: Preface, ISSN: 1571-0661

Conference paper

Raimondi F, Lomuscio A, 2004, Automatic verification of deontic properties of multi-agent systems, 7th International Workshop on Deontic Logic in Computer Science, Publisher: SPRINGER-VERLAG BERLIN, Pages: 228-242, ISSN: 0302-9743

Conference paper

Raimondi F, Lomuscio A, 2004, Automatic verification of deontic interpreted systems by model checking via OBDD's, Pages: 48-52, ISSN: 0922-6389

We present an algorithm for the verification of multiagent systems specified by means of a modal logic that includes a temporal, an epistemic, and a deontic operator. Verification is performed by model checking on OBDD's. We present an implementation of the algorithm and report on experimental results for the bit transmission problem with faults.

Conference paper

Wozna B, Lomuscio A, 2004, A logic for knowledge, correctness, and real time, 5th International Workshop on Computational Logic in Multi-Agent Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 1-15, ISSN: 0302-9743

Conference paper

van der Hoek W, Lomuscio A, 2004, A Logic for Ignorance, Electronic Notes of Theoretical Computer Science, Vol: 85

Journal article

Lomuscio A, Sergot MJ, 2004, A formulation of violation, error recovery, and enforcement in the bit transmission problem, Journal of Applied Logic, Vol: 2

Journal article

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: id=00306568&limit=30&person=true&page=5&respub-action=search.html