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

Lomuscio A, Michaliszyn J, 2015, Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions., CoRR, Vol: abs/1509.00608

JOURNAL ARTICLE

Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-Based Artifact Systems, JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, Vol: 51, Pages: 333-376, ISSN: 1076-9757

JOURNAL ARTICLE

Gonzalez P, Griesmayer A, Lomuscio A, 2014, Model Checking GSM-Based Multi-Agent Systems, SERVICE-ORIENTED COMPUTING - ICSOC 2013 WORKSHOPS, Vol: 8377, Pages: 54-68, ISSN: 0302-9743

JOURNAL ARTICLE

Čermák P, Lomuscio A, Mogavero F, Murano Aet al., 2014, MCMAS-SLK: A model checker for the verification of strategy logic specifications, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8559 LNCS, Pages: 525-532, ISSN: 0302-9743

Model checking has come of age. A number of techniques are increasingly used in industrial setting to verify hardware and software systems, both against models and concrete implementations. While it is generally accepted that obstacles still remain, notably handling infinite state systems efficiently, much of current work involves refining and improving existing techniques such as predicate abstraction. © 2014 Springer International Publishing.

JOURNAL ARTICLE

Lomuscio AR, Michaliszyn J, 2014, Decidability of model checking multi-agent systems against a class of EHS specifications, 21st European Conference on Artificial Intelligence (ECAI), Publisher: IOS PRESS, Pages: 543-548, ISSN: 0922-6389

CONFERENCE PAPER

, 2014, An abstraction technique for the verification of multi-agent systems against ATL specifications, Pages: 428-437

Copyright © 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. We introduce an abstraction methodology for the verification of multi-agent systems against specifications expressed in alternating-time temporal logic (ATL). Inspired by methodologies such as predicate abstraction, we define a three-valued semantics for the interpretation of ATL formulas on concurrent game structures and compare it to the standard two-valued semantics. We define abstract models and establish preservation results on the three-valued semantics between abstract models and their concrete counterparts. We illustrate the methodology on the large state spaces resulting from a card game.

CONFERENCE PAPER

, 2014, Model checking unbounded artifact-centric systems, Pages: 488-497

Copyright © 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. Artifact-centric systems are a recent paradigm for representing and implementing business processes. We present further results on the verification problem of artifact-centric systems specified by means of FO-CTL specifications. While the general problem is known to be undecidable, results in the literature prove decidability for artifact systems with infinite domains under boundedness and conditions such as uniformity. We here follow a different approach and investigate the general case with infinite domains. We show decidability of the model checking problem for the class of artifact-centric systems whose database schemas consist of a single unary relation, and we show that that the problem is undecidable if artifact systems are defined by using one binary relation or two unary relations.

CONFERENCE PAPER

Belardinelli F, Lomuscio A, Patrizi F, 2014, Verification of Agent-Based Artifact Systems., J. Artif. Intell. Res., Vol: 51, Pages: 333-376

JOURNAL ARTICLE

, 2014, Service-Oriented Computing - ICSOC 2013 Workshops - CCSA, CSB, PASCEB, SWESE, WESOA, and PhD Symposium, Berlin, Germany, December 2-5, 2013. Revised Selected Papers, Publisher: Springer

CONFERENCE PAPER

Lomuscio A, Moss LS, Ovchinnikova E, Rosati Ret al., 2014, Tutorials., Publisher: AAAI Press

CONFERENCE PAPER

, 2013, A cutoff technique for the verification of parameterised interpreted systems with parameterised environments, Pages: 2013-2019, ISSN: 1045-0823

We put forward a cutoff technique for determining the number of agents that is sufficient to consider when checking temporal-epistemic specifications on a system of any size. We identify a special class of interleaved interpreted systems for which we give a parameterised semantics and an abstraction methodology. This enables us to overcome the significant limitations in expressivity present in the state-of-the-art. We present an implementation and discuss experimental results.

CONFERENCE PAPER

, 2013, Decidability of model checking non-uniform artifact-centric quantified interpreted systems, Pages: 725-731, ISSN: 1045-0823

Artifact-Centric Systems are a novel paradigm in service-oriented computing. In the present contribution we show that model checking bounded, nonuniform artifact-centric systems is undecidable. We provide a partial model checking procedure for artifact-centric systems against the universal fragment of a first-order version of the logic CTL. We obtain this result by introducing a counterpart semantics and developing an abstraction methodology operating on these structures. This enables us to generate finite abstractions of infinite artifact-centric systems, hence perform verification on abstract models.

CONFERENCE PAPER

, 2013, An epistemic Halpern-Shoham logic, Pages: 1010-1016, ISSN: 1045-0823

We define a family of epistemic extensions of Halpern-Shoham logic for reasoning about temporal-epistemic properties of multi-agent systems. We exemplify their use and study the complexity of their model checking problem. We show a range of results ranging from PTIME to PSPACE-hard depending on the logic considered.

CONFERENCE PAPER

, 2013, Model checking distributed systems against temporal-epistemic specifications, Pages: 130-145, ISSN: 0302-9743

Concurrency and message reordering are two main causes for the state-explosion in distributed systems with asynchronous communication. We study this domain by analysing ABS, an executable modelling language for object-based distributed systems and present a symbolic model checking methodology for verifying ABS programs against temporal-epistemic specifications. Specifically, we show how to map an ABS program into an ISPL program for verification with MCMAS, a model checker for multi-agent systems. We present a compiler implementing the formal map, exemplify the methodology on a mesh network use case and report experimental results. © 2013 IFIP International Federation for Information Processing.

CONFERENCE PAPER

Lomuscio A, Strulo B, Walker N, Wu Pet al., 2013, ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS, INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, Vol: 24, Pages: 419-444, ISSN: 0129-0541

JOURNAL ARTICLE

, 2013, Automatic verification of parameterised interleaved multi-agent systems, 12th International Conference on Autonomous Agents and Multiagent Systems 2013, AAMAS 2013, Vol: 2, Pages: 861-868

A key problem in verification of multi-agent systems by model checking concerns the fact that the state-space of the system grows exponentially with the number of agents present. This often makes practical model checking unfeasible whenever the system contains more than a few agents. In this paper we put forward a technique to establish a cutoff result, thereby showing that systems with an arbitrary number of agents can be verified by checking a single system consisting of a number of agents equal to the cutoff of the system. While this problem is undecidable in general, we here define a class of parameterised interpreted systems and a parameterised temporal-epistemic logic for which the result can be shown. We exemplify the theoretical results on a robotic example and present an implementation of the technique as an extension of MCMAS, an open-source model checker for multi-agent systems. Copyright © 2013, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.

JOURNAL ARTICLE

Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised multi-agent systems., Publisher: IFAAMAS, Pages: 861-868

CONFERENCE PAPER

Lomuscio A, Pinchinat S, Schlingloff H, 2013, VaToMAS - Verification and Testing of Multi-Agent Systems (Dagstuhl Seminar 13181)., Dagstuhl Reports, Vol: 3, Pages: 151-187

JOURNAL ARTICLE

, 2012, Synthesizing agent protocols from LTL specifications against multiple partially-observable environments, Pages: 457-466

We consider the problem of synthesizing an agent protocol satisfying LTL specifications for multiple, partially-observable environments. We present a sound and complete procedure for solving the synthesis problem in this setting and show it is computationally optimal from a theoretical complexity standpoint. While this produces perfect-recall, hence unbounded, strategies we show how to transform these into agent protocols with bounded number of states. Copyright © 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

CONFERENCE PAPER

, 2012, An abstraction technique for the verification of artifact-centric systems, Pages: 319-328

We explore the paradigm of artifact-centric systems from a knowledge-based perspective. We provide a semantics based on interpreted-systems to interpret a first-order temporal-epistemic language with identity in a multi-agent setting. We consider the model checking problem for this language and provide abstraction results. We isolate a natural subclass of artifact-systems for which the model checking problem is de-cidable. We give an upper bound on the complexity of the model checking problem. Copyright © 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

CONFERENCE PAPER

, 2012, Verification of GSM-based artifact-centric systems through finite abstraction, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7636 LNCS, Pages: 17-31, ISSN: 0302-9743

The GSM framework provides a methodology for the development of artifact-centric systems, an increasingly popular paradigm in service-oriented computing. In this paper we tackle the problem of verifying GSM programs in a multi-agent system setting. We provide an embedding from GSM into a suitable multi-agent systems semantics for reasoning about knowledge and time at the first-order level. While we observe that GSM programs generate infinite models, we isolate a large class of "amenable" systems, which we show admit finite abstractions and are therefore verifiable through model checking. We illustrate the contribution with a procurement use-case taken from the relevant business process literature. © Springer-Verlag Berlin Heidelberg 2012.

JOURNAL ARTICLE

, 2012, Verifying GSM-based business artifacts, Pages: 25-32

Business artifacts allow to manage operations of business processes by capturing the key concepts and relevant information to guide their work flow. The Guard-Stage- Milestone (GSM) meta-model is a novel formalism for designing business artifacts that features declarative description of the intended behaviour without requiring an explicit specification of the control flow. Its concept of hierarchical structures of stages and explicit rules for the fulfilment of their guards and milestones supports the designing process but poses a challenge for formal verification. We show here how to approach the verification problem by developing a symbolic representation amenable to model checking. The feasibility of the approach is demonstrated by presenting a case study on the direct verification of a GSM model using a tool implementation. © 2012 IEEE.

CONFERENCE PAPER

Belardinelli F, Gonzalez P, Lomuscio A, 2012, Automated Verification of Quantum Protocols using MCMAS, Pages: 48-62

CONFERENCE PAPER

, 2012, Symbolic model checking for temporal-epistemic logic, Pages: 172-195, ISSN: 0302-9743

We survey some of the recent work in verification via symbolic model checking of temporal-epistemic logic. Specifically, we discuss OBDD-based and SAT-based approaches for epistemic logic built on discrete and real-time branching time temporal logic. The underlying semantical model considered throughout is the one of interpreted system, suitably extended whenever necessary. © 2012 Springer-Verlag Berlin Heidelberg.

CONFERENCE PAPER

, 2012, The scientific contribution of marek sergot, Pages: 4-11, ISSN: 0302-9743

Marek Sergot's technical contributions range over different subjects. He has developed a series of novel ideas and formal methods bridging different research domains, such as artificial intelligence, computational logic, philosophical logic, legal theory, artificial intelligence and law, multi-agent systems and bioinformatics. By combining his background in logic and computing with his interest in the law, deontic logic, action, and related areas, and applying to all his capacity to understand the subtleties of social interactions and normative reasoning, Marek has been able to open new directions of research, and has been a reference, an inspiration, and a model for many researchers in the many fields in which he has worked. © 2012 Springer-Verlag Berlin Heidelberg.

CONFERENCE PAPER

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

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, ISSN: 1076-9757

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

, 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

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