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

187 results found

Cohen M, Dam M, Russo F, Lomuscio Aet al., 2009, Abstraction in model checking multi-agent systems, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 710-717, ISSN: 1548-8403

We present an abstraction technique for multi-agent, systems preserving temporal-epistcrnic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain. Copyright © 2009, International Foundation for Autonomous Agents and Multiagent Systems.

Journal article

, 2009,

Conference paper

Cohen M, Dam M, Lomuscio A, Qu Het al., 2009, A Symmetry Reduction Technique for Model Checking Temporal-Epistemic Logic, 21st International Joint Conference on Artificial Intelligence (IJCAI-09), Publisher: IJCAI-INT JOINT CONF ARTIF INTELL, Pages: 721-726

Conference paper

, 2009,

Conference paper

Lomuscio A, Penczek W, Qu H, 2009, Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic, 5th International Workshop on Model Checking and Artificial Intelligence (MoChArt 2008), Publisher: SPRINGER-VERLAG BERLIN, Pages: 106-+, ISSN: 0302-9743

Conference paper

Cohen M, Dam M, Lomuscio A, Qi Het al., 2009, A Data Symmetry Reduction Technique for Temporal-epistemic Logic, 7th International Symposium on Automated Technology for Verification and Analysis, Publisher: SPRINGER-VERLAG BERLIN, Pages: 69-83, ISSN: 0302-9743

Conference paper

Ezekiel J, Lomuscio A, 2009, An automated approach to verifying diagnosability in multi-agent systems, 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009), Publisher: IEEE COMPUTER SOC, Pages: 51-60

Conference paper

Lomuscio A, Qu H, Raimondi F, 2009, MCMAS: A Model Checker for the Verification of Multi-Agent Systems, 21st International Conference on Computer Aided Verification, Publisher: SPRINGER-VERLAG BERLIN, Pages: 682-688, ISSN: 0302-9743

Conference paper

Boureanu I, Cohen M, Lomuscio A, 2009, Automatic verification of temporal-epistemic properties of cryptographic protocols., Journal of Applied Non-Classical Logics, Vol: 19, Pages: 463-487, ISSN: 1166-3081

Journal article

Belardinelli F, Lomuscio A, 2009, Quantified Epistemic Logics for Reasoning About Knowledge in Multi-Agent Systems, Artificial Intelligence, Vol: 173, Pages: 982-1013

Journal article

Belardinelli F, Lomuscio A, 2009, First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment, Publisher: Springer, Pages: 140-154

Conference paper

Lomuscio A, Qu H, Raimondi F, 2009, MCMAS: A model checker for Multiagent systems, London

Software

Lomuscio A, Qu H, Solanki M, 2008, Towards verifying contract regulated service composition, Pages: 254-261

We report on a novel approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify web services and the contracts governing them as WSBPEL behaviours. We compile WSBPEL behaviours into the specialised system description language ISPL, to be used with the model checker MCMAS to verify behaviours automatically. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example whose state space is approximately 106 and discuss experimental results. © 2008 IEEE.

Conference paper

Belardinelli F, Lomuscio A, 2008, A complete first-order logic of knowledge and time, Pages: 705-714

We introduce and investigate quantified interpreted systems, a semantics to reason about knowledge and time in a firstorder setting. We provide an axiomatisation, which we show to be sound and complete. We utilise the formalism to study message passing systems (Lamport 1978; Fagin et al 1995) in a first-order setting, and compare the results obtained to those available for the propositional case. Copyright © 2008, Association for the Advancement of Artificial Intelligence.

Conference paper

Lomuscio A, Penczek W, 2008, LDYIS: a Framework for Model Checking Security Protocols, Concurrency Specification and Programming Workshop, Publisher: IOS PRESS, Pages: 359-375, ISSN: 0169-2968

Conference paper

Lomuscio A, Qu H, Solanki M, 2008, Towards verifying compliance in agent-based Web service compositions, Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, Vol: 1, Pages: 262-269, ISSN: 1548-8403

We explore the problem of specification and verification of compliance in agent based Web service compositions. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example where the behaviours of participating agents are governed by contracts. The composition is specified in OWL-S and mapped to our chosen formalism. Finally we use an existing symbolic model checker to verify the example specification whose state space is approximately 221 and discuss experimental results. Copyright © 2008, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Journal article

, 2008,

Conference paper

Belardinelli F, Lomuscio A, 2008, A Complete Quantified Epistemic Logic for Reasoning about Message Passing Systems, 8th International Workshop on Computational Logic in Multi-Agent Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 248-+, ISSN: 0302-9743

Conference paper

Belardinelli F, Lomuscio A, 2007, A quantified epistemic logic for reasoning about multi-agent systems, Pages: 601-603

We investigate quantified interpreted systems, a semantics for multiagent systems in which agents can reason about individuals, their properties, and the relationships among them. We analyse a first-order epistemic language interpreted on this semantics and show soundness and completeness of Q.S5n, an axiomatisation for these structures. © 2007 IFAAMAS.

Conference paper

Lomuscio A, Wo┼║na B, 2007, A temporal epistemic logic with a reset operation, Pages: 574-581

We present an axiomatisation for an extension of a temporal epistemic logic with an epistemic "reset" operator defined on the intersection between epistemic and temporal relations. Additionally we show the logic has the finite model property, hence it is decidable. © 2007 IFAAMAS.

Conference paper

Edelkamp S, Lomuscio A, 2007, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 4428 LNAI, ISSN: 0302-9743

Journal article

Lomuscio A, Penczek W, 2007, Symbolic model checking for temporal-epistemic logics, Publisher: Association for Computing Machinery (ACM), Pages: 77-77, ISSN: 0163-5700

Conference paper

Lomuscio A, Raimondi F, wozna B, 2007, Verification of the TESLA protocol in MCMAS-X, Workshop on the Concurrency Specification and Programming (CS&P), Publisher: IOS PRESS, Pages: 473-486, ISSN: 0169-2968

Conference paper

, 2007,

Conference paper

Lomuscio A, Qu H, Sergot M, Solanki Met al., 2007, Verifying temporal and epistemic properties of web service compositions, 5th International Conference on Service-Oriented Computing (ICSOC 2007), Publisher: SPRINGER-VERLAG BERLIN, Pages: 456-+, ISSN: 0302-9743

Conference paper

Lomuscio A, Pecheur C, Raimondi F, 2007, Automatic Verification of Knowledge and Time with NuSMV, 20th International Joint Conference on Artificial Intelligence, Publisher: IJCAI-INT JOINT CONF ARTIF INTELL, Pages: 1384-1389

Conference paper

, 2007,

Conference paper

Lomuscio A R, Penczek W, Wozna B, 2007, Bounded Model Checking for Knowledge and Real Time, roceedings of the 4th International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS'05), Publisher: Elsevier

Conference paper

Edelkamp S, Lomuscio A, 2007, Proceedings of Mochart4, Publisher: Springer

Book

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

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=4&respub-action=search.html