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

181 results found

, 2006, Preface, Pages: 1-2, ISSN: 1571-0661

CONFERENCE PAPER

, 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, 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, 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

Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Conference on Precision Electromagnetic Measurements (CPEM 06), Publisher: SPRINGER-VERLAG BERLIN, Pages: 29-+, ISSN: 0302-9743

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

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

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, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications., Publisher: ACM, Pages: 548-550

CONFERENCE PAPER

, 2005, Editorial, Pages: 369-370, ISSN: 1570-8683

CONFERENCE PAPER

, 2005, Bounded model checking for deontic interpreted systems, Electronic Notes in Theoretical Computer Science, Vol: 126, Pages: 93-114, ISSN: 1571-0661

We propose a framework for the verification of multi-agent systems' specification by symbolic model checking. The language CTLKD (an extension of CTL) allows for the representation of the temporal evolution of epistemic states of the agents, as well as their correct and incorrect functioning behaviour. We ground our analysis on the semantics of deontic interpreted systems. The verification approach is based on an adaption of the technique of bounded model checking, a mainstream approach in verification of reactive systems. We test our results on a typical communication scenario: the bit transmission problem with faults.

JOURNAL ARTICLE

Kacprzak M, Lomuscio A, Lasica T, Penczek W, Szreter Met al., 2005, Verifying multi-agent systems via unbounded model checking, 3rd International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2004), Publisher: SPRINGER-VERLAG BERLIN, Pages: 189-212, ISSN: 0302-9743

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

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

JOURNAL ARTICLE

Wozna B, Lomuscio A, Penczek W, 2005, Bounded model checking for knowledge and real time., Publisher: ACM, Pages: 165-172

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

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

, 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

, 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

, 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

, 2004, Electronic Notes in Theoretical Computer Science: Preface, ISSN: 1571-0661

CONFERENCE PAPER

, 2004, A tool for specification and verification of epistemic properties in interpreted systems, Electronic Notes in Theoretical Computer Science, Vol: 85, Pages: 176-191, ISSN: 1571-0661

We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems. We apply this methodology to the verification of a communication protocol - the dining cryptographers. © 2004 Published by Elsevier Science B.V.

JOURNAL ARTICLE

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

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

van der Hoek W, Lomuscio A, 2004, A logic for ignorance, DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES, Vol: 2990, Pages: 97-108, ISSN: 0302-9743

JOURNAL ARTICLE

Raimondi F, Lomuscio A, 2004, Automatic verification of deontic interpreted systems by model checking via OBDD'S, 16th European Conference on Artificial Intelligence, Publisher: I O S PRESS, Pages: 53-57, ISSN: 0922-6389

CONFERENCE PAPER

, 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

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

Kacprzak M, Lomuscio A, Lasica T, Penczek W, Szreter Met al., 2004, Verifying Multi-agent Systems via Unbounded Model Checking., Publisher: Springer, Pages: 189-212

CONFERENCE PAPER

Lomuscio A, Sergot M, 2004, A formalisation of violation, error recovery, and enforcement in the bit transmission problem, Journal of Applied Logic, Vol: 2, Pages: 93-116, ISSN: 1570-8683

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