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

Lomuscio A, Qu H, Solanki M, 2012, Towards verifying contract regulated service composition, AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, Vol: 24, Pages: 345-373, ISSN: 1387-2532

Journal article

Boureanu I, Jones AV, Lomuscio A, 2012, Automatic verification of epistemic specifications under convergent equational theories, 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track, Vol: 2, Pages: 1072-1079

We present a methodology for the automatic verification of multi-agent systems against temporal-epistemic specifications derived from higher-level languages defined over convergent equational theories. We introduce a modality called rewriting knowledge that operates on local equalities. We discuss the conditions under which its interpretation can be approximated by a second modality that we introduce called empirical knowledge. Empirical knowledge is computationally attractive from a verification perspective. We report on an implementation of a technique to verify this modality with the open source model checker MCMAS. We evaluate the approach by verifying multi-agent models of electronic voting protocols automatically extracted from high-level descriptions. Copyright © 2012, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Journal article

Jones AV, Knapik M, Lomuscio A, Penczek Wet al., 2012, Group synthesis for parametric temporal-epistemic logic, 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track, Vol: 2, Pages: 880-887

We investigate parameter synthesis in the context of temporal-epistemic logic. We introduce CTLPK, a parametric extension to the branching time temporal-epistemic logic CTLK with free variables representing groups of agents. We give algorithms for automatically synthesising the groups of agents that make a given parametric formula satisfied. We discuss an implementation of the technique on top of the open-source model checker MCMAS and demonstrate its attractiveness by reporting the experimental results obtained. Copyright © 2012, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Journal article

Belardinelli F, Lomuscio A, Patrizi F, 2012, Verification of GSM-based artifact-centric systems through finite abstraction, Proceedings of the 10th International Conference on Service Oriented Computing (ISCOC12), Vol: 7636, Pages: 17-31

Journal article

Belardinelli F, Lomuscio A, Patrizi F, 2012, Verification of GSM-Based Artifact-Centric Systems through Finite Abstraction, Publisher: Springer, Pages: 17-31

Conference paper

Jones AV, Knapik M, Penczek W, Lomuscio Aet al., 2012, Group synthesis for parametric temporal-epistemic logic., Publisher: IFAAMAS, Pages: 1107-1114

Conference paper

Belardinelli F, Lomuscio A, 2012, Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results, Journal of Artificial Intelligence Research, Vol: 45, Pages: 1-45

Journal article

Belardinelli F, Lomuscio A, Patrizi F, 2012, An Abstraction Technique for the Verification of Artifact-Centric Systems, Publisher: AAAI Press, Pages: 319-328

Conference paper

Boureanu I, Jones AV, Lomuscio A, 2012, Automatic verification of epistemic specifications under convergent equational theories., Publisher: IFAAMAS, Pages: 1141-1148

Conference paper

Ezekiel J, Lomuscio A, Molnar L, Veres S, Pebody Met al., 2011, Verifying fault tolerance and self-diagnosability of an autonomous underwater vehicle, Pages: 1659-1664, ISSN: 1045-0823

We report the results obtained during the verification of Autosub6000, an autonomous underwater vehicle used for deep oceanic exploration. Our starting point is the Simulink/Matlab engineering model of the submarine, which is discretised by a compiler into a representation suitable for model checking. We assess the ability of the vehicle to function under degraded conditions by injecting faults automatically into the discretised model. The resulting system is analysed by means of the model checker MCMAS, and conclusions are drawn on the system's ability to withstand faults and to perform self-diagnosis and recovery. We present lessons learnt from this and suggest a general method for verifying autonomous vehicles.

Conference paper

Lomuscio A, Qu H, Russo F, 2011, Automatic data-abstraction in model checking multi-agent systems, Pages: 52-68, ISSN: 0302-9743

We present an automatic data-abstraction technique for the verification of the universal fragment of the temporal-epistemic logic CTLK. We show the correctness of the methodology and present an implementation operating on ISPL models, the input files for MCMAS, a model checker for multi-agent systems. The experimental results point to the attractiveness of the technique in a number of examples in the multi-agent systems domain. © 2011 Springer-Verlag.

Conference paper

Lomuscio A, Penczek W, Solanki M, Szreter Met al., 2011, Runtime Monitoring of Contract Regulated Web Services, FUNDAMENTA INFORMATICAE, Vol: 111, Pages: 339-355, ISSN: 0169-2968

Journal article

Belardinelli F, Lomuscio A, Patrizi F, 2011, Verification of deployed artifact systems via data abstraction, Publisher: Springer, Pages: 142-156

Conference paper

Belardinelli F, Lomuscio A, Patrizi F, 2011, A computationally grounded semantics for artifact centric systems and abstraction results, Publisher: AAAI Press, Pages: 738-743

Conference paper

Belardinelli F, Jones AV, Lomuscio A, 2011, Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata, Fundamenta Informaticae, Vol: 112, Pages: 19-37

Journal article

Lomuscio A, Penczek W, Qu H, 2010, Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems, Pages: 659-666, ISSN: 1548-8403

We investigate partial order reduction Tor model checking multi-agent systems by focusing on interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed. We present a notion of stuttering-equivalence, and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing the experimental results obtained against well-known examples in the MAS literature. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Conference paper

Lomuscio A, Strulo B, Walker N, Wu Pet al., 2010, Assume-Guarantee Reasoning with Local Specifications, 12th International Conference on Formal Engineering Methods, Publisher: SPRINGER-VERLAG BERLIN, Pages: 204-+, ISSN: 0302-9743

Conference paper

Ezekiel J, Lomuscio A, 2010, A Methodology for Automatic Diagnosability Analysis, 12th International Conference on Formal Engineering Methods, Publisher: SPRINGER-VERLAG BERLIN, Pages: 549-564, ISSN: 0302-9743

Conference paper

Cohen M, Lomuscio A, 2010, Non-elementary speed up for model checking synchronous perfect recall, 19th European Conference on Artificial Intelligence (ECAI)/6th Conference on Prestigious Applications of Intelligent Systems (PAIS), Publisher: IOS PRESS, Pages: 1077-+, ISSN: 0922-6389

Conference paper

Kwiatkowska M, Lomuscio A, Qu H, 2010, Parallel Model Checking for Temporal Epistemic Logic, 19th European Conference on Artificial Intelligence (ECAI)/6th Conference on Prestigious Applications of Intelligent Systems (PAIS), Publisher: IOS PRESS, Pages: 543-548, ISSN: 0922-6389

Conference paper

Boureanu I, Cohen M, Lomuscio A, 2010, Model checking detectability of attacks in multiagent systems, Pages: 691-698, ISSN: 1548-8403

Information security is vital to many multiagent system applications. In this paper we formalise the notion of detectability of attacks in a MAS setting and analyse its applicability. We introduce a taxonomy of detectability specifications expressed in temporal-epistemic logic. We illustrate the practical relevance of attack detectability in a case study applied to a variant of Kerberos protocol. We model-check attack detectability in automatically generated MAS models for security protocols. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Conference paper

Jones AV, Lomuscio A, 2010, Distributed BDD-based BMC for the verification of multi-agent systems, Pages: 675-682, ISSN: 1548-8403

We present a method of distributed model checking of multi-agent systems specified by a branching-time temporal-epistemic logic. We introduce a serial algorithm, central to the distributed approach, for combining binary decision diagrams with bounded model checking. The algorithm is based on a notion of "seed states" to allow for state-space partitioning. Exploring individual partitions displays benefits arising from the verification of partial state-spaces. When verifying both an industrial model and a scalable benchmark scenario the serial bounded technique was found to be effective. Results for the distributed technique demonstrate that it out-performs the sequential approach for falsifiable formulae. Experimental data indicates that increasing the number of hosts improves verification efficiency. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

Conference paper

Lomuscio A, Penczek W, Qu H, 2010, Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems, FUNDAMENTA INFORMATICAE, Vol: 101, Pages: 71-90, ISSN: 0169-2968

Journal article

Lomuscio A, Walker NG, Strulo B, Wu Pet al., 2010, Model Checking Optimisation Based Congestion Control Algorithms, Publisher: IOS PRESS, Pages: 77-96, ISSN: 0169-2968

Conference paper

Lomuscio A, Solanki M, Penczek W, Szreter Met al., 2010, Runtime monitoring of contract regulated web services., Publisher: IFAAMAS, Pages: 1449-1450

Conference paper

Belardinelli F, Lomuscio A, 2010, First-Order Linear-time Epistemic Logic Group Knowledge: An Axiomatisation of the Monodic Fragment, Fundamenta Informaticae, Vol: 106, Pages: 175-190

Journal article

Belardinelli F, Lomuscio A, 2010, Interactions between knowledge and time in a first-order logic for multi-agent systems, Publisher: AAAI Press, Pages: 38-48

Conference paper

Lomuscio A, Solanki M, 2009, Mapping OWL-S processes to multi agent systems: a verification oriented approach, 23rd International Conference on Advanced Information Networking and Applications Workshops, Publisher: IEEE, Pages: 488-493

Conference paper

Lomuscio A, Solanki M, 2009, Towards an Agent Based Approach for Verification of OWL-S Process Models, 6th European Sematic Web Conference, Publisher: SPRINGER-VERLAG BERLIN, Pages: 578-592, ISSN: 0302-9743

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

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